Q2Presentation.Induction.MstageDiamond

source

theorem Q2Presentation.Induction.ops_one_of_card_two {Yt : BoundaryFramedTarget} [Finite Yt.Y] {V : Type} [AddCommGroup V] [Module (ZMod 2) V] (Φ : Lifting.OperatorFamily Yt V) (hcard : Nat.card V = 2) (y : Yt.Y) :

Φ.op y = 1

On a two-element module every family operator is the identity.

source

theorem Q2Presentation.Induction.mstage_card_ne_two {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) :

Nat.card (Lifting.NAdd (mstageKernel chief K hR)) ≠ 2

The mstage layer never has exactly two elements: operators would be trivial and a nonzero functional invariant, contradicting the proven invariant vanishing.

source

theorem Q2Presentation.Induction.mstage_card_Y_four {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (hN : 1 < Nat.card (Lifting.NAdd (mstageKernel chief K hR))) :

4 ∣ Nat.card p.fst.Y

4 divides |Y| whenever the mstage layer is nontrivial.

source

theorem Q2Presentation.Induction.mstage_marking_covers {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (mstageKernel chief K hR).N ⋯ ⋯) (TorsorProgram.quotientFrame p.fst (mstageKernel chief K hR).N ⋯ ⋯ p.snd)) (q : Marking p.fst.Y) (hlift : ∀ (a : Gen), (QuotientGroup.mk' (mstageKernel chief K hR).N) (q a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a)) (y : p.fst.Y) :

∃ c ∈ Subgroup.closure (Set.range q), y * c⁻¹ ∈ (mstageKernel chief K hR).N

The marking covers Y modulo the mstage kernel.

source

theorem Q2Presentation.Induction.mstage_hcover {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (mstageKernel chief K hR).N ⋯ ⋯) (TorsorProgram.quotientFrame p.fst (mstageKernel chief K hR).N ⋯ ⋯ p.snd)) (q : Marking p.fst.Y) (hlift : ∀ (a : Gen), (QuotientGroup.mk' (mstageKernel chief K hR).N) (q a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a)) (y : p.fst.Y) :

∃ c ∈ Subgroup.closure (Set.range q), (Lifting.conjFamily (mstageKernel chief K hR)).op (y * c⁻¹) = 1

The cover in operator form.

source

theorem Q2Presentation.Induction.mstage_relator_tame_op_one {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (mstageKernel chief K hR).N ⋯ ⋯) (TorsorProgram.quotientFrame p.fst (mstageKernel chief K hR).N ⋯ ⋯ p.snd)) (q : Marking p.fst.Y) (hlift : ∀ (a : Gen), (QuotientGroup.mk' (mstageKernel chief K hR).N) (q a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a)) :

(Lifting.conjFamily (mstageKernel chief K hR)).op (Q2Word.tameRelator.eval q) = 1

Relator operators are trivial at compatible markings.

source

theorem Q2Presentation.Induction.mstage_relator_wild_op_one {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (mstageKernel chief K hR).N ⋯ ⋯) (TorsorProgram.quotientFrame p.fst (mstageKernel chief K hR).N ⋯ ⋯ p.snd)) (q : Marking p.fst.Y) (hlift : ∀ (a : Gen), (QuotientGroup.mk' (mstageKernel chief K hR).N) (q a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a)) :

(Lifting.conjFamily (mstageKernel chief K hR)).op (Q2Word.wildRelator.eval q) = 1

source

theorem Q2Presentation.Induction.mstage_markedAug_full {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (mstageKernel chief K hR).N ⋯ ⋯) (TorsorProgram.quotientFrame p.fst (mstageKernel chief K hR).N ⋯ ⋯ p.snd)) (q : Marking p.fst.Y) (hlift : ∀ (a : Gen), (QuotientGroup.mk' (mstageKernel chief K hR).N) (q a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a)) :

Lifting.markedAug (Lifting.conjFamily (mstageKernel chief K hR)) q = ⊤

The marked window is full at the mstage kernel.

source

∃ (n : Gen → Lifting.NAdd (mstageKernel chief K hR)), (Lifting.famRowsMap (Lifting.conjFamily (mstageKernel chief K hR)) q) n = uv

Mstage row surjectivity from the dévissage, conditional only on the nontrivial-simple faithfulness input. The one-element layer is trivially surjective.

source

∃ (n : Gen → Lifting.NAdd (mstageKernel chief K hR)), Lifting.foxShadowGen (Lifting.conjFamily (mstageKernel chief K hR)).op q n Q2Word.tameRelator - w ∈ W ∧ Lifting.foxShadowGen (Lifting.conjFamily (mstageKernel chief K hR)).op q n Q2Word.wildRelator ∈ W

The mstage Bockstein witness in keep shape, conditional only on the nontrivial-simple faithfulness input.