OAI/AlgebraicGeometry/Seshadri/Sheaves/SectionOpens.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MaximalSeshadri.SectionOpens.isIso_of_stalks line 18
  2. lemma OAI.MaximalSeshadri.SectionOpens.stalk_isIso_of_restrict line 29
  3. lemma OAI.MaximalSeshadri.SectionOpens.restrict_isIso_of_stalks line 37
  4. lemma OAI.MaximalSeshadri.SectionOpens.isIso_of_locally_isIso line 44
  5. def OAI.MaximalSeshadri.SectionOpens.isoOpen line 53
  6. lemma OAI.MaximalSeshadri.SectionOpens.mem_isoOpen_iff line 56
  7. theorem OAI.MaximalSeshadri.SectionOpens.isIso_restrict_isoOpen line 62
  8. lemma OAI.MaximalSeshadri.SectionOpens.isoOpen_postcomp line 79
  9. lemma OAI.MaximalSeshadri.SectionOpens.isoOpen_precomp line 96
  10. lemma OAI.MaximalSeshadri.SectionOpens.isoOpen_restrict line 113
  11. lemma OAI.MaximalSeshadri.Frames.isUnit_iff_basicOpen_top line 149
  12. lemma OAI.MaximalSeshadri.Frames.coefficient_restrict_isUnit line 158
  13. theorem OAI.MaximalSeshadri.Frames.isoOpen_eq_basicOpen line 168
  14. lemma OAI.MaximalSeshadri.Frames.isoOpen_restrictSection line 190
  15. theorem OAI.MaximalSeshadri.Frames.preimage_isoOpen line 196
  16. theorem OAI.MaximalSeshadri.Geometry.LineBundle.sectionOpen_power line 212