Generation of the tame target

theorem Q2Presentation.Induction.tame_target_generated {Yt : BoundaryFramedTarget} (F : BoundaryFrame Yt) : Subgroup.closure {(ProfiniteGrp.Hom.hom F.alpha) tameSigma, (ProfiniteGrp.Hom.hom F.alpha) tameTau} = ⊤

The finite tame target is generated by the images of σ, τ.

Head simplicity

def Q2Presentation.Induction.moduleSubgroup {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (U : Submodule (ZMod 2) (Lifting.NAdd (mstageKernel chief K hR))) : Subgroup p.fst.Y

The Y-subgroup underlying an invariant submodule of the kernel module.

Equations

• Q2Presentation.Induction.moduleSubgroup chief K hR U = Subgroup.map K.Ksub.subtype (Subgroup.toAddSubgroup.symm ((AddSubgroup.toZModSubmodule 2).symm U))

theorem Q2Presentation.Induction.mem_moduleSubgroup {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (U : Submodule (ZMod 2) (Lifting.NAdd (mstageKernel chief K hR))) (y : p.fst.Y) : y ∈ moduleSubgroup chief K hR U ↔ ∃ (hy : y ∈ K.Ksub), Additive.ofMul ⟨y, hy⟩ ∈ U

theorem Q2Presentation.Induction.head_submodule_dichotomy {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (V' : Submodule (ZMod 2) (HeadMod chief K hR)) (hinv : ∀ (y : p.fst.Y), ∀ v ∈ V', (headOp chief K hR y) v ∈ V') : V' = ⊥ ∨ V' = ⊤

Head simplicity: a conjugation-invariant submodule of the head is ⊥ or ⊤.