Localized high-power two-block vanishing

This file discharges the elementwise two-block condition in the concrete right-Rees Artinian adapter. A localized scalar whose specialization lies in an annihilating ideal sends every deformation vector into the parameter image. Two such scalar actions therefore produce two parameter factors and vanish by square-zero.

The opposite localization acts on the left in the order corresponding to written right multiplication. The finite sum below consequently retains the displayed product order. No residue-field action is placed on the deformation module.

theorem Stafford38.Characteristic.LocalizedHighPowerTwoBlockVanishing.localizedParameter_comm {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 (SquareZeroLocalizedExactness.OppositeDenominators D S)] (a : OreLocalization (SquareZeroLocalizedExactness.OppositeDenominators D S) Bᵐᵒᵖ) : OreLocalization.numeratorRingHom (MulOpposite.op D.c) * a = a * OreLocalization.numeratorRingHom (MulOpposite.op D.c)

The central deformation parameter remains central after Ore localization. The multiplication is in the opposite ring, hence represents written right multiplication in the original deformation ring.

theorem Stafford38.Characteristic.LocalizedHighPowerTwoBlockVanishing.smul_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 (SquareZeroLocalizedExactness.OppositeDenominators D S)] (a : OreLocalization (SquareZeroLocalizedExactness.OppositeDenominators D S) Bᵐᵒᵖ) (z : SquareZeroLocalizedExactness.LocalizedDeformationModule D S) : a • (SquareZeroLocalizedExactness.localizedCAct D S) z = (SquareZeroLocalizedExactness.localizedCAct D S) (a • z)

A localized scalar action commutes with the concrete parameter action. This is the bridge that permits the two high-power blocks to contribute two successive parameter factors.

theorem Stafford38.Characteristic.LocalizedHighPowerTwoBlockVanishing.smul_mem_parameterRange_of_specialization_mem_annihilator {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 (SquareZeroLocalizedExactness.OppositeDenominators D S)] (a : OreLocalization (SquareZeroLocalizedExactness.OppositeDenominators D S) Bᵐᵒᵖ) (ha : (SquareZeroLocalizedRing.localizedOppositeSpecialization D S) a ∈ Module.annihilator (Localization S) (LocalizedModule S G)) (z : SquareZeroLocalizedExactness.LocalizedDeformationModule D S) : a • z ∈ (SquareZeroLocalizedExactness.localizedCAct D S).range

If the specialization of a localized scalar lies in an ideal annihilating the special fibre, then its action on every deformation vector is a localized parameter multiple.

theorem Stafford38.Characteristic.LocalizedHighPowerTwoBlockVanishing.product_smul_eq_zero_of_specializations_mem_annihilator {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 (SquareZeroLocalizedExactness.OppositeDenominators D S)] (a b : OreLocalization (SquareZeroLocalizedExactness.OppositeDenominators D S) Bᵐᵒᵖ) (ha : (SquareZeroLocalizedRing.localizedOppositeSpecialization D S) a ∈ Module.annihilator (Localization S) (LocalizedModule S G)) (hb : (SquareZeroLocalizedRing.localizedOppositeSpecialization D S) b ∈ Module.annihilator (Localization S) (LocalizedModule S G)) (z : SquareZeroLocalizedExactness.LocalizedDeformationModule D S) : (a * b) • z = 0

Two localized factors whose specializations lie in one annihilating ideal act successively by zero.

theorem Stafford38.Characteristic.LocalizedHighPowerTwoBlockVanishing.localizedHighPowerTwoBlockVanishing_of_annihilatingPower {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 (SquareZeroLocalizedExactness.OppositeDenominators D S)] [IsLocalRing (Localization S)] (q : ℕ) (hpow : IsLocalRing.maximalIdeal (Localization S) ^ q ≤ Module.annihilator (Localization S) (LocalizedModule S G)) : RightReesArtinianAdapter.LocalizedHighPowerTwoBlockVanishing D S q

An annihilating maximal-ideal power supplies the exact two-block vanishing proposition required by RightReesArtinianAdapter.