Documentation

GQ2.Roe.Devissage.LESMaster

§5.11 dévissage on the r_R spine: the dualized SES, δ-squares, and the master two-of-three #

Mechanical R-spine clone of GQ2/Devissage/LESMaster.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 generic four_lemma_inj, dual_exact_pair, dual_ses_exact, dualMap* and H0w_exact_mid/H0wMap are reused from GQ2.Devissage.*; the δ-square cores forward to prop_5_8_*_R/lemma_5_6_R (GQ2.Roe.Devissage.TracedRows).

The dualized SES and the δ-squares #

Dualizing the SES gives 0 → A''^∨ --g^∨--> A^∨ --f^∨--> A'^∨ → 0; the LES machinery instantiates on it verbatim. The δ-squares — the genuinely new commutativity content of the ladder — reduce to two snake-vs-snake core computations, each a chain of Prop 5.8 and Lemma 5.6 through the chosen lifts.

source
noncomputable def GQ2.FoxH.delta0D_R {C : Type u_1} [Group C] {A' : Type u_2} {A : Type u_3} {A'' : Type u_4} [AddCommGroup A'] [DistribMulAction C 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) (hA₂ : ∀ (a : A), a + a = 0) (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) :
↥(H0w t) →+ H1wR t

δ⁰ of the dualized SES: H⁰w(A'^∨) →+ H¹w(A''^∨).

Equations
Instances For
    source
    noncomputable def GQ2.FoxH.delta1D_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) (hA₂ : ∀ (a : A), a + a = 0) (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) :
    H1wR t →+ H2wR t

    δ¹ of the dualized SES: H¹w(A'^∨) →+ H²w(A''^∨).

    Equations
    Instances For
      source
      theorem GQ2.FoxH.delta_square_core1_R {C : Type u_1} [Group C] {A' : Type u_2} {A : Type u_3} {A'' : Type u_4} [AddCommGroup A'] [DistribMulAction C 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) (hA₂ : ∀ (a : A), a + a = 0) (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) (c'' : ↥(Z1wR t)) (lam : ↥(H0w t)) :
      ↑lam ((snakeZ_R f g hg hsurj hexact t c'').1 + (snakeZ_R f g hg hsurj hexact t c'').2) = mixedB_R t (↑c'') (snake0Z'_R (dualMap g) (dualMap f) ⋯ ⋯ ⋯ t lam)

      δ-square core 1: evaluating λ ∈ H⁰w(A'^∨) on the δ¹-snake of c'' equals pairing c'' against the dual δ⁰-snake word of λ. (Lift λ to Λ along f^∨; both sides equal B(lift c'', d⁰Λ) by Prop 5.8 right resp. Lemma 5.6.)

      source
      theorem GQ2.FoxH.delta_square_core2_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) (hA₂ : ∀ (a : A), a + a = 0) (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) (a'' : ↥(H0w t)) (y' : ↥(Z1wR t)) :
      mixedB_R t (snake0Z'_R f g hg hsurj hexact t a'') ↑y' = (snakeZ_R (dualMap g) (dualMap f) ⋯ ⋯ ⋯ t y').1 ↑a'' + (snakeZ_R (dualMap g) (dualMap f) ⋯ ⋯ ⋯ t y').2 ↑a''

      δ-square core 2: pairing the primal δ⁰-snake word of a'' against a dual cocycle y' equals evaluating the dual δ¹-snake of y' on a''. (Mirror of core 1: Prop 5.8 left + Lemma 5.6 through the lifts.)

      source
      theorem GQ2.FoxH.square_delta1_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) (hA₂ : ∀ (a : A), a + a = 0) (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) (h'' : H1wR t) :
      (chi2_R t ht hw) ((delta1_R f g hf hg hinj hsurj hexact t ht hw) h'') = (dualMap (delta0D_R f g hf hg hinj hsurj hexact hA₂ t ht hw)) ((chi1_R t ht hw) h'')

      δ-square (1,2): χ²_{A'} ∘ δ¹ = (δ⁰ of the dual SES)^∨ ∘ χ¹_{A''}.

      source
      theorem GQ2.FoxH.square_delta0_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) (hA₂ : ∀ (a : A), a + a = 0) (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) (a'' : ↥(H0w t)) :
      (chi1_R t ht hw) ((delta0_R f g hf hg hinj hsurj hexact t ht hw) a'') = (dualMap (delta1D_R f g hf hg hinj hsurj hexact hA₂ t ht hw)) ((chi0_R t ht hw) a'')

      δ-square (0,1): χ¹_{A'} ∘ δ⁰ = (δ¹ of the dual SES)^∨ ∘ χ⁰_{A''}.

      source
      theorem GQ2.FoxH.square_delta0D_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) (hA₂ : ∀ (a : A), a + a = 0) (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) (lam : ↥(H0w t)) :
      (chi1T_R t ht hw) ((delta0D_R f g hf hg hinj hsurj hexact hA₂ t ht hw) lam) = (dualMap (delta1_R f g hf hg hinj hsurj hexact t ht hw)) ((chi0T_R t ht hw) lam)

      δ-square (0,1), transposed: χ¹ᵀ_{A''} ∘ δ⁰_dual = (δ¹)^∨ ∘ χ⁰ᵀ_{A'}.

      source
      theorem GQ2.FoxH.square_delta1D_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) (hA₂ : ∀ (a : A), a + a = 0) (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) (z' : H1wR t) :
      (chi2T_R t ht hw) ((delta1D_R f g hf hg hinj hsurj hexact hA₂ t ht hw) z') = (dualMap (delta0_R f g hf hg hinj hsurj hexact t ht hw)) ((chi1T_R t ht hw) z')

      δ-square (1,2), transposed: χ²ᵀ_{A''} ∘ δ¹_dual = (δ⁰)^∨ ∘ χ¹ᵀ_{A'}.

      source
      theorem GQ2.FoxH.selfdualW_two_of_three_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) (hA₂ : ∀ (a : A), a + a = 0) (t : Marking C) (ht : t.TameRel) (hw : t.WildRelR) :
      (IsSelfDualW_R t A' ∧ IsSelfDualW_R t A'' → IsSelfDualW_R t A) ∧ (IsSelfDualW_R t A' ∧ IsSelfDualW_R t A → IsSelfDualW_R t A'') ∧ (IsSelfDualW_R t A ∧ IsSelfDualW_R t A'' → IsSelfDualW_R t A')

      Lemma 5.11, word-internal form (exact-cone dévissage): two-out-of-three for IsSelfDualW_R along the module SES. Proof: translate each IsSelfDualW_R into χ-bijectivities (isSelfDualW_iff_R, chi_bij_of_selfdualW_R), then chase the duality ladder — nine four-lemma windows across the two LESs (word complex of the SES, and of its dualization) tied by the lemma_5_6_R-squares, the evaluation squares and the δ-squares.