Lemma 4: Künneth Formula for Balanced Products

Let H be a finite group of odd order, and let C, D be H-equivariant chain complexes over 𝔽₂. Then there is an isomorphism $$H_n(C \otimes_H D) \cong \bigoplus_{p+q=n} H_p(C) \otimes_H H_q(D)$$

The proof uses:

1. Over 𝔽₂ with |H| odd, coinvariants (-)_H is an exact functor
2. Exactness means coinvariants commutes with homology
3. The ordinary Künneth formula (Thm_1) gives H_n(C ⊗ D) ≅ ⊕ H_p(C) ⊗ H_q(D)
4. Applying coinvariants: H_n(C ⊗_H D) ≅ ⊕ H_p(C) ⊗_H H_q(D)

Main Definitions

• homologyAction: the induced H-action on H_p(C)
• balancedKunnethSummand: H_p(C) ⊗_H H_q(D)
• balancedKunnethSum: ⊕_{p+q=n} H_p(C) ⊗_H H_q(D)

Main Results

• kunnethBalancedProduct: the isomorphism H_n(C ⊗_H D) ≃ₗ[𝔽₂] ⊕ H_p(C) ⊗_H H_q(D)

Induced H-action on homology

Since the differentials are H-equivariant, H acts on cycles Z_p = ker ∂_p and boundaries B_p = im ∂_{p+1}. The induced action on H_p(C) = Z_p / B_p is well-defined.

def HEquivariantChainComplex.cyclesAction {H : Type u} [Group H] (C : HEquivariantChainComplex H) (p : ℤ) : Representation 𝔽₂ H ↥(C.complex.cycles p)

H acts on cycles Z_p(C) = ker ∂_p, since ∂(h · z) = h · ∂(z) = h · 0 = 0 for z ∈ ker ∂.

Equations

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

def HEquivariantChainComplex.boundariesAction {H : Type u} [Group H] (C : HEquivariantChainComplex H) (p : ℤ) : Representation 𝔽₂ H ↥(C.complex.boundaries p)

H acts on boundaries B_p(C) = im ∂_{p+1}, since for b = ∂(x), h · b = h · ∂(x) = ∂(h · x) ∈ im ∂.

Equations

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

def HEquivariantChainComplex.boundariesSubCyclesAction {H : Type u} [Group H] (C : HEquivariantChainComplex H) (p : ℤ) : Representation 𝔽₂ H ↥(C.complex.boundariesSubCycles p)

The boundaries submodule of cycles inherits an H-action from cyclesAction, compatible with the inclusion.

Equations

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

def HEquivariantChainComplex.homologyAction {H : Type u} [Group H] (C : HEquivariantChainComplex H) (p : ℤ) : Representation 𝔽₂ H (C.complex.homology' p)

The induced H-action on homology H_p(C) = Z_p / B_p. Since H acts on both Z_p and B_p compatibly, the quotient action is well-defined.

Equations

• C.homologyAction p = { toFun := fun (h : H) => (C.complex.boundariesSubCycles p).mapQ (C.complex.boundariesSubCycles p) ((C.cyclesAction p) h) ⋯, map_one' := ⋯, map_mul' := ⋯ }

Balanced Künneth summands

@[reducible, inline]

abbrev HEquivariantChainComplex.balancedKunnethSummand {H : Type u} [Group H] (C : HEquivariantChainComplex H) (D : HEquivariantChainComplex H) (n p : ℤ) : Type (max u_1 u_2)

The summand of the balanced Künneth decomposition at index p: H_p(C) ⊗_H H_{n-p}(D), the balanced product of homology groups. Defined as coinvariants of the tensor product representation, which avoids universe constraints of the balancedProduct abbreviation.

Equations

• C.balancedKunnethSummand D n p = ((C.homologyAction p).tprod (D.homologyAction (n - p))).Coinvariants

instance HEquivariantChainComplex.balancedKunnethSummand_addCommGroup {H : Type u} [Group H] (C : HEquivariantChainComplex H) (D : HEquivariantChainComplex H) (n p : ℤ) : AddCommGroup (C.balancedKunnethSummand D n p)

Equations

• C.balancedKunnethSummand_addCommGroup D n p = inferInstance

instance HEquivariantChainComplex.balancedKunnethSummand_module {H : Type u} [Group H] (C : HEquivariantChainComplex H) (D : HEquivariantChainComplex H) (n p : ℤ) : Module 𝔽₂ (C.balancedKunnethSummand D n p)

Equations

• C.balancedKunnethSummand_module D n p = inferInstance

@[reducible, inline]

abbrev HEquivariantChainComplex.balancedKunnethSum {H : Type u} [Group H] (C : HEquivariantChainComplex H) (D : HEquivariantChainComplex H) (n : ℤ) : Type (max u_2 u_1)

The balanced Künneth direct sum ⊕_{p : ℤ} H_p(C) ⊗_H H_{n-p}(D).

Equations

• C.balancedKunnethSum D n = DirectSum ℤ fun (p : ℤ) => C.balancedKunnethSummand D n p

instance HEquivariantChainComplex.balancedKunnethSum_addCommGroup {H : Type u} [Group H] (C : HEquivariantChainComplex H) (D : HEquivariantChainComplex H) (n : ℤ) : AddCommGroup (C.balancedKunnethSum D n)

Equations

• C.balancedKunnethSum_addCommGroup D n = DirectSum.instAddCommGroup fun (p : ℤ) => C.balancedKunnethSummand D n p

instance HEquivariantChainComplex.balancedKunnethSum_module {H : Type u} [Group H] (C : HEquivariantChainComplex H) (D : HEquivariantChainComplex H) (n : ℤ) : Module 𝔽₂ (C.balancedKunnethSum D n)

Equations

• C.balancedKunnethSum_module D n = DirectSum.instModule

Exactness of coinvariants in characteristic 2 with odd order group

Over 𝔽₂ with H of odd order, |H| = 1 in 𝔽₂, so the averaging map a(v) = ∑_h h·v is an idempotent splitting: V = V^H ⊕ ker(a). This makes (-)_H ≅ (-)^H an exact functor.

def HEquivariantChainComplex.invertible_card_of_odd_order {H : Type u} [Fintype H] (hodd : Odd (Fintype.card H)) : Invertible ↑(Fintype.card H)

The cardinality of H is invertible in 𝔽₂ when |H| is odd.

Equations

• HEquivariantChainComplex.invertible_card_of_odd_order hodd = ⋯.mpr invertibleOne

Main theorem: Künneth formula for balanced products

axiom HEquivariantChainComplex.kunnethBalancedProduct {H : Type u} [Group H] [Fintype H] (C D : HEquivariantChainComplex H) (hodd : Odd (Fintype.card H)) (n : ℤ) : (C.balancedProductComplex D).homology' n ≃ₗ[𝔽₂] C.balancedKunnethSum D n

Künneth Formula for Balanced Products (Lemma 4).

For H a finite group of odd order and C, D H-equivariant chain complexes over 𝔽₂, $$H_n(C \otimes_H D) \cong \bigoplus_{p+q=n} H_p(C) \otimes_H H_q(D).$$

The proof proceeds as follows:

1. Over 𝔽₂ with |H| odd, |H| = 1 in 𝔽₂, so the averaging map a = ∑_h ρ(h) is an idempotent with im(a) = V^H. This gives V = V^H ⊕ ker(a), making coinvariants (-)_H ≅ (-)^H an exact functor (Def_22, balancedProductInvariantsEquiv).
2. Since (-)_H is exact, it commutes with homology: H_n((C ⊗ D)_H) ≅ (H_n(C ⊗ D))_H.
3. By the Künneth formula (Thm_1): H_n(C ⊗ D) ≅ ⊕_{p+q=n} H_p(C) ⊗ H_q(D).
4. Taking coinvariants and using (-)_H commutes with finite direct sums: (H_n(C ⊗ D))_H ≅ ⊕_{p+q=n} (H_p(C) ⊗ H_q(D))_H = ⊕_{p+q=n} H_p(C) ⊗_H H_q(D).

Accepted as axiom: the full proof requires showing that the balanced product complex C ⊗_H D equals the coinvariants of the tensor product complex (C ⊗ D)_H at the chain complex level (connecting totalComplex from Def_10 with balancedProductComplex from Def_23), and then constructing the chain of isomorphisms through exact functor arguments. This infrastructure for coinvariant-homology interchange and for connecting the two total complex constructions is not available in Mathlib.

Satisfiability witnesses

theorem HEquivariantChainComplex.kunnethBalancedProduct_satisfiable : ∃ (H : Type) (x : Group H) (x_1 : Fintype H) (C : HEquivariantChainComplex H) (D : HEquivariantChainComplex H), Odd (Fintype.card H)

Witness: the premises of kunnethBalancedProduct are satisfiable. The trivial group H = Unit has odd order |H| = 1, and any chain complexes (e.g., the zero complex) are equivariant.

theorem HEquivariantChainComplex.balancedKunnethSummand_nonempty {H : Type u} [Group H] [Fintype H] (C : HEquivariantChainComplex H) (D : HEquivariantChainComplex H) (n p : ℤ) : Nonempty (C.balancedKunnethSummand D n p)

Witness: the balanced Künneth summand is nonempty (contains 0).

theorem HEquivariantChainComplex.balancedKunnethSum_nonempty {H : Type u} [Group H] [Fintype H] (C : HEquivariantChainComplex H) (D : HEquivariantChainComplex H) (n : ℤ) : Nonempty (C.balancedKunnethSum D n)

Witness: the balanced Künneth sum is nonempty (contains 0).