OAI/AlgebraicGeometry/CommutingDerivations/LocalizationSetup.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

The Laurent coefficient algebra and localization coordinates. The coefficient map is the lift of t ↦ F + 1.

  1. def OAI.AbhyankarSathaye.CommutingDerivations.ambientC line 18
  2. abbrev OAI.AbhyankarSathaye.CommutingDerivations.LocalizedAmbient line 19
  3. abbrev OAI.AbhyankarSathaye.CommutingDerivations.LaurentCoefficients line 20
  4. abbrev OAI.AbhyankarSathaye.CommutingDerivations.RelativePlane line 21
  5. def OAI.AbhyankarSathaye.CommutingDerivations.loc line 23
  6. def OAI.AbhyankarSathaye.CommutingDerivations.coefficientC line 24
  7. def OAI.AbhyankarSathaye.CommutingDerivations.coefficientD line 26
  8. def OAI.AbhyankarSathaye.CommutingDerivations.localD line 28
  9. theorem OAI.AbhyankarSathaye.CommutingDerivations.coefficient_unit line 30
  10. theorem OAI.AbhyankarSathaye.CommutingDerivations.local_unit line 33
  11. def OAI.AbhyankarSathaye.CommutingDerivations.polynomialCoefficientMap line 36
  12. def OAI.AbhyankarSathaye.CommutingDerivations.coefficientMap line 39
  13. theorem OAI.AbhyankarSathaye.CommutingDerivations.coefficientMap_C line 46
  14. theorem OAI.AbhyankarSathaye.CommutingDerivations.coefficientMap_D line 49
  15. def OAI.AbhyankarSathaye.CommutingDerivations.localAlpha line 58
  16. def OAI.AbhyankarSathaye.CommutingDerivations.localBeta line 59
  17. def OAI.AbhyankarSathaye.CommutingDerivations.localT line 61
  18. def OAI.AbhyankarSathaye.CommutingDerivations.localCoordinates line 62
  19. theorem OAI.AbhyankarSathaye.CommutingDerivations.local_cusp line 64
  20. theorem OAI.AbhyankarSathaye.CommutingDerivations.local_section line 67
  21. theorem OAI.AbhyankarSathaye.CommutingDerivations.local_bezout line 71
  22. theorem OAI.AbhyankarSathaye.CommutingDerivations.local_recover_s line 74
  23. def OAI.AbhyankarSathaye.CommutingDerivations.relativeBackward line 79

    Source documentation

    Evaluation at the displayed X,Y,T, with the explicit relative coefficient map.

    def relativeBackward : RelativePlane →+* LocalizedAmbient :=
…

    Mentions: OAI.AbhyankarSathaye.CommutingDerivations.RelativePlane, OAI.AbhyankarSathaye.CommutingDerivations.LocalizedAmbient

  24. theorem OAI.AbhyankarSathaye.CommutingDerivations.relativeBackward_C line 82
  25. theorem OAI.AbhyankarSathaye.CommutingDerivations.relativeBackward_X line 86
  26. def OAI.AbhyankarSathaye.CommutingDerivations.RelativeLocalizationContract line 92

    Source documentation

    A relative algebra equivalence over ℂ[c,c⁻¹], with c = F + 1, and its coordinate equations.

    def RelativeLocalizationContract : Prop :=
…