Definition 23: Balanced Product Chain Complex

Given a group H, chain complexes C and D with H-equivariant differentials (where each C_i carries a right H-action and each D_j carries a left H-action), the balanced product double complex C ⊠_H D has objects (C ⊠_H D)_{p,q} = C_p ⊗_H D_q (Def_22) with differentials:

• horizontal ∂^h = ∂^C ⊗_H id_D (changes p, keeps q)
• vertical ∂^v = id_C ⊗_H ∂^D (changes q, keeps p)

These satisfy the double complex (Def_9) because (∂^C)² = 0, (∂^D)² = 0, and ∂^C ⊗ ∂^D = ∂^C ⊗ ∂^D (commutativity).

The balanced product complex is C ⊗_H D = Tot(C ⊠_H D) (Def_10).

Main Definitions

• HEquivariantChainComplex: chain complex with H-action and equivariant differentials
• balancedProductDoubleComplex: the double complex C ⊠_H D
• balancedProductComplex: the total complex C ⊗_H D = Tot(C ⊠_H D)

Main Results

• Double complex : (∂^h)² = 0, (∂^v)² = 0, ∂^h ∘ ∂^v = ∂^v ∘ ∂^h

H-Equivariant Chain Complexes

structure HEquivariantChainComplex (H : Type u) [Group H] : Type (max u (u_1 + 1))

A chain complex with H-action on each degree, where differentials are H-equivariant: ∂(h · x) = h · ∂(x) for all x ∈ C_i, h ∈ H.

• complex : ChainComplex𝔽₂

  The underlying chain complex over 𝔽₂.

• action (i : ℤ) : Representation 𝔽₂ H ↑(self.complex.X i)

  The H-action on each degree.

• equivariant (i j : ℤ) (h : H) : ModuleCat.Hom.hom (self.complex.d i j) ∘ₗ (self.action i) h = (self.action j) h ∘ₗ ModuleCat.Hom.hom (self.complex.d i j)

  The differentials commute with the H-action.

Balanced Product Objects

def HEquivariantChainComplex.bpObj {H : Type u} [Group H] (C D : HEquivariantChainComplex H) (p q : ℤ) : ModuleCat 𝔽₂

The balanced product object at (p, q): C_p ⊗_H D_q.

Equations

• C.bpObj D p q = ModuleCat.of 𝔽₂ (balancedProduct (C.action p) (D.action q))

Equivariance lemmas for tensor product maps

Balanced Product Differentials

def HEquivariantChainComplex.bpDh {H : Type u} [Group H] (C D : HEquivariantChainComplex H) (p p' q : ℤ) : C.bpObj D p q ⟶ C.bpObj D p' q

The horizontal differential ∂^C ⊗_H id_D : C_p ⊗_H D_q → C_{p'} ⊗_H D_q. Well-defined on the balanced product by H-equivariance of ∂^C.

Equations

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

def HEquivariantChainComplex.bpDv {H : Type u} [Group H] (C D : HEquivariantChainComplex H) (p q q' : ℤ) : C.bpObj D p q ⟶ C.bpObj D p q'

The vertical differential id_C ⊗_H ∂^D : C_p ⊗_H D_q → C_p ⊗_H D_{q'}. Well-defined on the balanced product by H-equivariance of ∂^D.

Equations

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

Shape conditions

d² = 0 conditions

Commutativity: ∂^h ∘ ∂^v = ∂^v ∘ ∂^h

The Balanced Product Double Complex

def HEquivariantChainComplex.balancedProductDoubleComplex {H : Type u} [Group H] (C D : HEquivariantChainComplex H) : DoubleComplex𝔽₂

The balanced product double complex C ⊠_H D as a DoubleComplex𝔽₂. Objects are (C ⊠_H D)_{p,q} = C_p ⊗_H D_q with:

• horizontal differential ∂^h = ∂^C ⊗_H id_D (changes p)
• vertical differential ∂^v = id_C ⊗_H ∂^D (changes q)

Equations

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

Total complex

instance HEquivariantChainComplex.balancedProductDoubleComplex_hasTotal {H : Type u} [Group H] (C D : HEquivariantChainComplex H) : HomologicalComplex₂.HasTotal (C.balancedProductDoubleComplex D) (ComplexShape.down ℤ)

def HEquivariantChainComplex.balancedProductComplex {H : Type u} [Group H] (C D : HEquivariantChainComplex H) : ChainComplex𝔽₂

The balanced product complex C ⊗_H D = Tot(C ⊠_H D). This is the total complex of the balanced product double complex.

Equations

• C.balancedProductComplex D = (C.balancedProductDoubleComplex D).totalComplex

Basic properties

theorem HEquivariantChainComplex.balancedProductDoubleComplex_obj {H : Type u} [Group H] (C D : HEquivariantChainComplex H) (p q : ℤ) : (C.balancedProductDoubleComplex D).obj p q = C.bpObj D p q

The object (C ⊠_H D)_{p,q} = C_p ⊗_H D_q.

theorem HEquivariantChainComplex.balancedProductDoubleComplex_dv_eq {H : Type u} [Group H] (C D : HEquivariantChainComplex H) (p q : ℤ) : (C.balancedProductDoubleComplex D).dv p q = ModuleCat.Hom.hom (C.bpDv D p q (q - 1))

The vertical differential of the balanced product double complex is id_C ⊗_H ∂^D.

theorem HEquivariantChainComplex.balancedProductDoubleComplex_dh_eq {H : Type u} [Group H] (C D : HEquivariantChainComplex H) (p q : ℤ) : (C.balancedProductDoubleComplex D).dh p q = ModuleCat.Hom.hom (C.bpDh D p (p - 1) q)

The horizontal differential of the balanced product double complex is ∂^C ⊗_H id_D.

Witness: the balanced product is nonempty

theorem HEquivariantChainComplex.balancedProductComplex_nonempty {H : Type u} [Group H] (C D : HEquivariantChainComplex H) (n : ℤ) : Nonempty ↑((C.balancedProductComplex D).X n)