The equivariant-Hom counting engine

The single-step multiplicativity of equivariant-Hom counts across an equivariant short exact presentation, from a regular-summand package (the Lemma-6.11 output shape, taken as a hypothesis): for C-modules and an exact W' —j→ W —π→ W'' of finite 2-torsion modules,

#Hom_C(V, W) = #Hom_C(V, W') · #Hom_C(V, W'').

Design: equivHoms C V W is the subgroup of V →+ W cut out by C-equivariance; post-composition with π is an additive map Φ between these Hom groups; the count is Lagrange (AddSubgroup.card_eq_card_quotient_mul_card_addSubgroup) + the first isomorphism theorem (QuotientAddGroup.quotientKerEquivOfSurjective), with

• surjectivity of Φ supplied by equivariant_lift_of_regular_summand (GQ2/RegularSummand.lean; its input lemma_6_11 is std-3), and
• ker Φ ≃ Hom_C(V, W') from the kernel identification along j (choice-lift through the injection).

The iterated product over a full filtration is intentionally left to the consumer: concrete graded presentations vary, and each step is one application of card_equivHoms_of_exact. This file is axiom-free.

def GQ2.equivHoms (C : Type) [Group C] (V W : Type) [AddCommGroup V] [AddCommGroup W] [DistribMulAction C V] [DistribMulAction C W] : AddSubgroup (V →+ W)

The C-equivariant additive maps V →+ W, as an additive subgroup of V →+ W (equivariance is closed under 0, +, − since the actions are additive).

Equations

• GQ2.equivHoms C V W = { carrier := {f : V →+ W | ∀ (c : C) (v : V), f (c • v) = c • f v}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

def GQ2.postCompHom {C : Type} [Group C] {V W W'' : Type} [AddCommGroup V] [AddCommGroup W] [AddCommGroup W''] [DistribMulAction C V] [DistribMulAction C W] [DistribMulAction C W''] (π : W →+ W'') (hπeq : ∀ (c : C) (w : W), π (c • w) = c • π w) : ↥(equivHoms C V W) →+ ↥(equivHoms C V W'')

Post-composition with an equivariant π : W →+ W'', as an additive map between the equivariant-Hom groups.

Equations

• GQ2.postCompHom π hπeq = AddMonoidHom.mk' (fun (f : ↥(GQ2.equivHoms C V W)) => ⟨π.comp ↑f, ⋯⟩) ⋯

theorem GQ2.card_ker_postCompHom {C : Type} [Group C] {V W W' W'' : Type} [AddCommGroup V] [AddCommGroup W] [AddCommGroup W'] [AddCommGroup W''] [DistribMulAction C V] [DistribMulAction C W] [DistribMulAction C W'] [DistribMulAction C W''] (j : W' →+ W) (hjeq : ∀ (c : C) (w : W'), j (c • w) = c • j w) (hjinj : Function.Injective ⇑j) (π : W →+ W'') (hπeq : ∀ (c : C) (w : W), π (c • w) = c • π w) (hexact : ∀ (w : W), π w = 0 ↔ w ∈ Set.range ⇑j) : Nat.card ↥(postCompHom π hπeq).ker = Nat.card ↥(equivHoms C V W')

The kernel identification: composing with an equivariant injection j : W' →+ W whose range is ker π identifies Hom_C(V, W') with the kernel of post-composition by π.

theorem GQ2.card_equivHoms_of_exact {C : Type} [Group C] {V W W' W'' : Type} [AddCommGroup V] [AddCommGroup W] [AddCommGroup W'] [AddCommGroup W''] [DistribMulAction C V] [DistribMulAction C W] [DistribMulAction C W'] [DistribMulAction C W''] [Finite C] [Finite V] [Finite W] [Finite W''] (h2W : ∀ (w : W), w + w = 0) (h2W'' : ∀ (w : W''), w + w = 0) {N : ℕ} (ι : V →+ Fin N → C → ZMod 2) (r : (Fin N → C → ZMod 2) →+ V) (hι : ∀ (h : C) (v : V) (n : Fin N) (x : C), ι (h • v) n x = ι v n (h⁻¹ * x)) (hr : ∀ (h : C) (F : Fin N → C → ZMod 2), (r fun (n : Fin N) (x : C) => F n (h⁻¹ * x)) = h • r F) (hri : ∀ (v : V), r (ι v) = v) (j : W' →+ W) (hjeq : ∀ (c : C) (w : W'), j (c • w) = c • j w) (hjinj : Function.Injective ⇑j) (π : W →+ W'') (hπeq : ∀ (c : C) (w : W), π (c • w) = c • π w) (hπsurj : Function.Surjective ⇑π) (hexact : ∀ (w : W), π w = 0 ↔ w ∈ Set.range ⇑j) : Nat.card ↥(equivHoms C V W) = Nat.card ↥(equivHoms C V W') * Nat.card ↥(equivHoms C V W'')

The counting step (the deep-part proof): given a regular-summand package (ι, r) for V (the Lemma-6.11 output shape, as a hypothesis) and a C-equivariant short exact presentation W' —j→ W —π→ W'' of finite 2-torsion modules, the equivariant-Hom counts multiply:

#Hom_C(V, W) = #Hom_C(V, W') · #Hom_C(V, W'').

Lagrange along ker (π ∘ −) + first isomorphism theorem; surjectivity of post-composition is the banked equivariant_lift_of_regular_summand. Iterating over a filtration M = F₀ ⊇ … ⊇ F_n = 0 (one application per graded step, at the consumer's concrete presentation of grⱼ) yields #Hom_C(V, M) = ∏ⱼ #Hom_C(V, grⱼ) — the Hom(V^∨, −)-exactness count of the Lemma-6.17 dimension clause.

theorem GQ2.card_equivHoms_congr {C : Type} [Group C] {V W W'' : Type} [AddCommGroup V] [AddCommGroup W] [AddCommGroup W''] [DistribMulAction C V] [DistribMulAction C W] [DistribMulAction C W''] (e : W ≃+ W'') (heq : ∀ (c : C) (w : W), e (c • w) = c • e w) : Nat.card ↥(equivHoms C V W) = Nat.card ↥(equivHoms C V W'')

Transport: the equivariant-Hom count only depends on the target up to equivariant additive isomorphism — the consumer's tool for swapping in a concrete model of a graded piece.