Localization preserves the square-zero deformation sequence

Mathlib constructs the localization of a left module over a left Ore set as OreLocalization S N. Applied to the opposite deformation ring, this is the localization of the original right module. This file proves directly on Ore fractions that the square-zero parameter remains exact. It also constructs the specialization map to the ordinary commutative localization of the special fibre and proves that its kernel is the same parameter image.

The results are not conditional localized-exactness interfaces: the localized module, parameter action, and specialization map are concrete constructions. The only typeclass parameter is Mathlib's OreSet; its existence for the pulled-back denominators is proved in SquareZeroOreLocalization.

@[reducible, inline]

abbrev Stafford38.Characteristic.SquareZeroLocalizedExactness.OppositeDenominators {k : Type u_k} {R : Type u_R} {B : Type u_B} {N : Type u_N} {G : Type u_G} [Field k] [CommRing R] [Algebra k R] [Ring B] [Algebra k B] [AddCommGroup N] [Module k N] [Module Bᵐᵒᵖ N] [SMulCommClass k Bᵐᵒᵖ N] [AddCommGroup G] [Module k G] [Module R G] (D : SquareZeroTraceData.RightSquareZeroTraceData k R B N G) (S : Submonoid R) : Submonoid Bᵐᵒᵖ

Denominators in the opposite deformation ring lying over S.

Equations

• Stafford38.Characteristic.SquareZeroLocalizedExactness.OppositeDenominators D S = Submonoid.comap (Stafford38.Characteristic.SquareZeroOreLocalization.oppositeSpecializationMonoidHom D) S

@[reducible, inline]

abbrev Stafford38.Characteristic.SquareZeroLocalizedExactness.LocalizedDeformationModule {k : Type u_k} {R : Type u_R} {B : Type u_B} {N : Type u_N} {G : Type u_G} [Field k] [CommRing R] [Algebra k R] [Ring B] [Algebra k B] [AddCommGroup N] [Module k N] [Module Bᵐᵒᵖ N] [SMulCommClass k Bᵐᵒᵖ N] [AddCommGroup G] [Module k G] [Module R G] (D : SquareZeroTraceData.RightSquareZeroTraceData k R B N G) (S : Submonoid R) [OreLocalization.OreSet (OppositeDenominators D S)] : Type (max u_B u_N)

The concrete localized opposite-ring module supplied by Mathlib's Ore localization construction.

Equations

• Stafford38.Characteristic.SquareZeroLocalizedExactness.LocalizedDeformationModule D S = OreLocalization (Stafford38.Characteristic.SquareZeroLocalizedExactness.OppositeDenominators D S) N

def Stafford38.Characteristic.SquareZeroLocalizedExactness.denominatorMap {k : Type u_k} {R : Type u_R} {B : Type u_B} {N : Type u_N} {G : Type u_G} [Field k] [CommRing R] [Algebra k R] [Ring B] [Algebra k B] [AddCommGroup N] [Module k N] [Module Bᵐᵒᵖ N] [SMulCommClass k Bᵐᵒᵖ N] [AddCommGroup G] [Module k G] [Module R G] (D : SquareZeroTraceData.RightSquareZeroTraceData k R B N G) (S : Submonoid R) : ↥(OppositeDenominators D S) →* ↥S

A pulled-back Ore denominator specializes to a denominator in S.

Equations

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

def Stafford38.Characteristic.SquareZeroLocalizedExactness.localizedCAct {k : Type u_k} {R : Type u_R} {B : Type u_B} {N : Type u_N} {G : Type u_G} [Field k] [CommRing R] [Algebra k R] [Ring B] [Algebra k B] [AddCommGroup N] [Module k N] [Module Bᵐᵒᵖ N] [SMulCommClass k Bᵐᵒᵖ N] [AddCommGroup G] [Module k G] [Module R G] (D : SquareZeroTraceData.RightSquareZeroTraceData k R B N G) (S : Submonoid R) [OreLocalization.OreSet (OppositeDenominators D S)] : LocalizedDeformationModule D S →+ LocalizedDeformationModule D S

Action of the square-zero parameter on the localized module. It is the original opposite-ring action, extended by the Ore localization module construction.

Equations

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

@[simp]

theorem Stafford38.Characteristic.SquareZeroLocalizedExactness.localizedCAct_apply {k : Type u_k} {R : Type u_R} {B : Type u_B} {N : Type u_N} {G : Type u_G} [Field k] [CommRing R] [Algebra k R] [Ring B] [Algebra k B] [AddCommGroup N] [Module k N] [Module Bᵐᵒᵖ N] [SMulCommClass k Bᵐᵒᵖ N] [AddCommGroup G] [Module k G] [Module R G] (D : SquareZeroTraceData.RightSquareZeroTraceData k R B N G) (S : Submonoid R) [OreLocalization.OreSet (OppositeDenominators D S)] (x : LocalizedDeformationModule D S) : (localizedCAct D S) x = MulOpposite.op D.c • x

theorem Stafford38.Characteristic.SquareZeroLocalizedExactness.localizedCAct_oreDiv {k : Type u_k} {R : Type u_R} {B : Type u_B} {N : Type u_N} {G : Type u_G} [Field k] [CommRing R] [Algebra k R] [Ring B] [Algebra k B] [AddCommGroup N] [Module k N] [Module Bᵐᵒᵖ N] [SMulCommClass k Bᵐᵒᵖ N] [AddCommGroup G] [Module k G] [Module R G] (D : SquareZeroTraceData.RightSquareZeroTraceData k R B N G) (S : Submonoid R) [OreLocalization.OreSet (OppositeDenominators D S)] (m : N) (s : ↥(OppositeDenominators D S)) : (localizedCAct D S) (m /ₒ s) = MulOpposite.op D.c • m /ₒ s

On a displayed Ore fraction, the localized parameter acts on its numerator without changing its denominator.

theorem Stafford38.Characteristic.SquareZeroLocalizedExactness.localizedCAct_sq_eq_zero {k : Type u_k} {R : Type u_R} {B : Type u_B} {N : Type u_N} {G : Type u_G} [Field k] [CommRing R] [Algebra k R] [Ring B] [Algebra k B] [AddCommGroup N] [Module k N] [Module Bᵐᵒᵖ N] [SMulCommClass k Bᵐᵒᵖ N] [AddCommGroup G] [Module k G] [Module R G] (D : SquareZeroTraceData.RightSquareZeroTraceData k R B N G) (S : Submonoid R) [OreLocalization.OreSet (OppositeDenominators D S)] (x : LocalizedDeformationModule D S) : (localizedCAct D S) ((localizedCAct D S) x) = 0

The localized parameter still squares to zero.

theorem Stafford38.Characteristic.SquareZeroLocalizedExactness.localizedCAct_ker_eq_range {k : Type u_k} {R : Type u_R} {B : Type u_B} {N : Type u_N} {G : Type u_G} [Field k] [CommRing R] [Algebra k R] [Ring B] [Algebra k B] [AddCommGroup N] [Module k N] [Module Bᵐᵒᵖ N] [SMulCommClass k Bᵐᵒᵖ N] [AddCommGroup G] [Module k G] [Module R G] (D : SquareZeroTraceData.RightSquareZeroTraceData k R B N G) (S : Submonoid R) [OreLocalization.OreSet (OppositeDenominators D S)] : (localizedCAct D S).ker = (localizedCAct D S).range

Ore localization preserves the exact square-zero parameter sequence: the kernel of multiplication by c remains its image.

def Stafford38.Characteristic.SquareZeroLocalizedExactness.localizedSpecializationFun {k : Type u_k} {R : Type u_R} {B : Type u_B} {N : Type u_N} {G : Type u_G} [Field k] [CommRing R] [Algebra k R] [Ring B] [Algebra k B] [AddCommGroup N] [Module k N] [Module Bᵐᵒᵖ N] [SMulCommClass k Bᵐᵒᵖ N] [AddCommGroup G] [Module k G] [Module R G] (D : SquareZeroTraceData.RightSquareZeroTraceData k R B N G) (S : Submonoid R) [OreLocalization.OreSet (OppositeDenominators D S)] : LocalizedDeformationModule D S → LocalizedModule S G

Specialization of an Ore-localized deformation fraction to the ordinary commutative localization of the special fibre.

Equations

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

@[simp]

theorem Stafford38.Characteristic.SquareZeroLocalizedExactness.localizedSpecializationFun_oreDiv {k : Type u_k} {R : Type u_R} {B : Type u_B} {N : Type u_N} {G : Type u_G} [Field k] [CommRing R] [Algebra k R] [Ring B] [Algebra k B] [AddCommGroup N] [Module k N] [Module Bᵐᵒᵖ N] [SMulCommClass k Bᵐᵒᵖ N] [AddCommGroup G] [Module k G] [Module R G] (D : SquareZeroTraceData.RightSquareZeroTraceData k R B N G) (S : Submonoid R) [OreLocalization.OreSet (OppositeDenominators D S)] (m : N) (s : ↥(OppositeDenominators D S)) : localizedSpecializationFun D S (m /ₒ s) = LocalizedModule.mk (D.rho m) ((denominatorMap D S) s)

def Stafford38.Characteristic.SquareZeroLocalizedExactness.localizedSpecialization {k : Type u_k} {R : Type u_R} {B : Type u_B} {N : Type u_N} {G : Type u_G} [Field k] [CommRing R] [Algebra k R] [Ring B] [Algebra k B] [AddCommGroup N] [Module k N] [Module Bᵐᵒᵖ N] [SMulCommClass k Bᵐᵒᵖ N] [AddCommGroup G] [Module k G] [Module R G] (D : SquareZeroTraceData.RightSquareZeroTraceData k R B N G) (S : Submonoid R) [OreLocalization.OreSet (OppositeDenominators D S)] : LocalizedDeformationModule D S →+ LocalizedModule S G

The localized specialization is an additive homomorphism.

Equations

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

@[simp]

theorem Stafford38.Characteristic.SquareZeroLocalizedExactness.localizedSpecialization_apply {k : Type u_k} {R : Type u_R} {B : Type u_B} {N : Type u_N} {G : Type u_G} [Field k] [CommRing R] [Algebra k R] [Ring B] [Algebra k B] [AddCommGroup N] [Module k N] [Module Bᵐᵒᵖ N] [SMulCommClass k Bᵐᵒᵖ N] [AddCommGroup G] [Module k G] [Module R G] (D : SquareZeroTraceData.RightSquareZeroTraceData k R B N G) (S : Submonoid R) [OreLocalization.OreSet (OppositeDenominators D S)] (x : LocalizedDeformationModule D S) : (localizedSpecialization D S) x = localizedSpecializationFun D S x

theorem Stafford38.Characteristic.SquareZeroLocalizedExactness.localizedSpecialization_surjective {k : Type u_k} {R : Type u_R} {B : Type u_B} {N : Type u_N} {G : Type u_G} [Field k] [CommRing R] [Algebra k R] [Ring B] [Algebra k B] [AddCommGroup N] [Module k N] [Module Bᵐᵒᵖ N] [SMulCommClass k Bᵐᵒᵖ N] [AddCommGroup G] [Module k G] [Module R G] (D : SquareZeroTraceData.RightSquareZeroTraceData k R B N G) (S : Submonoid R) [OreLocalization.OreSet (OppositeDenominators D S)] : Function.Surjective ⇑(localizedSpecialization D S)

Specialization remains surjective after localization. A commutative denominator is lifted through the surjective deformation specialization.

theorem Stafford38.Characteristic.SquareZeroLocalizedExactness.localizedSpecialization_localizedCAct_eq_zero {k : Type u_k} {R : Type u_R} {B : Type u_B} {N : Type u_N} {G : Type u_G} [Field k] [CommRing R] [Algebra k R] [Ring B] [Algebra k B] [AddCommGroup N] [Module k N] [Module Bᵐᵒᵖ N] [SMulCommClass k Bᵐᵒᵖ N] [AddCommGroup G] [Module k G] [Module R G] (D : SquareZeroTraceData.RightSquareZeroTraceData k R B N G) (S : Submonoid R) [OreLocalization.OreSet (OppositeDenominators D S)] (x : LocalizedDeformationModule D S) : (localizedSpecialization D S) ((localizedCAct D S) x) = 0

The localized specialization kills the localized parameter image.

theorem Stafford38.Characteristic.SquareZeroLocalizedExactness.localizedSpecialization_ker_eq_range {k : Type u_k} {R : Type u_R} {B : Type u_B} {N : Type u_N} {G : Type u_G} [Field k] [CommRing R] [Algebra k R] [Ring B] [Algebra k B] [AddCommGroup N] [Module k N] [Module Bᵐᵒᵖ N] [SMulCommClass k Bᵐᵒᵖ N] [AddCommGroup G] [Module k G] [Module R G] (D : SquareZeroTraceData.RightSquareZeroTraceData k R B N G) (S : Submonoid R) [OreLocalization.OreSet (OppositeDenominators D S)] : (localizedSpecialization D S).ker = (localizedCAct D S).range

The specialization kernel after Ore localization is exactly the image of the localized square-zero parameter.

noncomputable def Stafford38.Characteristic.SquareZeroLocalizedExactness.localizedSpecialFibreAddEquiv {k : Type u_k} {R : Type u_R} {B : Type u_B} {N : Type u_N} {G : Type u_G} [Field k] [CommRing R] [Algebra k R] [Ring B] [Algebra k B] [AddCommGroup N] [Module k N] [Module Bᵐᵒᵖ N] [SMulCommClass k Bᵐᵒᵖ N] [AddCommGroup G] [Module k G] [Module R G] (D : SquareZeroTraceData.RightSquareZeroTraceData k R B N G) (S : Submonoid R) [OreLocalization.OreSet (OppositeDenominators D S)] : LocalizedDeformationModule D S ⧸ (localizedCAct D S).range ≃+ LocalizedModule S G

Quotienting the localized deformation module by the parameter image gives the ordinary commutative localization of the special fibre.

Equations

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

theorem Stafford38.Characteristic.SquareZeroLocalizedExactness.localized_squareZero_exactness {k : Type u_k} {R : Type u_R} {B : Type u_B} {N : Type u_N} {G : Type u_G} [Field k] [CommRing R] [Algebra k R] [Ring B] [Algebra k B] [AddCommGroup N] [Module k N] [Module Bᵐᵒᵖ N] [SMulCommClass k Bᵐᵒᵖ N] [AddCommGroup G] [Module k G] [Module R G] (D : SquareZeroTraceData.RightSquareZeroTraceData k R B N G) (S : Submonoid R) [OreLocalization.OreSet (OppositeDenominators D S)] : (localizedCAct D S).ker = (localizedCAct D S).range ∧ Function.Surjective ⇑(localizedSpecialization D S) ∧ (localizedSpecialization D S).ker = (localizedCAct D S).range

The complete localized exactness package needed by the local trace argument: both parameter exactness and specialization exactness hold, and the specialization is onto the ordinary localized special fibre.

def Stafford38.Characteristic.SquareZeroLocalizedExactness.LocalizedExactnessFor {k : Type u_k} {R : Type u_R} {B : Type u_B} {N : Type u_N} {G : Type u_G} [Field k] [CommRing R] [Algebra k R] [Ring B] [Algebra k B] [AddCommGroup N] [Module k N] [Module Bᵐᵒᵖ N] [SMulCommClass k Bᵐᵒᵖ N] [AddCommGroup G] [Module k G] [Module R G] (D : SquareZeroTraceData.RightSquareZeroTraceData k R B N G) (S : Submonoid R) (h : OreLocalization.OreSet (OppositeDenominators D S)) : Prop

Exactness for one explicit choice of Mathlib's pulled-back Ore-set structure. This packages only already constructed maps and equations.

Equations

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

theorem Stafford38.Characteristic.SquareZeroLocalizedExactness.exists_localizedExactnessFor {k : Type u_k} {R : Type u_R} {B : Type u_B} {N : Type u_N} {G : Type u_G} [Field k] [CommRing R] [Algebra k R] [Ring B] [Algebra k B] [AddCommGroup N] [Module k N] [Module Bᵐᵒᵖ N] [SMulCommClass k Bᵐᵒᵖ N] [AddCommGroup G] [Module k G] [Module R G] (D : SquareZeroTraceData.RightSquareZeroTraceData k R B N G) (S : Submonoid R) : ∃ (h : OreLocalization.OreSet (OppositeDenominators D S)), LocalizedExactnessFor D S h

The Ore-set existence theorem and the fraction-level exactness proof together produce a genuine localized deformation sequence for every multiplicative set in the special fibre.

theorem Stafford38.Characteristic.SquareZeroLocalizedExactness.exists_minimalPrimeLocalizedExactnessAndFiniteLength {k : Type u_k} {R : Type u_R} {B : Type u_B} {N : Type u_N} {G : Type u_G} [Field k] [CommRing R] [Algebra k R] [Ring B] [Algebra k B] [AddCommGroup N] [Module k N] [Module Bᵐᵒᵖ N] [SMulCommClass k Bᵐᵒᵖ N] [AddCommGroup G] [Module k G] [Module R G] (D : SquareZeroTraceData.RightSquareZeroTraceData k R B N G) [IsNoetherianRing R] [Module.Finite R G] (P : Ideal R) [P.IsPrime] (hP : P ∈ (Module.annihilator R G).minimalPrimes) : ∃ (h : OreLocalization.OreSet (OppositeDenominators D P.primeCompl)), LocalizedExactnessFor D P.primeCompl h ∧ Nontrivial (LocalizedModule P.primeCompl G) ∧ IsFiniteLength (Localization P.primeCompl) (LocalizedModule P.primeCompl G)

At a minimal prime over the special-fibre annihilator, the localized deformation exact sequence exists and its commutative special fibre is simultaneously nonzero and of finite length.

theorem Stafford38.CharacteristicConcreteSquareZeroTraceData.exists_primeLocalizedExactness (k : Type u) [Field k] {n : ℕ} (I : EulerSurjectivity.RightIdeal (WeylIteratedEquivalence.PresentedWeyl k n)) (P : Ideal (Characteristic.SymbolRing k n)) [P.IsPrime] : ∃ (h : OreLocalization.OreSet (Characteristic.SquareZeroLocalizedExactness.OppositeDenominators (filteredQuotientTwoJetTraceData k I) P.primeCompl)), Characteristic.SquareZeroLocalizedExactness.LocalizedExactnessFor (filteredQuotientTwoJetTraceData k I) P.primeCompl h

The concrete filtered Weyl two-jet admits a localized exact deformation sequence at every prime of its commutative symbol ring.