Generic 𝔽₂ counting: coannihilators and the sum line

theorem Q2Presentation.Lifting.card_dualCoannihilator_mul_card {V : Type} [AddCommGroup V] [Module (ZMod 2) V] [Finite V] (W : Submodule (ZMod 2) (Module.Dual (ZMod 2) V)) : Nat.card ↥W.dualCoannihilator * Nat.card ↥W = Nat.card V

Coannihilator dimension count over a finite 𝔽₂-module: a dual-side submodule and its coannihilator multiply to the ambient cardinality.

theorem Q2Presentation.Lifting.mem_sumLine_comap {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (A : Submodule (ZMod 2) V) (x : V × V) : x ∈ Submodule.comap (LinearMap.fst (ZMod 2) V V + LinearMap.snd (ZMod 2) V V) A ↔ x.1 + x.2 ∈ A

Membership in the sum-line comap is the sum condition.

def Q2Presentation.Lifting.dlineEquiv {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (A : Submodule (ZMod 2) V) : ↥(Submodule.comap (LinearMap.fst (ZMod 2) V V + LinearMap.snd (ZMod 2) V V) A) ≃ V × ↥A

The sum line over A matches V × A by (u, v) ↦ (u, u + v).

Equations

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

theorem Q2Presentation.Lifting.card_Dline {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (A : Submodule (ZMod 2) V) : Nat.card ↥(Submodule.comap (LinearMap.fst (ZMod 2) V V + LinearMap.snd (ZMod 2) V V) A) = Nat.card V * Nat.card ↥A

The sum-line count: |{(u,v) | u + v ∈ A}| = |V|·|A|.

The conjugation-invariant duals X = (R^∨)^Y

def Q2Presentation.Lifting.conjInvDuals {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) : Submodule (ZMod 2) (Module.Dual (ZMod 2) (NAdd E))

The conjugation-invariant duals X = (R^∨)^Y = (R^∨)^C of an elementary kernel (consumer spelling of the manuscript's 𝒳_R, §7 l.3720–3723).

Equations

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

theorem Q2Presentation.Lifting.mem_conjInvDuals {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (f : Module.Dual (ZMod 2) (NAdd E)) : f ∈ conjInvDuals E ↔ ∀ (y : Yt.Y) (m : NAdd E), f ((conjEndN E y) m) = f m

theorem Q2Presentation.Lifting.conjInvDuals_kills_markedAug {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (q : Marking Yt.Y) (f : Module.Dual (ZMod 2) (NAdd E)) (hf : f ∈ conjInvDuals E) (x : NAdd E) : x ∈ markedAug (conjFamily E) q → f x = 0

Invariant duals kill the marked window (no cover needed: invariance at the marking generators is an instance of full invariance).

theorem Q2Presentation.Lifting.markedAug_le_coann {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (q : Marking Yt.Y) : markedAug (conjFamily E) q ≤ (conjInvDuals E).dualCoannihilator

The marked window lies in the coannihilator of the invariant duals.

theorem Q2Presentation.Lifting.markedAug_eq_coann_of_cover {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (q : Marking Yt.Y) (hcover : ∀ (y : Yt.Y), ∃ c ∈ Subgroup.closure (Set.range q), (conjFamily E).op (y * c⁻¹) = 1) : markedAug (conjFamily E) q = (conjInvDuals E).dualCoannihilator

The marked window is the coannihilator of the invariant duals under the marking cover: a vector killed by every invariant dual lies in the marked window, because a functional separating it from the window is generator-invariant (kills_markedAug_iff), hence fully invariant by the cover upgrade (invariant_of_gen_of_cover).

theorem Q2Presentation.Lifting.card_markedAug_of_cover {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (q : Marking Yt.Y) (hcover : ∀ (y : Yt.Y), ∃ c ∈ Subgroup.closure (Set.range q), (conjFamily E).op (y * c⁻¹) = 1) : Nat.card ↥(markedAug (conjFamily E) q) * Nat.card ↥(conjInvDuals E) = Nat.card (NAdd E)

The marked-window count: |markedAug|·|X| = |N| under the cover — the coannihilator dimension count at the invariant duals.