theorem Q2Presentation.Lifting.famWord_stable {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) [Finite V] (U : Submodule (ZMod 2) V) (hUσ : ∀ m ∈ U, (Φ.op (q Gen.sigma)) m ∈ U) (hUτ : ∀ m ∈ U, (Φ.op (q Gen.tau)) m ∈ U) (w : Yt.Y) : w ∈ Subgroup.closure {q Gen.sigma, q Gen.tau} → ∀ x ∈ U, (Φ.op w) x ∈ U

Word-closure stability from σ/τ-stability (finite inverses).

theorem Q2Presentation.Lifting.section_nontrivial {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (W' W : Submodule (ZMod 2) V) (hlt : W' < W) : Nontrivial (↥W ⧸ Submodule.comap W.subtype W')

A strict stable pair has a nontrivial section.

def Q2Presentation.Lifting.pullSection {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (W' W : Submodule (ZMod 2) V) (U : Submodule (ZMod 2) (↥W ⧸ Submodule.comap W.subtype W')) : Submodule (ZMod 2) V

The pullback of a section submodule to the ambient module.

Equations

• Q2Presentation.Lifting.pullSection W' W U = Submodule.map W.subtype (Submodule.comap (Submodule.comap W.subtype W').mkQ U)

theorem Q2Presentation.Lifting.mem_pullSection {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (W' W : Submodule (ZMod 2) V) (U : Submodule (ZMod 2) (↥W ⧸ Submodule.comap W.subtype W')) (x : V) : x ∈ pullSection W' W U ↔ ∃ (z : ↥W), (Submodule.comap W.subtype W').mkQ z ∈ U ∧ ↑z = x

theorem Q2Presentation.Lifting.pullSection_le {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (W' W : Submodule (ZMod 2) V) (U : Submodule (ZMod 2) (↥W ⧸ Submodule.comap W.subtype W')) : pullSection W' W U ≤ W

theorem Q2Presentation.Lifting.le_pullSection {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (W' W : Submodule (ZMod 2) V) (hle : W' ≤ W) (U : Submodule (ZMod 2) (↥W ⧸ Submodule.comap W.subtype W')) : W' ≤ pullSection W' W U

theorem Q2Presentation.Lifting.pullSection_eq_W'_iff {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (W' W : Submodule (ZMod 2) V) (hle : W' ≤ W) (U : Submodule (ZMod 2) (↥W ⧸ Submodule.comap W.subtype W')) : pullSection W' W U = W' ↔ U = ⊥

theorem Q2Presentation.Lifting.pullSection_eq_W_iff {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (W' W : Submodule (ZMod 2) V) (U : Submodule (ZMod 2) (↥W ⧸ Submodule.comap W.subtype W')) : pullSection W' W U = W ↔ U = ⊤

theorem Q2Presentation.Lifting.pullSection_op_mem {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (W' W : Submodule (ZMod 2) V) (hW : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) (hW' : ∀ (y : Yt.Y), ∀ m ∈ W', (Φ.op y) m ∈ W') (hle : W' ≤ W) (U : Submodule (ZMod 2) (↥W ⧸ Submodule.comap W.subtype W')) (y : Yt.Y) (hy : ∀ m ∈ U, ((sectionFamily Φ W' W hW hW').op y) m ∈ U) (x : V) : x ∈ pullSection W' W U → (Φ.op y) x ∈ pullSection W' W U

Section-stability at an operator pulls back.

theorem Q2Presentation.Lifting.section_dichotomy_of_max {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (W' W : Submodule (ZMod 2) V) (hW : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) (hW' : ∀ (y : Yt.Y), ∀ m ∈ W', (Φ.op y) m ∈ W') (hlt : W' < W) (hmax : ∀ U < W, W' ≤ U → (∀ (y : Yt.Y), ∀ m ∈ U, (Φ.op y) m ∈ U) → U = W') (U : Submodule (ZMod 2) (↥W ⧸ Submodule.comap W.subtype W')) (hU : ∀ (y : Yt.Y), ∀ m ∈ U, ((sectionFamily Φ W' W hW hW').op y) m ∈ U) : U = ⊥ ∨ U = ⊤

Fully stable section submodules collapse under maximality.

theorem Q2Presentation.Lifting.sectionWild_ops_one {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (W' W : Submodule (ZMod 2) V) (hW : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) (hW' : ∀ (y : Yt.Y), ∀ m ∈ W', (Φ.op y) m ∈ W') [Finite V] (hlt : W' < W) (hmax : ∀ U < W, W' ≤ U → (∀ (y : Yt.Y), ∀ m ∈ U, (Φ.op y) m ∈ U) → U = W') (y : Yt.Y) : y ∈ Yt.LY → (sectionFamily Φ W' W hW hW').op y = 1

Wild triviality at the section from maximality.

theorem Q2Presentation.Lifting.section_simple_of_max {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : OperatorFamily Yt V) (q : Marking Yt.Y) (W' W : Submodule (ZMod 2) V) (hW : ∀ (y : Yt.Y), ∀ m ∈ W, (Φ.op y) m ∈ W) (hW' : ∀ (y : Yt.Y), ∀ m ∈ W', (Φ.op y) m ∈ W') [Finite V] (hlt : W' < W) (hmax : ∀ U < W, W' ≤ U → (∀ (y : Yt.Y), ∀ m ∈ U, (Φ.op y) m ∈ U) → U = W') (hdecomp : ∀ (y : Yt.Y), ∃ w ∈ Subgroup.closure {q Gen.sigma, q Gen.tau}, y * w⁻¹ ∈ Yt.LY) (U : Submodule (ZMod 2) (↥W ⧸ Submodule.comap W.subtype W')) : (∀ m ∈ U, ((sectionFamily Φ W' W hW hW').op (q Gen.sigma)) m ∈ U) → (∀ m ∈ U, ((sectionFamily Φ W' W hW hW').op (q Gen.tau)) m ∈ U) → U = ⊥ ∨ U = ⊤

σ/τ-simplicity of the section from maximality and the word decomposition.