theorem Q2Presentation.Induction.marking_defect_mem {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)) (w : GExpr) (hw1 : (w.eval fun (a : Gen) => (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a)) = 1) : w.eval q ∈ K.Ksub

The relator defect of a marking over g lies in the kernel.

theorem Q2Presentation.Induction.tame_relation_at_target {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)) : rconj (p.fst.piY (q Gen.tau)) (p.fst.piY (q Gen.sigma)) = p.fst.piY (q Gen.tau) ^ 2

The tame relation holds at the tame images: rconj τ̄ σ̄ = τ̄².

theorem Q2Presentation.Induction.tau_bar_odd_order {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)) : Odd (orderOf (p.fst.piY (q Gen.tau)))

τ̄ has odd order.

def Q2Presentation.Induction.headFamily {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) : Lifting.OperatorFamily p.fst (HeadMod chief K hR)

The head family (the descended conjugation operators).

Equations

• Q2Presentation.Induction.headFamily chief K hR = (Q2Presentation.Lifting.conjFamily (Q2Presentation.Induction.mstageKernel chief K hR)).descend (Q2Presentation.Induction.radicalW chief K hR) ⋯

theorem Q2Presentation.Induction.headFamily_op {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (y : p.fst.Y) : (headFamily chief K hR).op y = headOp chief K hR y

The head family agrees with headOp.

theorem Q2Presentation.Induction.headFamily_ker_eq_one {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (y : p.fst.Y) (hy : p.fst.piY y = 1) : (headFamily chief K hR).op y = 1

Elements of ker π_Y act trivially on the head.

theorem Q2Presentation.Induction.headOp_tau_pow_order {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (q : Marking p.fst.Y) : (headFamily chief K hR).op (q Gen.tau) ^ orderOf (p.fst.piY (q Gen.tau)) = 1

Cτ has order dividing e = |τ̄|.

theorem Q2Presentation.Induction.headOp_comm_law {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)) : (headFamily chief K hR).op (q Gen.tau) * (headFamily chief K hR).op (q Gen.sigma) = (headFamily chief K hR).op (q Gen.sigma) * (headFamily chief K hR).op (q Gen.tau) ^ ((orderOf (p.fst.piY (q Gen.tau)) + 1) / 2)

The head commutation law: Cτ · Cσ = Cσ · Cτ^m for m = (e+1)/2.