def Q2Presentation.Lifting.dualFamily {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) : OperatorFamily Yt (Module.Dual (ZMod 2) V)

The dual operator family.

Equations

• Q2Presentation.Lifting.dualFamily Φ = { op := fun (y : Yt.Y) => Q2Presentation.Lifting.dualOp Φ y, op_one := ⋯, op_mul := ⋯ }

@[simp]

theorem Q2Presentation.Lifting.dualFamily_op {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (y : Yt.Y) : (dualFamily Φ).op y = dualOp Φ y

theorem Q2Presentation.Lifting.famRows_smul {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n : Gen → V) (c : ZMod 2) (w : GExpr) : foxShadowGen Φ.op q (c • n) w = c • foxShadowGen Φ.op q n w

ZMod-2 scalar action from additivity.

def Q2Presentation.Lifting.famRowsMap {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) : (Gen → V) →ₗ[ZMod 2] V × V

The family-generic row map as a linear map.

Equations

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

theorem Q2Presentation.Lifting.famRowsMap_apply {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (n : Gen → V) : (famRowsMap Φ q) n = (foxShadowGen Φ.op q n Q2Word.tameRelator, foxShadowGen Φ.op q n Q2Word.wildRelator)

def Q2Presentation.Lifting.famCobMap {Yt : BoundaryFramedTarget} {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) : V →ₗ[ZMod 2] Gen → V

The generic coboundary as a linear map — the d⁰.

Equations

• Q2Presentation.Lifting.famCobMap Φ q = { toFun := fun (a : V) => Q2Presentation.Lifting.coboundary Φ q a, map_add' := ⋯, map_smul' := ⋯ }

theorem Q2Presentation.Lifting.famCobMap_apply {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (a : V) : (famCobMap Φ q) a = coboundary Φ q a

def Q2Presentation.Lifting.famInvariants {Yt : BoundaryFramedTarget} {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) : Submodule (ZMod 2) V

Invariant vectors of the family.

Equations

• Q2Presentation.Lifting.famInvariants Φ = { carrier := {v : V | ∀ (y : Yt.Y), (Φ.op y) v = v}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem Q2Presentation.Lifting.mem_famInvariants {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (v : V) : v ∈ famInvariants Φ ↔ ∀ (y : Yt.Y), (Φ.op y) v = v

theorem Q2Presentation.Lifting.famInvariants_dual {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (lam : Module.Dual (ZMod 2) V) : lam ∈ famInvariants (dualFamily Φ) ↔ ∀ (y : Yt.Y) (x : V), lam ((Φ.op y) x) = lam x

Invariant duals are the dual family's invariants.