structure Q2Presentation.Lifting.OperatorFamily (Yt : BoundaryFramedTarget) (V : Type) [AddCommGroup V] [Module (ZMod 2) V] : Type

An operator family with the conjugation antihomomorphism laws.

• op : Yt.Y → Module.End (ZMod 2) V
• op_one : self.op 1 = 1
• op_mul (y₁ y₂ : Yt.Y) : self.op (y₁ * y₂) = self.op y₂ * self.op y₁

theorem Q2Presentation.Lifting.OperatorFamily.op_inv_mul_cancel {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (y : Yt.Y) : Φ.op y⁻¹ * Φ.op y = 1

theorem Q2Presentation.Lifting.OperatorFamily.op_mul_inv_cancel {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (y : Yt.Y) : Φ.op y * Φ.op y⁻¹ = 1

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

theorem Q2Presentation.Lifting.OperatorFamily.op_inv_apply {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (y : Yt.Y) (x : V) : (Φ.op y⁻¹) ((Φ.op y) x) = x

theorem Q2Presentation.Lifting.OperatorFamily.op_apply_inv {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (y : Yt.Y) (x : V) : (Φ.op y) ((Φ.op y⁻¹) x) = x

theorem Q2Presentation.Lifting.OperatorFamily.op_pow {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (y : Yt.Y) (k : ℕ) : Φ.op (y ^ k) = Φ.op y ^ k

def Q2Presentation.Lifting.conjFamily {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) : OperatorFamily Yt (NAdd E)

The concrete conjugation family of an elementary kernel.

Equations

• Q2Presentation.Lifting.conjFamily E = { op := Q2Presentation.Lifting.conjEndN E, op_one := ⋯, op_mul := ⋯ }

@[simp]

theorem Q2Presentation.Lifting.conjFamily_op {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) : (conjFamily E).op = conjEndN E

def Q2Presentation.Lifting.OperatorFamily.descend {Yt : BoundaryFramedTarget} {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (W : Submodule (ZMod 2) V) (hW : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) : OperatorFamily Yt (V ⧸ W)

Descend a family along an invariant submodule.

Equations

• Φ.descend W hW = { op := fun (y : Yt.Y) => W.mapQ W (Φ.op y) ⋯, op_one := ⋯, op_mul := ⋯ }

def Q2Presentation.Lifting.OperatorFamily.restrict {Yt : BoundaryFramedTarget} {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (W : Submodule (ZMod 2) V) (hW : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) : OperatorFamily Yt ↥W

Restrict a family to an invariant submodule.

Equations

• Φ.restrict W hW = { op := fun (y : Yt.Y) => LinearMap.restrict (Φ.op y) ⋯, op_one := ⋯, op_mul := ⋯ }

theorem Q2Presentation.Lifting.OperatorFamily.restrict_comm {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (W : Submodule (ZMod 2) V) (hW : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) (y : Yt.Y) (w : ↥W) : W.subtype (((Φ.restrict W hW).op y) w) = (Φ.op y) (W.subtype w)

Restriction commutes with the inclusion pointwise.

theorem Q2Presentation.Lifting.OperatorFamily.descend_comm {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (W : Submodule (ZMod 2) V) (hW : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) (y : Yt.Y) (v : V) : W.mkQ ((Φ.op y) v) = ((Φ.descend W hW).op y) (W.mkQ v)

Descent commutes with the projection pointwise.