Annihilator closure from a square-zero deformation

The exact parameter sequence already forces the annihilator of the special fibre to be closed under the recorded first-order bracket. The proof uses only right-action order, centrality and square-zero exactness; no localization, trace, finiteness or commutative-algebra hypothesis beyond the existing commutative special fibre is needed.

This proves closure only when both bracket inputs lie in the annihilator itself. It does not prove bracket closure of its radical or of any prime ideal for inputs that merely lie in that larger ideal.

theorem Stafford38.Characteristic.SquareZeroAnnihilatorBracket.rightAction_mem_range_cAct_of_pi_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) {a : B} (ha : D.pi a ∈ Module.annihilator R G) (m : N) : MulOpposite.op a • m ∈ D.cAct.range

If the specialization of a annihilates G, right multiplication by a on the deformation module lands in the image of the parameter action.

theorem Stafford38.Characteristic.SquareZeroAnnihilatorBracket.rightAction_cAct_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) (a : B) (m : N) : MulOpposite.op a • D.cAct m = D.cAct (MulOpposite.op a • m)

Centrality of the parameter lets every right action pass through its recorded action on N.

theorem Stafford38.Characteristic.SquareZeroAnnihilatorBracket.iterated_rightAction_eq_zero_of_pi_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) {a b : B} (ha : D.pi a ∈ Module.annihilator R G) (hb : D.pi b ∈ Module.annihilator R G) (m : N) : MulOpposite.op b • MulOpposite.op a • m = 0

Two successive right actions vanish when both specializations annihilate the special fibre. The displayed order is literal: first a, then b.

theorem Stafford38.Characteristic.SquareZeroAnnihilatorBracket.commutator_rightAction_eq_zero_of_pi_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) {a b : B} (ha : D.pi a ∈ Module.annihilator R G) (hb : D.pi b ∈ Module.annihilator R G) (m : N) : MulOpposite.op (Stafford.commutator a b) • m = 0

Consequently the right action of the deformation-ring commutator vanishes. The reversal [R_b,R_a] = R_[a,b] is explicit.

theorem Stafford38.Characteristic.SquareZeroAnnihilatorBracket.rho_rightAction_eq_zero_of_commutator_factor {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) {a b z : B} (ha : D.pi a ∈ Module.annihilator R G) (hb : D.pi b ∈ Module.annihilator R G) (hz : Stafford.commutator a b = D.c * z) (m : N) : D.rho (MulOpposite.op z • m) = 0

If [a,b]=c*z, then the quotient z acts trivially after module specialization. The explicit left factor c*z is essential here: centrality moves it to the right-module order needed by cAct.

theorem Stafford38.Characteristic.SquareZeroAnnihilatorBracket.bracket_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) {x y : R} (hx : x ∈ Module.annihilator R G) (hy : y ∈ Module.annihilator R G) : (D.bracket x) y ∈ Module.annihilator R G

The recorded bracket preserves the annihilator of the special fibre in both inputs.