Generic invariance from generator stability

theorem Q2Presentation.Induction.head_invariant_of_gen_stable {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (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))) (V : Submodule (ZMod 2) (HeadMod chief K hR)) (hσ : ∀ x ∈ V, ((headFamily chief K hR).op (q Gen.sigma)) x ∈ V) (hτ : ∀ x ∈ V, ((headFamily chief K hR).op (q Gen.tau)) x ∈ V) (y : p.fst.Y) (x : HeadMod chief K hR) : x ∈ V → (headOp chief K hR y) x ∈ V

Stability at the two generator slots gives stability for the whole conjugation family.

The nontrivial action reaches the head

theorem Q2Presentation.Induction.head_action_nontrivial {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) : ∃ (y : p.fst.Y) (x : HeadMod chief K hR), (headOp chief K hR y) x ≠ x

The chief nontriviality reaches the head module.

The σ-fixed space and hSone

def Q2Presentation.Induction.sigmaFixed {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.sigmaFixed chief K hR q = (1 + (Q2Presentation.Induction.headFamily chief K hR).op (q Q2Presentation.Gen.sigma)).ker

theorem Q2Presentation.Induction.mem_sigmaFixed {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 ∈ sigmaFixed chief K hR q ↔ ((headFamily chief K hR).op (q Gen.sigma)) x = x

theorem Q2Presentation.Induction.sigma_dichotomy {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (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))) (hT : (headFamily chief K hR).op (q Gen.tau) = 1) : (headFamily chief K hR).op (q Gen.sigma) = 1 ∨ sigmaFixed chief K hR q = ⊥

The σ-dichotomy on the Cτ = 1 branch.

theorem Q2Presentation.Induction.all_ops_one {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (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))) (hT : (headFamily chief K hR).op (q Gen.tau) = 1) (hS : (headFamily chief K hR).op (q Gen.sigma) = 1) (y : p.fst.Y) : headOp chief K hR y = 1

If both generator operators are trivial, every head operator is.

theorem Q2Presentation.Induction.hSone_of_tau_eq_one {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (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))) (hT : (headFamily chief K hR).op (q Gen.tau) = 1) : IsUnit (1 + (headFamily chief K hR).op (q Gen.sigma))

hSone on the Cτ = 1 branch: 1 + Cσ is a unit.