The tame images and generation

theorem Q2Presentation.Induction.piY_marking {p : FramedPair} (F : BoundaryFrame p.fst) (q : Marking p.fst.Y) (hframe : ∀ (a : Gen), p.fst.qYMap (q a) = (ProfiniteGrp.Hom.hom F.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))) (a : Gen) : p.fst.piY (q a) = (ProfiniteGrp.Hom.hom F.alpha) ((ProfiniteGrp.Hom.hom (CategoryTheory.Limits.pullback.fst nu_t nu_2)) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a)))

The tame image of a generator slot is the framed image of its tame boundary value.

theorem Q2Presentation.Induction.piY_marking_sigma {p : FramedPair} (F : BoundaryFrame p.fst) (q : Marking p.fst.Y) (hframe : ∀ (a : Gen), p.fst.qYMap (q a) = (ProfiniteGrp.Hom.hom F.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))) : p.fst.piY (q Gen.sigma) = (ProfiniteGrp.Hom.hom F.alpha) tameSigma

theorem Q2Presentation.Induction.piY_marking_tau {p : FramedPair} (F : BoundaryFrame p.fst) (q : Marking p.fst.Y) (hframe : ∀ (a : Gen), p.fst.qYMap (q a) = (ProfiniteGrp.Hom.hom F.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))) : p.fst.piY (q Gen.tau) = (ProfiniteGrp.Hom.hom F.alpha) tameTau

theorem Q2Presentation.Induction.piY_marking_generates {p : FramedPair} (F : BoundaryFrame p.fst) (q : Marking p.fst.Y) (hframe : ∀ (a : Gen), p.fst.qYMap (q a) = (ProfiniteGrp.Hom.hom F.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))) : Subgroup.closure {p.fst.piY (q Gen.sigma), p.fst.piY (q Gen.tau)} = ⊤

The tame images of the marking generate H.

theorem Q2Presentation.Induction.lift_decomposition {p : FramedPair} (F : BoundaryFrame p.fst) (q : Marking p.fst.Y) (hframe : ∀ (a : Gen), p.fst.qYMap (q a) = (ProfiniteGrp.Hom.hom F.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))) (y : p.fst.Y) : ∃ w ∈ Subgroup.closure {q Gen.sigma, q Gen.tau}, y * w⁻¹ ∈ p.fst.LY

Lift decomposition: every element of Y is a word in the marking's σ, τ-values times a wild element.

Fixed-space invariance and the dichotomy

def Q2Presentation.Induction.tauFixed {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (q : Marking p.fst.Y) : Submodule (ZMod 2) (HeadMod chief K hR)

The τ-fixed space, as the kernel of 1 + Cτ (char 2).

Equations

• Q2Presentation.Induction.tauFixed chief K hR q = (1 + (Q2Presentation.Induction.headFamily chief K hR).op (q Q2Presentation.Gen.tau)).ker

theorem Q2Presentation.Induction.mem_tauFixed {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (q : Marking p.fst.Y) (x : HeadMod chief K hR) : x ∈ tauFixed chief K hR q ↔ ((headFamily chief K hR).op (q Gen.tau)) x = x

theorem Q2Presentation.Induction.tauFixed_pow {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (q : Marking p.fst.Y) (x : HeadMod chief K hR) (hx : ((headFamily chief K hR).op (q Gen.tau)) x = x) (k : ℕ) : ((headFamily chief K hR).op (q Gen.tau) ^ k) x = x

Fixed vectors are fixed by all powers.

theorem Q2Presentation.Induction.tauFixed_sigma_stable {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (F : BoundaryFrame p.fst) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (mstageKernel chief K hR).N ⋯ ⋯) (TorsorProgram.quotientFrame p.fst (mstageKernel chief K hR).N ⋯ ⋯ F)) (q : Marking p.fst.Y) (hlift : ∀ (a : Gen), (QuotientGroup.mk' (mstageKernel chief K hR).N) (q a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a)) (x : HeadMod chief K hR) (hx : x ∈ tauFixed chief K hR q) : ((headFamily chief K hR).op (q Gen.sigma)) x ∈ tauFixed chief K hR q

Cσ preserves the τ-fixed space (the commutation law).

theorem Q2Presentation.Induction.tau_dichotomy {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (F : BoundaryFrame p.fst) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (mstageKernel chief K hR).N ⋯ ⋯) (TorsorProgram.quotientFrame p.fst (mstageKernel chief K hR).N ⋯ ⋯ F)) (q : Marking p.fst.Y) (hlift : ∀ (a : Gen), (QuotientGroup.mk' (mstageKernel chief K hR).N) (q a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a)) (hframe : ∀ (a : Gen), p.fst.qYMap (q a) = (ProfiniteGrp.Hom.hom F.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))) : (headFamily chief K hR).op (q Gen.tau) = 1 ∨ tauFixed chief K hR q = ⊥

The τ-dichotomy: Cτ = 1 or the τ-fixed space is trivial.

theorem Q2Presentation.Induction.hTone_of_ne_one {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (F : BoundaryFrame p.fst) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (mstageKernel chief K hR).N ⋯ ⋯) (TorsorProgram.quotientFrame p.fst (mstageKernel chief K hR).N ⋯ ⋯ F)) (q : Marking p.fst.Y) (hlift : ∀ (a : Gen), (QuotientGroup.mk' (mstageKernel chief K hR).N) (q a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a)) (hframe : ∀ (a : Gen), p.fst.qYMap (q a) = (ProfiniteGrp.Hom.hom F.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))) (hne : (headFamily chief K hR).op (q Gen.tau) ≠ 1) : IsUnit (1 + (headFamily chief K hR).op (q Gen.tau))

hTone on the nontrivial branch: if Cτ ≠ 1 then 1 + Cτ is a unit.