OAI/AlgebraicGeometry/RelativeTriviality/Coordinates.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CampanaPeternellSix.ProjectiveCoordinates.map_component line 18
  2. def OAI.CampanaPeternellSix.ProjectiveCoordinates.comapIdeal line 32
  3. def OAI.CampanaPeternellSix.ProjectiveCoordinates.mapFraction line 41
  4. def OAI.CampanaPeternellSix.ProjectiveCoordinates.mapLocalization line 49
  5. lemma OAI.CampanaPeternellSix.ProjectiveCoordinates.mapLocalization_mk line 80
  6. def OAI.CampanaPeternellSix.ProjectiveCoordinates.mapLocalRing line 85
  7. lemma OAI.CampanaPeternellSix.ProjectiveCoordinates.val_mapLocalRing line 88
  8. instance OAI.CampanaPeternellSix.ProjectiveCoordinates.(instance at line 94) line 94
  9. lemma OAI.CampanaPeternellSix.ProjectiveCoordinates.isUnit_of_mapLocalRing line 100
  10. def OAI.CampanaPeternellSix.ProjectiveCoordinates.comapPoint line 116
  11. def OAI.CampanaPeternellSix.ProjectiveCoordinates.comapContinuous line 121
  12. def OAI.CampanaPeternellSix.ProjectiveCoordinates.comapSectionFun line 131
  13. lemma OAI.CampanaPeternellSix.ProjectiveCoordinates.locallyFraction_comapSection line 136
  14. def OAI.CampanaPeternellSix.ProjectiveCoordinates.comapSections line 155
  15. def OAI.CampanaPeternellSix.ProjectiveCoordinates.projectiveSheafMap line 184
  16. lemma OAI.CampanaPeternellSix.ProjectiveCoordinates.germ_map_section line 197
  17. lemma OAI.CampanaPeternellSix.ProjectiveCoordinates.localRingMap_comp_stalkIso line 207
  18. lemma OAI.CampanaPeternellSix.ProjectiveCoordinates.isUnit_of_ringIso line 224
  19. def OAI.CampanaPeternellSix.ProjectiveCoordinates.projectiveMap line 229
  20. theorem OAI.CampanaPeternellSix.ProjectiveCoordinates.preimage_basicOpen line 244
  21. def OAI.CampanaPeternellSix.ProjectiveCoordinates.HasCoordinatePullback line 258
  22. theorem OAI.CampanaPeternellSix.ProjectiveCoordinates.degreeScalingProjMap line 270
  23. lemma OAI.CampanaPeternellSix.ProjectiveCoordinates.topIso_inv_appTop line 286
  24. lemma OAI.CampanaPeternellSix.ProjectiveCoordinates.toSpecZero_section line 302
  25. lemma OAI.CampanaPeternellSix.ProjectiveCoordinates.mapLocalRing_fromZero line 316
  26. abbrev OAI.CampanaPeternellSix.RelativePolynomialEvaluation.grading line 336
  27. def OAI.CampanaPeternellSix.RelativePolynomialEvaluation.space line 337
  28. def OAI.CampanaPeternellSix.RelativePolynomialEvaluation.constants line 338
  29. def OAI.CampanaPeternellSix.RelativePolynomialEvaluation.toBase line 344
  30. lemma OAI.CampanaPeternellSix.RelativePolynomialEvaluation.toBase_section line 348
  31. lemma OAI.CampanaPeternellSix.RelativePolynomialEvaluation.tuple_homogeneous line 361
  32. lemma OAI.CampanaPeternellSix.RelativePolynomialEvaluation.tuple_admissible line 367
  33. def OAI.CampanaPeternellSix.RelativePolynomialEvaluation.evaluation line 381
  34. lemma OAI.CampanaPeternellSix.RelativePolynomialEvaluation.evaluation_coordinates line 386
  35. lemma OAI.CampanaPeternellSix.RelativePolynomialEvaluation.evaluation_overBase line 399
  36. theorem OAI.CampanaPeternellSix.RelativePolynomialEvaluation.homogeneousTupleMap line 430