Cotangent spaces and localization at a maximal ideal

Let p be a maximal ideal of a commutative ring R, and let Rₚ be a localization of R at p. The map from R to Rₚ identifies the cotangent space p / p² with the cotangent space pRₚ / (pRₚ)² of the local ring Rₚ. This file constructs that identification and proves that it is semilinear for the canonical equivalence between the two residue fields.

This is the localization bridge needed to compare the augmentation-ideal model of the tangent space of an affine group with the Zariski tangent space of its spectrum at the identity. That comparison is a prerequisite for the smoothness and dimension tools in Layer 2 of the ReductiveGroups roadmap.

Main declarations

• Ideal.cotangentLocalizationEquiv: localization at a maximal ideal preserves the cotangent space.
• Ideal.cotangentLocalizationEquiv_smul: the equivalence is semilinear for the canonical residue-field equivalence.

References

• J. S. Milne, Algebraic Groups (2017), §10.a.

noncomputable def Ideal.cotangentLocalizationEquiv {R : Type u_1} {Rₚ : Type u_2} [CommRing R] (p : Ideal R) [p.IsMaximal] [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] : p.Cotangent ≃ₗ[R] (IsLocalRing.maximalIdeal Rₚ).Cotangent

The canonical linear equivalence p / p² ≃ pRₚ / (pRₚ)² induced by localization.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Ideal.cotangentLocalizationEquiv_toCotangent {R : Type u_1} {Rₚ : Type u_2} [CommRing R] (p : Ideal R) [p.IsMaximal] [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] (x : ↥p) : p.cotangentLocalizationEquiv (p.toCotangent x) = (IsLocalRing.maximalIdeal Rₚ).toCotangent ⟨(algebraMap R Rₚ) ↑x, ⋯⟩

On a class represented by x ∈ p, the cotangent localization equivalence is induced by the ring localization map.

@[simp]

theorem Ideal.cotangentLocalizationEquiv_smul {R : Type u_1} {Rₚ : Type u_2} [CommRing R] (p : Ideal R) [p.IsMaximal] [CommRing Rₚ] [Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] (r : R ⧸ p) (x : p.Cotangent) : p.cotangentLocalizationEquiv (r • x) = (IsLocalization.AtPrime.equivQuotMaximalIdeal p Rₚ) r • p.cotangentLocalizationEquiv x

The cotangent localization equivalence is semilinear for the canonical equivalence between the residue field R / p and the residue field of Rₚ.