Q2Presentation.Lifting.SectionDischarge

source

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

Submodule (ZMod 2) V

The wild-fixed submodule V^{L_Y}.

Equations

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

Instances For

source

theorem Q2Presentation.Lifting.mem_famWildFixed {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (v : V) :

v ∈ famWildFixed Φ ↔ ∀ y ∈ Yt.LY, (Φ.op y) v = v

source

theorem Q2Presentation.Lifting.famWildFixed_stable {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (z : Yt.Y) (v : V) (hv : v ∈ famWildFixed Φ) :

(Φ.op z) v ∈ famWildFixed Φ

The wild-fixed space is stable under every operator (normality).

source

theorem Q2Presentation.Lifting.famWildFixed_ne_bot {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) [Finite V] [Nontrivial V] :

famWildFixed Φ ≠ ⊥

Nonzero wild-fixed vectors exist (lem:simpletame's counting core).

source

theorem Q2Presentation.Lifting.famWild_ops_one {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) [Finite V] [Nontrivial V] (hsimple : ∀ (U : Submodule (ZMod 2) V), (∀ m ∈ U, (Φ.op (q Gen.sigma)) m ∈ U) → (∀ m ∈ U, (Φ.op (q Gen.tau)) m ∈ U) → U = ⊥ ∨ U = ⊤) (y : Yt.Y) :

y ∈ Yt.LY → Φ.op y = 1

Wild triviality on a σ/τ-simple nontrivial module.

source

theorem Q2Presentation.Lifting.famOp_of_ker_piY {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) [Finite V] [Nontrivial V] (hsimple : ∀ (U : Submodule (ZMod 2) V), (∀ m ∈ U, (Φ.op (q Gen.sigma)) m ∈ U) → (∀ m ∈ U, (Φ.op (q Gen.tau)) m ∈ U) → U = ⊥ ∨ U = ⊤) (y : Yt.Y) (hy : Yt.piY y = 1) :

Φ.op y = 1

Operators of tame-kernel elements are trivial.

source

theorem Q2Presentation.Lifting.famOp_tau_pow {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) [Finite V] [Nontrivial V] (hsimple : ∀ (U : Submodule (ZMod 2) V), (∀ m ∈ U, (Φ.op (q Gen.sigma)) m ∈ U) → (∀ m ∈ U, (Φ.op (q Gen.tau)) m ∈ U) → U = ⊥ ∨ U = ⊤) :

Φ.op (q Gen.tau) ^ orderOf (Yt.piY (q Gen.tau)) = 1

The τ-operator has the τ̄-order as a power-period.

source

theorem Q2Presentation.Lifting.tame_comm_of_rconj {H : Type} [Group H] [Finite H] (σb τb : H) (hrel : rconj τb σb = τb ^ 2) (hodd : Odd (orderOf τb)) :

σb * τb * σb⁻¹ = τb ^ ((orderOf τb + 1) / 2)

The H-level commutation law from the raw tame relation and odd order: σ̄ τ̄ σ̄⁻¹ = τ̄^{(e+1)/2}.

source

theorem Q2Presentation.Lifting.famOp_comm_of_target {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) [Finite V] [Nontrivial V] (hsimple : ∀ (U : Submodule (ZMod 2) V), (∀ m ∈ U, (Φ.op (q Gen.sigma)) m ∈ U) → (∀ m ∈ U, (Φ.op (q Gen.tau)) m ∈ U) → U = ⊥ ∨ U = ⊤) (hrel : rconj (Yt.piY (q Gen.tau)) (Yt.piY (q Gen.sigma)) = Yt.piY (q Gen.tau) ^ 2) :

Φ.op (q Gen.tau) * Φ.op (q Gen.sigma) = Φ.op (q Gen.sigma) * Φ.op (q Gen.tau) ^ ((orderOf (Yt.piY (q Gen.tau)) + 1) / 2)

The operator commutation law descends from the raw H-level tame relation.

source

theorem Q2Presentation.Lifting.famNontriv_sigma_tau {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) [Finite V] [Nontrivial V] (hsimple : ∀ (U : Submodule (ZMod 2) V), (∀ m ∈ U, (Φ.op (q Gen.sigma)) m ∈ U) → (∀ m ∈ U, (Φ.op (q Gen.tau)) m ∈ U) → U = ⊥ ∨ U = ⊤) (haction : ¬∀ (y : Yt.Y), Φ.op y = 1) (hdecomp : ∀ (y : Yt.Y), ∃ w ∈ Subgroup.closure {q Gen.sigma, q Gen.tau}, y * w⁻¹ ∈ Yt.LY) :

¬(Φ.op (q Gen.sigma) = 1 ∧ Φ.op (q Gen.tau) = 1)

Nontrivial action forces a nontrivial σ- or τ-operator.

source

theorem Q2Presentation.Lifting.famTau_order_dvd {Yt : BoundaryFramedTarget} [Finite Yt.Y] (q : Marking Yt.Y) :

orderOf (Yt.piY (q Gen.tau)) ∣ Nat.card Yt.Y

The τ̄-order divides the group order.

source

theorem Q2Presentation.Lifting.famRows_surjective_of_simple_structured {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) [Finite V] [Nontrivial V] (htwo : 2 ∣ Nat.card Yt.Y) (hx1LY : q Gen.x1 ∈ Yt.LY) (hsimple : ∀ (U : Submodule (ZMod 2) V), (∀ m ∈ U, (Φ.op (q Gen.sigma)) m ∈ U) → (∀ m ∈ U, (Φ.op (q Gen.tau)) m ∈ U) → U = ⊥ ∨ U = ⊤) (haction : ¬∀ (y : Yt.Y), Φ.op y = 1) (hdecomp : ∀ (y : Yt.Y), ∃ w ∈ Subgroup.closure {q Gen.sigma, q Gen.tau}, y * w⁻¹ ∈ Yt.LY) (hrel : rconj (Yt.piY (q Gen.tau)) (Yt.piY (q Gen.sigma)) = Yt.piY (q Gen.tau) ^ 2) (uv : V × V) :

∃ (n : Gen → V), (foxShadowGen Φ.op q n Q2Word.tameRelator, foxShadowGen Φ.op q n Q2Word.wildRelator) = uv

Structured simple-module row surjectivity: every hypothesis of the abstract simple case discharges from the framed structure, σ/τ-simplicity, a nontrivial action, the word decomposition, and the H-level tame relation.