Definition 22: Balanced Product of Vector Spaces

The balanced product V ⊗_H W of 𝔽₂[H]-modules is defined as the coinvariants of the diagonal H-action on V ⊗ W. In the paper's right-action convention vh = ρ_V(h⁻¹)(v), the balanced relation is [vh ⊗ w] = [v ⊗ hw].

Main Definitions

• balancedProduct: V ⊗_H W as coinvariants of ρ_V ⊗ ρ_W.
• balancedProduct.mk: quotient map V ⊗ W → V ⊗_H W.

Main Results

• balancedProduct.balanced: [ρ_V(h⁻¹)(v) ⊗ w] = [v ⊗ ρ_W(h)(w)].
• balancedProductInvariantsEquiv: V ⊗_H W ≅ (V ⊗ W)^H when |H| is odd.
• balancedProductCoinvariantsEquiv: V ⊗_H 𝔽₂ ≅ V_H.

The Balanced Product

@[reducible, inline]

abbrev balancedProduct {H : Type u} [Group H] {V W : Type u} [AddCommGroup V] [Module 𝔽₂ V] [AddCommGroup W] [Module 𝔽₂ W] (ρV : Representation 𝔽₂ H V) (ρW : Representation 𝔽₂ H W) : Type u

The balanced product V ⊗_H W, defined as the coinvariants of the diagonal H-action h · (v ⊗ w) = ρ_V(h)(v) ⊗ ρ_W(h)(w) on V ⊗ W. Equivalently, V ⊗_{𝔽₂[H]} W — the tensor product over the group algebra.

Equations

• balancedProduct ρV ρW = (ρV.tprod ρW).Coinvariants

def balancedProduct.mk {H : Type u} [Group H] {V W : Type u} [AddCommGroup V] [Module 𝔽₂ V] [AddCommGroup W] [Module 𝔽₂ W] (ρV : Representation 𝔽₂ H V) (ρW : Representation 𝔽₂ H W) : TensorProduct 𝔽₂ V W →ₗ[𝔽₂] balancedProduct ρV ρW

The quotient map V ⊗ W → V ⊗_H W.

Equations

• balancedProduct.mk ρV ρW = Representation.Coinvariants.mk (ρV.tprod ρW)

theorem balancedProduct.diagonal_balanced {H : Type u} [Group H] {V W : Type u} [AddCommGroup V] [Module 𝔽₂ V] [AddCommGroup W] [Module 𝔽₂ W] (ρV : Representation 𝔽₂ H V) (ρW : Representation 𝔽₂ H W) (h : H) (v : V) (w : W) : (Representation.Coinvariants.mk (ρV.tprod ρW)) ((ρV h) v ⊗ₜ[𝔽₂] (ρW h) w) = (Representation.Coinvariants.mk (ρV.tprod ρW)) (v ⊗ₜ[𝔽₂] w)

[ρ_V(h)(v) ⊗ ρ_W(h)(w)] = [v ⊗ w] in V ⊗_H W.

theorem balancedProduct.balanced {H : Type u} [Group H] {V W : Type u} [AddCommGroup V] [Module 𝔽₂ V] [AddCommGroup W] [Module 𝔽₂ W] (ρV : Representation 𝔽₂ H V) (ρW : Representation 𝔽₂ H W) (h : H) (v : V) (w : W) : (Representation.Coinvariants.mk (ρV.tprod ρW)) ((ρV h⁻¹) v ⊗ₜ[𝔽₂] w) = (Representation.Coinvariants.mk (ρV.tprod ρW)) (v ⊗ₜ[𝔽₂] (ρW h) w)

The paper's balancing relation: [ρ_V(h⁻¹)(v) ⊗ w] = [v ⊗ ρ_W(h)(w)]. In right-action notation, this says [vh ⊗ w] = [v ⊗ hw]. Proof: apply diagonal relation at h to (ρ_V(h⁻¹)(v), w).

theorem balancedProduct.balanced' {H : Type u} [Group H] {V W : Type u} [AddCommGroup V] [Module 𝔽₂ V] [AddCommGroup W] [Module 𝔽₂ W] (ρV : Representation 𝔽₂ H V) (ρW : Representation 𝔽₂ H W) (h : H) (v : V) (w : W) : (Representation.Coinvariants.mk (ρV.tprod ρW)) ((ρV h) v ⊗ₜ[𝔽₂] w) = (Representation.Coinvariants.mk (ρV.tprod ρW)) (v ⊗ₜ[𝔽₂] (ρW h⁻¹) w)

Equivalent: [ρ_V(h)(v) ⊗ w] = [v ⊗ ρ_W(h⁻¹)(w)].

theorem balancedProduct.ext' {H : Type u} [Group H] {V W : Type u} [AddCommGroup V] [Module 𝔽₂ V] [AddCommGroup W] [Module 𝔽₂ W] (ρV : Representation 𝔽₂ H V) (ρW : Representation 𝔽₂ H W) {X : Type u} [AddCommGroup X] [Module 𝔽₂ X] (f g : (ρV.tprod ρW).Coinvariants →ₗ[𝔽₂] X) (h : ∀ (v : V) (w : W), f ((Representation.Coinvariants.mk (ρV.tprod ρW)) (v ⊗ₜ[𝔽₂] w)) = g ((Representation.Coinvariants.mk (ρV.tprod ρW)) (v ⊗ₜ[𝔽₂] w))) : f = g

Extensionality for maps from V ⊗_H W.

theorem balancedProduct.mk_surjective {H : Type u} [Group H] {V W : Type u} [AddCommGroup V] [Module 𝔽₂ V] [AddCommGroup W] [Module 𝔽₂ W] (ρV : Representation 𝔽₂ H V) (ρW : Representation 𝔽₂ H W) : Function.Surjective ⇑(mk ρV ρW)

The quotient map is surjective.

Isomorphism with Invariants (Odd Order Case)

def avgDescended {H : Type u} [Group H] {V W : Type u} [AddCommGroup V] [Module 𝔽₂ V] [AddCommGroup W] [Module 𝔽₂ W] (ρV : Representation 𝔽₂ H V) (ρW : Representation 𝔽₂ H W) [Fintype H] [Invertible ↑(Fintype.card H)] : balancedProduct ρV ρW →ₗ[𝔽₂] ↥(ρV.tprod ρW).invariants

The descended averaging map: V ⊗_H W → (V ⊗ W)^H.

Equations

• avgDescended ρV ρW = (Representation.Coinvariants.ker (ρV.tprod ρW)).liftQ (LinearMap.codRestrict (ρV.tprod ρW).invariants (ρV.tprod ρW).averageMap ⋯) ⋯

def invToBalanced {H : Type u} [Group H] {V W : Type u} [AddCommGroup V] [Module 𝔽₂ V] [AddCommGroup W] [Module 𝔽₂ W] (ρV : Representation 𝔽₂ H V) (ρW : Representation 𝔽₂ H W) : ↥(ρV.tprod ρW).invariants →ₗ[𝔽₂] balancedProduct ρV ρW

The inclusion map: (V ⊗ W)^H → V ⊗_H W.

Equations

• invToBalanced ρV ρW = Representation.Coinvariants.mk (ρV.tprod ρW) ∘ₗ (ρV.tprod ρW).invariants.subtype

noncomputable def balancedProductInvariantsEquiv {H : Type u} [Group H] {V W : Type u} [AddCommGroup V] [Module 𝔽₂ V] [AddCommGroup W] [Module 𝔽₂ W] (ρV : Representation 𝔽₂ H V) (ρW : Representation 𝔽₂ H W) [Fintype H] [Invertible ↑(Fintype.card H)] : balancedProduct ρV ρW ≃ₗ[𝔽₂] ↥(ρV.tprod ρW).invariants

When H is finite of odd order, V ⊗_H W ≅ (V ⊗ W)^H.

The forward map sends [v ⊗ w] ↦ (1/|H|) ∑_h ρ_V(h)(v) ⊗ ρ_W(h)(w). The inverse is the composition of the inclusion and the quotient map.

Equations

• balancedProductInvariantsEquiv ρV ρW = { toFun := ⇑(avgDescended ρV ρW), map_add' := ⋯, map_smul' := ⋯, invFun := ⇑(invToBalanced ρV ρW), left_inv := ⋯, right_inv := ⋯ }

Coinvariants Specialization

def balancedProductCoinvariantsEquiv {H : Type u} [Group H] {V : Type u} [AddCommGroup V] [Module 𝔽₂ V] (ρV : Representation 𝔽₂ H V) : (ρV.tprod (Representation.trivial 𝔽₂ H 𝔽₂)).Coinvariants ≃ₗ[𝔽₂] ρV.Coinvariants

V ⊗_H 𝔽₂ ≅ V_H when 𝔽₂ has trivial H-action. This identifies (V ⊗ 𝔽₂)/⟨ρ_V(h)(v) ⊗ a - v ⊗ a⟩ ≅ V/⟨ρ_V(h)(v) - v⟩ via TensorProduct.rid : V ⊗ 𝔽₂ ≅ V.

Equations

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

Witness

theorem balancedProduct_nonempty {H : Type u} [Group H] {V W : Type u} [AddCommGroup V] [Module 𝔽₂ V] [AddCommGroup W] [Module 𝔽₂ W] (ρV : Representation 𝔽₂ H V) (ρW : Representation 𝔽₂ H W) : Nonempty (balancedProduct ρV ρW)

The balanced product contains 0.