OAI/AlgebraicGeometry/Seshadri/Sheaves/PowerExtension.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MaximalSeshadri.Geometry.LineBundle.finite_cover_power_extension line 20
  2. def OAI.MaximalSeshadri.InvertibleLocal.frameOfLE line 100
  3. lemma OAI.MaximalSeshadri.InvertibleLocal.affine_frame line 109
  4. theorem OAI.MaximalSeshadri.Geometry.LineBundle.power_extension line 126
  5. lemma OAI.MaximalSeshadri.TensorLocalization.map_tensor_right_unit line 163
  6. lemma OAI.MaximalSeshadri.Geometry.sheafification_tensor_right_isIso line 188
  7. lemma OAI.MaximalSeshadri.Geometry.sheafification_tensor_left_isIso line 242
  8. def OAI.MaximalSeshadri.Geometry.sheafificationTensorRight line 259
  9. def OAI.MaximalSeshadri.Geometry.sheafificationTensorLeft line 276
  10. def OAI.MaximalSeshadri.Geometry.lineTensorAssoc line 293
  11. def OAI.MaximalSeshadri.Geometry.moduleTensorRightUnit line 303
  12. def OAI.MaximalSeshadri.Geometry.linePowerAdd line 311
  13. def OAI.MaximalSeshadri.Geometry.linePowerMul line 321
  14. theorem OAI.MaximalSeshadri.Geometry.LineBundle.common_degree line 338
  15. theorem OAI.MaximalSeshadri.Geometry.LineBundle.ample_common_degree_cover line 358