§5.11 dévissage: the long exact sequence — SES of complexes and connecting maps

Part of the §5.11 dévissage development (split from GQ2/Devissage.lean).

The long exact sequence

A module SES 0 → A' --f--> A --g--> A'' → 0 (with C-equivariant f, g) induces a short exact sequence of word complexes; the degreewise functors (·)⁴ and (·)² are exact. From this we build the connecting maps and the nine-term LES.

theorem GQ2.FoxH.pi_g_surjective {A : Type u_3} {A'' : Type u_4} [AddCommGroup A] [AddCommGroup A''] (g : A →+ A'') (hsurj : Function.Surjective ⇑g) : Function.Surjective fun (x : Fin 4 → A) (i : Fin 4) => g (x i)

Degree-1 ((·)⁴) surjectivity: g applied componentwise is surjective.

theorem GQ2.FoxH.pi_exact {A' : Type u_2} {A : Type u_3} {A'' : Type u_4} [AddCommGroup A'] [AddCommGroup A] [AddCommGroup A''] (f : A' →+ A) (g : A →+ A'') (hexact : f.range = g.ker) (y : Fin 4 → A) : (fun (i : Fin 4) => g (y i)) = 0 ↔ ∃ (x : Fin 4 → A'), (fun (i : Fin 4) => f (x i)) = y

Degree-1 exactness: ker(g∘·) = range(f∘·) on Fin 4 → A.

theorem GQ2.FoxH.prod_g_surjective {A : Type u_3} {A'' : Type u_4} [AddCommGroup A] [AddCommGroup A''] (g : A →+ A'') (hsurj : Function.Surjective ⇑g) : Function.Surjective ⇑(g.prodMap g)

Degree-2 ((·)²) surjectivity: g × g is surjective.

theorem GQ2.FoxH.prod_exact {A' : Type u_2} {A : Type u_3} {A'' : Type u_4} [AddCommGroup A'] [AddCommGroup A] [AddCommGroup A''] (f : A' →+ A) (g : A →+ A'') (hexact : f.range = g.ker) (p : A × A) : (g.prodMap g) p = 0 ↔ ∃ (q : A' × A'), (f.prodMap f) q = p

Degree-2 exactness: ker(g × g) = range(f × f) on A × A.

The connecting map δ¹ : H¹w(A'') → H²w(A') (snake)

noncomputable def GQ2.FoxH.snakeLift {A : Type u_3} {A'' : Type u_4} [AddCommGroup A] [AddCommGroup A''] (g : A →+ A'') (hsurj : Function.Surjective ⇑g) (c'' : Fin 4 → A'') : Fin 4 → A

A chosen lift of a degree-1 A''-cochain to A⁴ (via g surjective).

Equations

• GQ2.FoxH.snakeLift g hsurj c'' i = ⋯.choose

@[simp]

theorem GQ2.FoxH.snakeLift_spec {A : Type u_3} {A'' : Type u_4} [AddCommGroup A] [AddCommGroup A''] (g : A →+ A'') (hsurj : Function.Surjective ⇑g) (c'' : Fin 4 → A'') (i : Fin 4) : g (snakeLift g hsurj c'' i) = c'' i

theorem GQ2.FoxH.snake_d1_mem {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) (c'' : ↥(Z1w t)) : (g.prodMap g) ((d1 t) (snakeLift g hsurj ↑c'')) = 0

For a cocycle c'' ∈ Z¹w(A''), d¹ of its lift lands in ker(g × g).

noncomputable def GQ2.FoxH.snakeZ {C : Type u_1} [Group C] {A' : Type u_2} {A : Type u_3} {A'' : Type u_4} [AddCommGroup A'] [AddCommGroup A] [DistribMulAction C A] [Finite A] [AddCommGroup A''] [DistribMulAction C A''] [Finite A''] [Finite C] (f : A' →+ A) (g : A →+ A'') (hg : ∀ (c : C) (a : A), g (c • a) = c • g a) (hsurj : Function.Surjective ⇑g) (hexact : f.range = g.ker) (t : Marking C) (c'' : ↥(Z1w t)) : A' × A'

The A'²-element the snake extracts: (f × f)(snakeZ) = d¹(lift c'').

Equations

• GQ2.FoxH.snakeZ f g hg hsurj hexact t c'' = ⋯.choose

theorem GQ2.FoxH.snakeZ_spec {C : Type u_1} [Group C] {A' : Type u_2} {A : Type u_3} {A'' : Type u_4} [AddCommGroup A'] [AddCommGroup A] [DistribMulAction C A] [Finite A] [AddCommGroup A''] [DistribMulAction C A''] [Finite A''] [Finite C] (f : A' →+ A) (g : A →+ A'') (hg : ∀ (c : C) (a : A), g (c • a) = c • g a) (hsurj : Function.Surjective ⇑g) (hexact : f.range = g.ker) (t : Marking C) (c'' : ↥(Z1w t)) : (f.prodMap f) (snakeZ f g hg hsurj hexact t c'') = (d1 t) (snakeLift g hsurj ↑c'')

theorem GQ2.FoxH.snakeZ_welldef {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) (c'' : ↥(Z1w t)) (c : Fin 4 → A) (z : A' × A') (hc : (fun (i : Fin 4) => g (c i)) = ↑c'') (hz : (f.prodMap f) z = (d1 t) c) : ↑z = ↑(snakeZ f g hg hsurj hexact t c'')

Well-definedness of the snake: for any lift c of c'' and any z with (f×f)(z) = d¹(c), the class [z] ∈ H²w(A') equals [snakeZ c''] — so δ¹ will not depend on the chosen lift, hence descends to a hom on H¹w(A'').

noncomputable def GQ2.FoxH.delta1raw {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) : ↥(Z1w t) →+ H2w t

The connecting map on cocycles, Z¹w(A'') →+ H²w(A'), c'' ↦ [snakeZ c''] (a hom by snakeZ_welldef, using additive lifts).

Equations

• GQ2.FoxH.delta1raw f g hf hg hinj hsurj hexact t = { toFun := fun (c'' : ↥(GQ2.FoxH.Z1w t)) => ↑(GQ2.FoxH.snakeZ f g hg hsurj hexact t c''), map_zero' := ⋯, map_add' := ⋯ }

noncomputable def GQ2.FoxH.delta1 {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.WildRel) : H1w t →+ H2w t

The snake connecting map δ¹ : H¹w(A'') → H²w(A'). Descends delta1raw through the B¹w-quotient: a coboundary c'' = d⁰(a'') lifts to d⁰(â), whose d¹ is 0, so its class is 0.

Equations

• GQ2.FoxH.delta1 f g hf hg hinj hsurj hexact t ht hw = QuotientAddGroup.lift ((GQ2.FoxH.B1w t).addSubgroupOf (GQ2.FoxH.Z1w t)) (GQ2.FoxH.delta1raw f g hf hg hinj hsurj hexact t) ⋯

The connecting map δ⁰ : H⁰w(A'') → H¹w(A') (snake)

The mirror of δ¹ one degree down. Lift a'' ∈ H⁰w(A'') to a ∈ A; then d⁰a ∈ ker(g∘·) (as g∘d⁰a = d⁰(g a) = d⁰a'' = 0), so d⁰a = f∘w for a unique w : A'⁴, which is a cocycle (f∘d¹w = d¹(f∘w) = d¹d⁰a = 0, f injective). δ⁰(a'') := [w] ∈ H¹w(A'); the class is independent of the lift a (a different lift shifts w by a coboundary). The domain H⁰w is an honest subgroup (no quotient), so — unlike δ¹ — no descent is needed, only lift-independence.

theorem GQ2.FoxH.snake0_d0_mem {C : Type u_1} [Group C] {A : Type u_3} {A'' : Type u_4} [AddCommGroup A] [DistribMulAction C A] [AddCommGroup A''] [DistribMulAction C A''] (g : A →+ A'') (hg : ∀ (c : C) (a : A), g (c • a) = c • g a) (hsurj : Function.Surjective ⇑g) (t : Marking C) (a'' : ↥(H0w t)) : (fun (i : Fin 4) => g ((d0 t) ⋯.choose i)) = 0

For a'' ∈ H⁰w(A''), d⁰ of the chosen lift lands in ker(g∘·) (degree 1).

noncomputable def GQ2.FoxH.snake0Z' {C : Type u_1} [Group C] {A' : Type u_2} {A : Type u_3} {A'' : Type u_4} [AddCommGroup A'] [AddCommGroup A] [DistribMulAction C A] [AddCommGroup A''] [DistribMulAction C A''] (f : A' →+ A) (g : A →+ A'') (hg : ∀ (c : C) (a : A), g (c • a) = c • g a) (hsurj : Function.Surjective ⇑g) (hexact : f.range = g.ker) (t : Marking C) (a'' : ↥(H0w t)) : Fin 4 → A'

The A'⁴-cochain the degree-0 snake extracts: f∘(snake0Z') = d⁰(lift a'').

Equations

• GQ2.FoxH.snake0Z' f g hg hsurj hexact t a'' = ⋯.choose

theorem GQ2.FoxH.snake0Z'_spec {C : Type u_1} [Group C] {A' : Type u_2} {A : Type u_3} {A'' : Type u_4} [AddCommGroup A'] [AddCommGroup A] [DistribMulAction C A] [AddCommGroup A''] [DistribMulAction C A''] (f : A' →+ A) (g : A →+ A'') (hg : ∀ (c : C) (a : A), g (c • a) = c • g a) (hsurj : Function.Surjective ⇑g) (hexact : f.range = g.ker) (t : Marking C) (a'' : ↥(H0w t)) : (fun (i : Fin 4) => f (snake0Z' f g hg hsurj hexact t a'' i)) = (d0 t) ⋯.choose

theorem GQ2.FoxH.snake0Z'_mem {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.WildRel) (a'' : ↥(H0w t)) : (d1 t) (snake0Z' f g hg hsurj hexact t a'') = 0

snake0Z' ∈ Z¹w(A'): its d¹ vanishes (pull d¹∘d⁰ = 0 back through the injection f).

theorem GQ2.FoxH.delta0_welldef {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.WildRel) (a'' : ↥(H0w t)) (a : A) (w : Fin 4 → A') (hwmem : (d1 t) w = 0) (ha : g a = ↑a'') (hfw : (fun (i : Fin 4) => f (w i)) = (d0 t) a) : ↑⟨w, ⋯⟩ = ↑⟨snake0Z' f g hg hsurj hexact t a'', ⋯⟩

Lift-independence of δ⁰: any lift a of a'' with cocycle w (f∘w = d⁰a) gives the same class [w] = δ⁰(a''). A second lift differs by f a', shifting w by d⁰a'.

noncomputable def GQ2.FoxH.delta0 {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.WildRel) : ↥(H0w t) →+ H1w t

The degree-0 connecting map δ⁰ : H⁰w(A'') →+ H¹w(A').

Equations

• GQ2.FoxH.delta0 f g hf hg hinj hsurj hexact t ht hw = { toFun := fun (a'' : ↥(GQ2.FoxH.H0w t)) => ↑⟨GQ2.FoxH.snake0Z' f g hg hsurj hexact t a'', ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }