OAI/AlgebraicGeometry/CommutingDerivations/ExtendedLocalization.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Localization coordinates in every dimension n ≥ 4.

The localization at extendedF hn + 1 is a polynomial extension of the four-dimensional localization, with an explicit structural map from the ambient ring.

  1. abbrev OAI.AbhyankarSathaye.CommutingDerivations.ExtendedLocalizedAmbient line 17
  2. def OAI.AbhyankarSathaye.CommutingDerivations.extendedLocAlgHom line 19
  3. def OAI.AbhyankarSathaye.CommutingDerivations.extendedLocMap line 24
  4. def OAI.AbhyankarSathaye.CommutingDerivations.extendedAlgebra line 29
  5. theorem OAI.AbhyankarSathaye.CommutingDerivations.extendedScalarTower line 33
  6. theorem OAI.AbhyankarSathaye.CommutingDerivations.extendedLocMap_c line 38
  7. theorem OAI.AbhyankarSathaye.CommutingDerivations.extended_isLocalization line 47

    Source documentation

    This polynomial extension is the localization of the exact full ambient ring at the powers of extendedF+1, with the displayed structural map.

    theorem extended_isLocalization {n : ℕ} (hn : 4 ≤ n) :
    letI := extendedAlgebra hn
…

    Mentions: OAI.AbhyankarSathaye.CommutingDerivations.extendedAlgebra

  8. def OAI.AbhyankarSathaye.CommutingDerivations.extendedCoefficientMap line 62
  9. def OAI.AbhyankarSathaye.CommutingDerivations.extendedLocalizationEquiv line 67

    Source documentation

    Complex-linear localization coordinates, with exactly n−1 independent polynomial variables and the original Laurent coefficient ring.

    def extendedLocalizationEquiv {n : ℕ} (hn : 4 ≤ n) :
    ExtendedLocalizedAmbient n ≃ₐ[ℂ] MvPolynomial (Fin (n-1)) LaurentCoefficients :=
…

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

  10. theorem OAI.AbhyankarSathaye.CommutingDerivations.extendedLocalizationEquiv_coefficient line 73
  11. theorem OAI.AbhyankarSathaye.CommutingDerivations.extendedLocalizationEquiv_c line 87
  12. def OAI.AbhyankarSathaye.CommutingDerivations.extendedRelativeAlgebra line 93
  13. def OAI.AbhyankarSathaye.CommutingDerivations.extendedRelativeLocalizationEquiv line 99

    Source documentation

    The all-dimensional equivalence fixes precisely the specified Laurent coefficient map, as an actual relative algebra equivalence.

    def extendedRelativeLocalizationEquiv {n : ℕ} (hn : 4 ≤ n) :
    letI := extendedRelativeAlgebra n
…

    Mentions: OAI.AbhyankarSathaye.CommutingDerivations.extendedRelativeAlgebra