OAI/AlgebraicGeometry/Seshadri/Sheaves/Sections.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MaximalSeshadri.Frames.moduleSectionsTopEquiv line 18
  2. def OAI.MaximalSeshadri.Frames.moduleSectionEquiv line 36
  3. lemma OAI.MaximalSeshadri.Frames.moduleSectionEquiv_apply line 39
  4. def OAI.MaximalSeshadri.Frames.openSectionEquiv line 42
  5. lemma OAI.MaximalSeshadri.Frames.section_value_natural line 51
  6. lemma OAI.MaximalSeshadri.Frames.openSectionEquiv_restrict line 58
  7. lemma OAI.MaximalSeshadri.Frames.moduleSectionEquiv_scalar line 74
  8. lemma OAI.MaximalSeshadri.Frames.openSectionEquiv_scalar line 82
  9. lemma OAI.MaximalSeshadri.Frames.openSectionEquiv_restrict_value line 93
  10. lemma OAI.MaximalSeshadri.Frames.image_section_extension line 106
  11. theorem OAI.MaximalSeshadri.Geometry.local_affine_power_extension line 128
  12. lemma OAI.MaximalSeshadri.Geometry.trivialModule_restriction_injective line 171
  13. theorem OAI.MaximalSeshadri.Geometry.LineBundle.restriction_injective line 186
  14. theorem OAI.MaximalSeshadri.Geometry.LineBundle.section_restriction_injective line 220
  15. theorem OAI.MaximalSeshadri.Geometry.LineBundle.glue_dense_subopens line 257