OAI/AlgebraicGeometry/CommutingDerivations/LocalizationEquivalence.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Explicit maps between the ambient localization and the polynomial algebra over Laurent coefficients, using the unrestricted reconstruction formulas.

  1. def OAI.AbhyankarSathaye.CommutingDerivations.ambientToFree line 14
  2. theorem OAI.AbhyankarSathaye.CommutingDerivations.ambientToFree_constant line 18
  3. theorem OAI.AbhyankarSathaye.CommutingDerivations.ambientToFree_h line 22
  4. theorem OAI.AbhyankarSathaye.CommutingDerivations.ambientToFree_u line 25
  5. theorem OAI.AbhyankarSathaye.CommutingDerivations.ambientToFree_v line 28
  6. theorem OAI.AbhyankarSathaye.CommutingDerivations.ambientToFree_w line 31
  7. theorem OAI.AbhyankarSathaye.CommutingDerivations.ambientToFree_x line 34
  8. theorem OAI.AbhyankarSathaye.CommutingDerivations.ambientToFree_y line 36
  9. theorem OAI.AbhyankarSathaye.CommutingDerivations.ambientToFree_s line 38
  10. theorem OAI.AbhyankarSathaye.CommutingDerivations.ambientToFree_c line 41
  11. theorem OAI.AbhyankarSathaye.CommutingDerivations.ambientToFree_shiftX line 44
  12. theorem OAI.AbhyankarSathaye.CommutingDerivations.ambientToFree_shiftY line 46
  13. theorem OAI.AbhyankarSathaye.CommutingDerivations.coefficientMap_complex line 49
  14. def OAI.AbhyankarSathaye.CommutingDerivations.relativeForward line 56
  15. theorem OAI.AbhyankarSathaye.CommutingDerivations.relativeForward_loc line 62
  16. theorem OAI.AbhyankarSathaye.CommutingDerivations.relativeForward_coefficientMap line 65
  17. theorem OAI.AbhyankarSathaye.CommutingDerivations.relativeForward_coefficient line 75
  18. theorem OAI.AbhyankarSathaye.CommutingDerivations.relativeForward_d line 79
  19. theorem OAI.AbhyankarSathaye.CommutingDerivations.relativeForward_alpha line 82
  20. theorem OAI.AbhyankarSathaye.CommutingDerivations.relativeForward_beta line 85
  21. theorem OAI.AbhyankarSathaye.CommutingDerivations.relativeForward_shiftX line 89
  22. theorem OAI.AbhyankarSathaye.CommutingDerivations.relativeForward_shiftY line 91
  23. theorem OAI.AbhyankarSathaye.CommutingDerivations.relativeForward_T line 93
  24. theorem OAI.AbhyankarSathaye.CommutingDerivations.relativeForward_backward line 104
  25. theorem OAI.AbhyankarSathaye.CommutingDerivations.relativeBackward_freeS line 112
  26. theorem OAI.AbhyankarSathaye.CommutingDerivations.relativeBackward_freeX line 115
  27. theorem OAI.AbhyankarSathaye.CommutingDerivations.relativeBackward_freeY line 118
  28. theorem OAI.AbhyankarSathaye.CommutingDerivations.relativeBackward_freeH line 121
  29. theorem OAI.AbhyankarSathaye.CommutingDerivations.relativeBackward_freeAlpha line 124
  30. theorem OAI.AbhyankarSathaye.CommutingDerivations.relativeBackward_freeBeta line 127
  31. theorem OAI.AbhyankarSathaye.CommutingDerivations.relativeBackward_free_original line 131
  32. theorem OAI.AbhyankarSathaye.CommutingDerivations.relativeBackward_forward line 142
  33. def OAI.AbhyankarSathaye.CommutingDerivations.localizationRingEquiv line 167

    Source documentation

    Actual localized ring equivalence, with explicit maps and both composites.

    def localizationRingEquiv : LocalizedAmbient ≃+* RelativePlane :=
…

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

  34. def OAI.AbhyankarSathaye.CommutingDerivations.relativeAlgebra line 173

    Source documentation

    The algebra structure is exactly the specified map c ↦ F+1.

    def relativeAlgebra : Algebra LaurentCoefficients LocalizedAmbient := coefficientMap.toAlgebra

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

  35. def OAI.AbhyankarSathaye.CommutingDerivations.localizationEquiv line 176

    Source documentation

    Actual equivalence over the Laurent coefficient ring.

    def localizationEquiv :
    letI := relativeAlgebra
…

    Mentions: OAI.AbhyankarSathaye.CommutingDerivations.relativeAlgebra

  36. def OAI.AbhyankarSathaye.CommutingDerivations.localizationComplexEquiv line 184

    Source documentation

    The same explicit equivalence also preserves the original complex scalars.

    def localizationComplexEquiv : LocalizedAmbient ≃ₐ[ℂ] RelativePlane :=
…

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

  37. theorem OAI.AbhyankarSathaye.CommutingDerivations.relativeLocalizationContract_proved line 194