OAI/AlgebraicGeometry/Seshadri/Projective/SectionMaps.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MaximalSeshadri.Projective.evalAway line 20
  2. lemma OAI.MaximalSeshadri.Projective.evalAway_val line 24
  3. lemma OAI.MaximalSeshadri.Projective.evalAway_transition line 27
  4. lemma OAI.MaximalSeshadri.Projective.evalAway_natural line 42
  5. lemma OAI.MaximalSeshadri.Projective.evalAway_mk_clear line 53
  6. lemma OAI.MaximalSeshadri.Projective.evalAway_scale line 62
  7. def OAI.MaximalSeshadri.Projective.fromUnitCoordinate line 78
  8. lemma OAI.MaximalSeshadri.Projective.fromUnitCoordinate_mul line 82
  9. lemma OAI.MaximalSeshadri.Projective.fromUnitCoordinate_natural line 92
  10. lemma OAI.MaximalSeshadri.Projective.fromUnitCoordinate_scale line 99
  11. lemma OAI.MaximalSeshadri.Projective.fromUnitCoordinate_preimage line 106
  12. theorem OAI.MaximalSeshadri.Projective.fromUnitCoordinate_eq line 118
  13. lemma OAI.MaximalSeshadri.Projective.coordinates_X_mem line 137
  14. def OAI.MaximalSeshadri.Projective.coordinatesMap line 140
  15. lemma OAI.MaximalSeshadri.Projective.coordinates_eval_natural line 145
  16. lemma OAI.MaximalSeshadri.Projective.coordinatesMap_natural line 151
  17. lemma OAI.MaximalSeshadri.Projective.coordinatesMap_scale line 165
  18. lemma OAI.MaximalSeshadri.Projective.coordinatesMap_preimage line 191
  19. structure OAI.MaximalSeshadri.Projective.CoordinateAtlas line 200
  20. def OAI.MaximalSeshadri.Projective.CoordinateAtlas.localMap line 217
  21. lemma OAI.MaximalSeshadri.Projective.CoordinateAtlas.compatible line 221
  22. def OAI.MaximalSeshadri.Projective.CoordinateAtlas.morphism line 234
  23. lemma OAI.MaximalSeshadri.Projective.CoordinateAtlas.cover_morphism line 238
  24. def OAI.MaximalSeshadri.Projective.atlasOfFramedSections line 251
  25. def OAI.MaximalSeshadri.Projective.sectionFrame line 273
  26. lemma OAI.MaximalSeshadri.Projective.sectionFrame_normalized line 279
  27. def OAI.MaximalSeshadri.Projective.sectionsMorphism line 283
  28. lemma OAI.MaximalSeshadri.Projective.sectionsMorphism_local line 301
  29. theorem OAI.MaximalSeshadri.Projective.sectionsMorphism_preimage line 314