Transport of Stafford certificates

The right-ideal certificate is 1 = e * R + F * e * S. This module supplies the generic conditional reduction from monicization and an exponent hypothesis, together with transport through algebra automorphisms and nonzero scalars. These conditional interfaces are retained for current imports; the unconditional theorem is proved in Stafford38.FoundationClosure.

def Stafford.Reduction.ad {A : Type u_2} [Ring A] (Y u : A) : A

The commutator ad Y u = Y * u - u * Y.

Equations

• Stafford.Reduction.ad Y u = Y * u - u * Y

def Stafford.Reduction.Stafford38 {A : Type u_2} [Ring A] (e : A) : Prop

Stafford 3.8 for a single element, in written operator order.

Equations

• Stafford.Reduction.Stafford38 e = ∃ (F : A) (R : A) (S : A), 1 = e * R + F * e * S

def Stafford.Reduction.monicElt {A : Type u_2} [Ring A] (X : A) (N : ℕ) (β : Fin N → A) : A

The monic right-coefficient presentation X ^ N + ∑_{i<N} X ^ i * β i.

Equations

• Stafford.Reduction.monicElt X N β = X ^ N + ∑ i : Fin N, X ^ ↑i * β i

def Stafford.Reduction.WeylMonic {A : Type u_2} [Ring A] (e : A) : Prop

e is Weyl-monic if some Weyl pair presents it monically with all coefficients commuting with the partner.

Equations

• Stafford.Reduction.WeylMonic e = ∃ (X : A) (Y : A) (N : ℕ) (β : Fin N → A), Stafford.Reduction.ad Y X = 1 ∧ (∀ (i : Fin N), Commute Y (β i)) ∧ e = Stafford.Reduction.monicElt X N β

Transport lemmas

theorem Stafford.Reduction.stafford38_of_ringEquiv {A : Type u_2} [Ring A] (φ : A ≃+* A) {e : A} (h : Stafford38 (φ e)) : Stafford38 e

Stafford 3.8 transports along any ring automorphism.

theorem Stafford.Reduction.stafford38_smul {k : Type u_1} {A : Type u_2} [Field k] [Ring A] [Algebra k A] (c : k) {e : A} (h : Stafford38 (c • e)) : Stafford38 e

Stafford 3.8 transports along scalar multiples (no nonvanishing needed: the scalar is absorbed into the cofactors R and S).

theorem Stafford.Reduction.stafford38_of_power {A : Type u_2} [Ring A] {e Y : A} {s : ℕ} {R S : A} (h : 1 = e * R + Y ^ s * e * S) : Stafford38 e

A cofactor of the special form Y ^ s already witnesses Stafford 3.8.

The two hypotheses

def Stafford.Reduction.Monicization (k : Type u_3) (A : Type u_4) [Field k] [Ring A] [Algebra k A] : Prop

Hypothesis M (monicization). Every nonzero element is, after an algebra automorphism and a nonzero scalar, Weyl-monic.

Equations

• Stafford.Reduction.Monicization k A = ∀ (e : A), e ≠ 0 → ∃ (φ : A ≃ₐ[k] A) (c : k), c ≠ 0 ∧ Stafford.Reduction.WeylMonic (c • φ e)

def Stafford.Reduction.ExponentHypothesis (A : Type u_3) [Ring A] : Prop

Hypothesis E (exponent). For every Weyl-monic presentation some power of the Weyl partner is a Stafford cofactor.

Equations

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

The reduction

theorem Stafford.Reduction.stafford38_of_weylMonic {A : Type u_2} [Ring A] (hE : ExponentHypothesis A) {e : A} (he : WeylMonic e) : Stafford38 e

Hypothesis E gives Stafford 3.8 for every Weyl-monic element.

theorem Stafford.Reduction.stafford38_of_hypotheses {k : Type u_1} {A : Type u_2} [Field k] [Ring A] [Algebra k A] (hM : Monicization k A) (hE : ExponentHypothesis A) (e : A) : e ≠ 0 → Stafford38 e

Stafford 3.8 from the two named hypotheses.

If every nonzero element monicizes (Hypothesis M) and every Weyl-monic element admits a cofactor that is a power of the Weyl partner (Hypothesis E), then

∀ e ≠ 0, ∃ F R S, 1 = e * R + F * e * S.