Q2Presentation.Lifting.SimpleSectionRows

source

theorem Q2Presentation.Lifting.odd_dvd_omega2_residue {Yt : BoundaryFramedTarget} [Finite Yt.Y] (e : ℕ) (hodd : Odd e) (heY : e ∣ Nat.card Yt.Y) :

e ∣ (omega2Mod (Nat.card Yt.Y)).val

An odd divisor of the group order divides the ω₂-residue length.

source

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

Submodule (ZMod 2) V

The τ-fixed space of a marking's family.

Equations

Q2Presentation.Lifting.famTauFixed Φ q = (1 + Φ.op (q Q2Presentation.Gen.tau)).ker

Instances For

source

theorem Q2Presentation.Lifting.mem_famTauFixed {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (x : V) :

x ∈ famTauFixed Φ q ↔ (Φ.op (q Gen.tau)) x = x

source

theorem Q2Presentation.Lifting.famTauFixed_pow {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (x : V) (hx : x ∈ famTauFixed Φ q) (k : ℕ) :

(Φ.op (q Gen.tau) ^ k) x = x

source

theorem Q2Presentation.Lifting.famTauFixed_sigma_stable {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (e : ℕ) (hcomm : Φ.op (q Gen.tau) * Φ.op (q Gen.sigma) = Φ.op (q Gen.sigma) * Φ.op (q Gen.tau) ^ ((e + 1) / 2)) (x : V) (hx : x ∈ famTauFixed Φ q) :

(Φ.op (q Gen.sigma)) x ∈ famTauFixed Φ q

σ-stability of the τ-fixed space, from the commutation law.

source

theorem Q2Presentation.Lifting.famTau_dichotomy {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (e : ℕ) (hsimple : ∀ (U : Submodule (ZMod 2) V), (∀ m ∈ U, (Φ.op (q Gen.sigma)) m ∈ U) → (∀ m ∈ U, (Φ.op (q Gen.tau)) m ∈ U) → U = ⊥ ∨ U = ⊤) (hcomm : Φ.op (q Gen.tau) * Φ.op (q Gen.sigma) = Φ.op (q Gen.sigma) * Φ.op (q Gen.tau) ^ ((e + 1) / 2)) :

Φ.op (q Gen.tau) = 1 ∨ famTauFixed Φ q = ⊥

The τ-dichotomy on a σ/τ-simple module.

source

theorem Q2Presentation.Lifting.famOne_add_isUnit {V : Type} [AddCommGroup V] [Module (ZMod 2) V] [Finite V] (C : Module.End (ZMod 2) V) (hbot : (1 + C).ker = ⊥) :

IsUnit (1 + C)

Trivial kernel of 1 + C upgrades to invertibility on a finite module.

source

theorem Q2Presentation.Lifting.famSone_of_tau_eq_one {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) [Finite 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 = ⊤) (hT : Φ.op (q Gen.tau) = 1) (hSne : Φ.op (q Gen.sigma) ≠ 1) :

IsUnit (1 + Φ.op (q Gen.sigma))

On the σ/τ-simple module with Cτ = 1 and nontrivial σ, the operator 1 + Cσ is invertible.

source

theorem Q2Presentation.Lifting.famNorm_telescope {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (e : ℕ) (hCe : Φ.op (q Gen.tau) ^ e = 1) :

Φ.op (q Gen.tau) * ∑ i ∈ Finset.range e, Φ.op (q Gen.tau) ^ i = ∑ i ∈ Finset.range e, Φ.op (q Gen.tau) ^ i

The τ-norm telescope: Cτ · Σ = Σ for the order-length norm.

source

theorem Q2Presentation.Lifting.famNorm_eq_zero {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (e : ℕ) (hCe : Φ.op (q Gen.tau) ^ e = 1) (hbot : famTauFixed Φ q = ⊥) :

∑ i ∈ Finset.range e, Φ.op (q Gen.tau) ^ i = 0

On the τ-regular branch the order-length norm vanishes.

source

theorem Q2Presentation.Lifting.famSum_residue_eq_zero {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (e : ℕ) (hCe : Φ.op (q Gen.tau) ^ e = 1) (hodd : Odd e) (heY : e ∣ Nat.card Yt.Y) (hbot : famTauFixed Φ q = ⊥) :

∑ i ∈ Finset.range (omega2Mod (Nat.card Yt.Y)).val, Φ.op (q Gen.tau) ^ i = 0

On the τ-regular branch the ω₂-length sum vanishes.

source

theorem Q2Presentation.Lifting.famPop_of_sum {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (hx1 : Φ.op (q Gen.x1) = 1) (hsum : ∑ i ∈ Finset.range (omega2Mod (Nat.card Yt.Y)).val, Φ.op (q Gen.tau) ^ i = 0) :

∑ i ∈ Finset.range (omega2Mod (Nat.card Yt.Y)).val, Φ.op ((Q2Word.x1.mul Q2Word.tau).eval q) ^ i = 0

With a trivial x₁-operator the case-(ii) sum reduces to the τ-sum.

source

theorem Q2Presentation.Lifting.famRows_surjective_of_simple {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) [Finite V] (htwo : 2 ∣ Nat.card Yt.Y) (hx1 : Φ.op (q Gen.x1) = 1) (hsimple : ∀ (U : Submodule (ZMod 2) V), (∀ m ∈ U, (Φ.op (q Gen.sigma)) m ∈ U) → (∀ m ∈ U, (Φ.op (q Gen.tau)) m ∈ U) → U = ⊥ ∨ U = ⊤) (hnontriv : ¬(Φ.op (q Gen.sigma) = 1 ∧ Φ.op (q Gen.tau) = 1)) (e : ℕ) (hCe : Φ.op (q Gen.tau) ^ e = 1) (hodd : Odd e) (heY : e ∣ Nat.card Yt.Y) (hcomm : Φ.op (q Gen.tau) * Φ.op (q Gen.sigma) = Φ.op (q Gen.sigma) * Φ.op (q Gen.tau) ^ ((e + 1) / 2)) (uv : V × V) :

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

Abstract simple-module row surjectivity (lem:simplenormalforms): on a σ/τ-simple module with nontrivial action, trivial x₁-operator, and the tame relations, the rows are surjective.