OAI/AlgebraicGeometry/Seshadri/Projective/FramedMaps.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MaximalSeshadri.Projective.framedSectionsMorphism line 26
  2. lemma OAI.MaximalSeshadri.Projective.framedSectionsMorphism_local line 30
  3. theorem OAI.MaximalSeshadri.Projective.framedSectionsMorphism_preimage line 37
  4. theorem OAI.MaximalSeshadri.Projective.framedSectionsMorphism_over line 51
  5. instance OAI.MaximalSeshadri.Projective.framedSectionsMorphism_proper line 62
  6. theorem OAI.MaximalSeshadri.Projective.framedSectionsMorphism_closed line 70
  7. theorem OAI.MaximalSeshadri.Projective.framedSectionsMorphism_eq line 109
  8. lemma OAI.MaximalSeshadri.Projective.framedSectionsMorphism_eq_sectionsMorphism line 149
  9. lemma OAI.MaximalSeshadri.Geometry.isIso_restricted_section line 169
  10. theorem OAI.MaximalSeshadri.Geometry.LineBundle.power_extension_ratio line 174
  11. lemma OAI.MaximalSeshadri.Geometry.coefficient_ratio line 188
  12. theorem OAI.MaximalSeshadri.Geometry.LineBundle.power_section_embedding line 209
  13. lemma OAI.MaximalSeshadri.Projective.coefficient_postcomp line 286
  14. theorem OAI.MaximalSeshadri.Projective.sectionsMorphism_transport line 299