Documentation

GQ2.Roe.Devissage.LESExact

§5.11 dévissage on the r_R spine: exactness of the nine-term LES #

Mechanical R-spine clone of GQ2/Devissage/LESExact.lean (campaign decision, docs/orchestration/roe-r20-recon.md); proofs ported verbatim. Spine renames Z1w → Z1wR, H1w → H1wR, H2w → H2wR, d1Fun → d1FunR, d1 → d1R, mixedB → mixedB_R, WildRel → WildRelR, IsSelfDual(W) → IsSelfDual(W)_R, with R-suffixed public names. The relator-free H0w_exact_mid is reused from GQ2.Devissage.LESExact, never cloned.

Exactness of the nine-term LES #

Each spot is stated as y ∈ ker(out) ↔ y ∈ range(in) (equivalently at the ends, injectivity / surjectivity), the usual snake-lemma bookkeeping.

source
theorem GQ2.FoxH.H2wMap_g_surjective_R {C : Type u_1} [Group C] {A : Type u_3} {A'' : Type u_4} [AddCommGroup A] [DistribMulAction C A] [Finite A] [AddCommGroup A''] [DistribMulAction C A''] [Finite A''] [Finite C] (g : A →+ A'') (hg : ∀ (c : C) (a : A), g (c • a) = c • g a) (hsurj : Function.Surjective ⇑g) (t : Marking C) :
Function.Surjective ⇑(H2wMap_R t g hg)

Exactness at the right end: H²wMap g is surjective.

source
theorem GQ2.FoxH.H2w_exact_mid_R {C : Type u_1} [Group C] {A' : Type u_2} {A : Type u_3} {A'' : Type u_4} [AddCommGroup A'] [DistribMulAction C A'] [Finite A'] [AddCommGroup A] [DistribMulAction C A] [Finite A] [AddCommGroup A''] [DistribMulAction C A''] [Finite A''] [Finite C] (f : A' →+ A) (g : A →+ A'') (hf : ∀ (c : C) (a : A'), f (c • a) = c • f a) (hg : ∀ (c : C) (a : A), g (c • a) = c • g a) (hsurj : Function.Surjective ⇑g) (hexact : f.range = g.ker) (t : Marking C) (y : H2wR t) :
y ∈ (H2wMap_R t g hg).ker ↔ y ∈ (H2wMap_R t f hf).range

Exactness at H²w(A): ker(H²wMap g) = range(H²wMap f).

source
theorem GQ2.FoxH.H0w_exact_right_R {C : Type u_1} [Group C] {A' : Type u_2} {A : Type u_3} {A'' : Type u_4} [AddCommGroup A'] [DistribMulAction C A'] [Finite A'] [AddCommGroup A] [DistribMulAction C A] [Finite A] [AddCommGroup A''] [DistribMulAction C A''] [Finite C] (f : A' →+ A) (g : A →+ A'') (hf : ∀ (c : C) (a : A'), f (c • a) = c • f a) (hg : ∀ (c : C) (a : A), g (c • a) = c • g a) (hinj : Function.Injective ⇑f) (hsurj : Function.Surjective ⇑g) (hexact : f.range = g.ker) (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) (a'' : ↥(H0w t)) :
a'' ∈ (delta0_R f g hf hg hinj hsurj hexact t ht hw).ker ↔ a'' ∈ (H0wMap t g hg).range

Exactness at H⁰w(A''): ker δ⁰ = range(H⁰wMap g).

source
theorem GQ2.FoxH.H1w_exact_left_R {C : Type u_1} [Group C] {A' : Type u_2} {A : Type u_3} {A'' : Type u_4} [AddCommGroup A'] [DistribMulAction C A'] [Finite A'] [AddCommGroup A] [DistribMulAction C A] [Finite A] [AddCommGroup A''] [DistribMulAction C A''] [Finite C] (f : A' →+ A) (g : A →+ A'') (hf : ∀ (c : C) (a : A'), f (c • a) = c • f a) (hg : ∀ (c : C) (a : A), g (c • a) = c • g a) (hinj : Function.Injective ⇑f) (hsurj : Function.Surjective ⇑g) (hexact : f.range = g.ker) (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) (h : H1wR t) :
h ∈ (H1wMap_R t f hf).ker ↔ h ∈ (delta0_R f g hf hg hinj hsurj hexact t ht hw).range

Exactness at H¹w(A'): ker(H¹wMap f) = range δ⁰.

source
theorem GQ2.FoxH.H1w_exact_mid_R {C : Type u_1} [Group C] {A' : Type u_2} {A : Type u_3} {A'' : Type u_4} [AddCommGroup A'] [DistribMulAction C A'] [Finite A'] [AddCommGroup A] [DistribMulAction C A] [Finite A] [AddCommGroup A''] [DistribMulAction C A''] [Finite A''] [Finite C] (f : A' →+ A) (g : A →+ A'') (hf : ∀ (c : C) (a : A'), f (c • a) = c • f a) (hg : ∀ (c : C) (a : A), g (c • a) = c • g a) (hinj : Function.Injective ⇑f) (hsurj : Function.Surjective ⇑g) (hexact : f.range = g.ker) (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) (h : H1wR t) :
h ∈ (H1wMap_R t g hg).ker ↔ h ∈ (H1wMap_R t f hf).range

Exactness at H¹w(A): ker(H¹wMap g) = range(H¹wMap f).

source
theorem GQ2.FoxH.H1w_exact_right_R {C : Type u_1} [Group C] {A' : Type u_2} {A : Type u_3} {A'' : Type u_4} [AddCommGroup A'] [DistribMulAction C A'] [Finite A'] [AddCommGroup A] [DistribMulAction C A] [Finite A] [AddCommGroup A''] [DistribMulAction C A''] [Finite A''] [Finite C] (f : A' →+ A) (g : A →+ A'') (hf : ∀ (c : C) (a : A'), f (c • a) = c • f a) (hg : ∀ (c : C) (a : A), g (c • a) = c • g a) (hinj : Function.Injective ⇑f) (hsurj : Function.Surjective ⇑g) (hexact : f.range = g.ker) (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) (h : H1wR t) :
h ∈ (delta1_R f g hf hg hinj hsurj hexact t ht hw).ker ↔ h ∈ (H1wMap_R t g hg).range

Exactness at H¹w(A''): ker δ¹ = range(H¹wMap g).

source
theorem GQ2.FoxH.H2w_exact_left_R {C : Type u_1} [Group C] {A' : Type u_2} {A : Type u_3} {A'' : Type u_4} [AddCommGroup A'] [DistribMulAction C A'] [Finite A'] [AddCommGroup A] [DistribMulAction C A] [Finite A] [AddCommGroup A''] [DistribMulAction C A''] [Finite A''] [Finite C] (f : A' →+ A) (g : A →+ A'') (hf : ∀ (c : C) (a : A'), f (c • a) = c • f a) (hg : ∀ (c : C) (a : A), g (c • a) = c • g a) (hinj : Function.Injective ⇑f) (hsurj : Function.Surjective ⇑g) (hexact : f.range = g.ker) (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) (y : H2wR t) :
y ∈ (H2wMap_R t f hf).ker ↔ y ∈ (delta1_R f g hf hg hinj hsurj hexact t ht hw).range

Exactness at H²w(A'): ker(H²wMap f) = range δ¹.