e divides the ω₂-residue #
theorem
Q2Presentation.Induction.tau_order_dvd_residue
{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))
:
The order of τ̄ divides the ω₂-residue mod |Y|.
The norm telescopes into the fixed space #
theorem
Q2Presentation.Induction.headNorm_telescope
{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) * ∑ i ∈ Finset.range (orderOf (p.fst.piY (q Gen.tau))), (headFamily chief K hR).op (q Gen.tau) ^ i = ∑ i ∈ Finset.range (orderOf (p.fst.piY (q Gen.tau))), (headFamily chief K hR).op (q Gen.tau) ^ i
Cτ · P = P for the order-length norm.
theorem
Q2Presentation.Induction.headNorm_eq_zero
{p : FramedPair}
(chief : FirstNonScalarChiefFactor p)
(K : KernelMinimal chief.toNonScalarChiefFactor)
(hR : Nat.card ↥(kernelFrattini K) = 1)
(q : Marking p.fst.Y)
(hbot : tauFixed chief K hR q = ⊥)
:
∑ i ∈ Finset.range (orderOf (p.fst.piY (q Gen.tau))), (headFamily chief K hR).op (q Gen.tau) ^ i = 0
On the trivial-fixed-space branch, the norm vanishes.
theorem
Q2Presentation.Induction.headSum_residue_eq_zero
{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))
(hbot : tauFixed chief K hR q = ⊥)
:
On the trivial-fixed-space branch, the ω₂-length sum vanishes.