theorem
Q2Presentation.Induction.xr_marking_covers
{p : FramedPair}
(chief : FirstNonScalarChiefFactor p)
(K : KernelMinimal chief.toNonScalarChiefFactor)
(g :
boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (xrKernel chief K).N ⋯ ⋯)
(TorsorProgram.quotientFrame p.fst (xrKernel chief K).N ⋯ ⋯ p.snd))
(q : Marking p.fst.Y)
(hlift : ∀ (a : Gen), (QuotientGroup.mk' (xrKernel chief K).N) (q a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a))
(y : p.fst.Y)
:
The marking covers Y modulo the kernel: the generators
topologically generate Γ_A and the boundary surjection fills the
finite quotient.
theorem
Q2Presentation.Induction.xr_hcover
{p : FramedPair}
(chief : FirstNonScalarChiefFactor p)
(K : KernelMinimal chief.toNonScalarChiefFactor)
(g :
boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (xrKernel chief K).N ⋯ ⋯)
(TorsorProgram.quotientFrame p.fst (xrKernel chief K).N ⋯ ⋯ p.snd))
(q : Marking p.fst.Y)
(hlift : ∀ (a : Gen), (QuotientGroup.mk' (xrKernel chief K).N) (q a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a))
(y : p.fst.Y)
:
∃ c ∈ Subgroup.closure (Set.range q), (Lifting.conjFamily (xrKernel chief K)).op (y * c⁻¹) = 1
The cover in operator form.
theorem
Q2Presentation.Induction.xr_relator_tame_op_one
{p : FramedPair}
(chief : FirstNonScalarChiefFactor p)
(K : KernelMinimal chief.toNonScalarChiefFactor)
(g :
boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (xrKernel chief K).N ⋯ ⋯)
(TorsorProgram.quotientFrame p.fst (xrKernel chief K).N ⋯ ⋯ p.snd))
(q : Marking p.fst.Y)
(hlift : ∀ (a : Gen), (QuotientGroup.mk' (xrKernel chief K).N) (q a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a))
:
Relator operators are trivial at compatible markings.
theorem
Q2Presentation.Induction.xr_relator_wild_op_one
{p : FramedPair}
(chief : FirstNonScalarChiefFactor p)
(K : KernelMinimal chief.toNonScalarChiefFactor)
(g :
boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (xrKernel chief K).N ⋯ ⋯)
(TorsorProgram.quotientFrame p.fst (xrKernel chief K).N ⋯ ⋯ p.snd))
(q : Marking p.fst.Y)
(hlift : ∀ (a : Gen), (QuotientGroup.mk' (xrKernel chief K).N) (q a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a))
:
theorem
Q2Presentation.Induction.xr_markedAug_full
{p : FramedPair}
(chief : FirstNonScalarChiefFactor p)
(K : KernelMinimal chief.toNonScalarChiefFactor)
(g :
boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (xrKernel chief K).N ⋯ ⋯)
(TorsorProgram.quotientFrame p.fst (xrKernel chief K).N ⋯ ⋯ p.snd))
(q : Marking p.fst.Y)
(hchar :
¬∃ (lam : Module.Dual (ZMod 2) (sec7RawTowerPacketCanonical chief K).rawModuleData.R),
lam ≠ 0 ∧ ∀ (c : (sec7RawTowerPacketCanonical chief K).rawModuleData.C),
lam ∘ₗ ↑((sec7RawTowerPacketCanonical chief K).rawActionData.actR c) = lam)
(hlift : ∀ (a : Gen), (QuotientGroup.mk' (xrKernel chief K).N) (q a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a))
:
The marked window is full at the XR kernel.
theorem
Q2Presentation.Induction.frattini_ne_top_of_nontrivial
{G : Type u_1}
[Group G]
[Finite G]
[Nontrivial G]
:
Frattini subgroups of nontrivial finite groups are proper.
theorem
Q2Presentation.Induction.xr_card_Y_four
{p : FramedPair}
(chief : FirstNonScalarChiefFactor p)
(K : KernelMinimal chief.toNonScalarChiefFactor)
(hR : 1 < Nat.card ↥(kernelFrattini K))
:
4 divides |Y| in the R ≠ 1 branch: the kernel subgroup is a
2-group of order at least 4 (its Frattini subgroup is proper and
already nontrivial).
theorem
Q2Presentation.Induction.xr_rows_surjective_diamond
{p : FramedPair}
(chief : FirstNonScalarChiefFactor p)
(K : KernelMinimal chief.toNonScalarChiefFactor)
(g :
boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (xrKernel chief K).N ⋯ ⋯)
(TorsorProgram.quotientFrame p.fst (xrKernel chief K).N ⋯ ⋯ p.snd))
(q : Marking p.fst.Y)
(hR : 1 < Nat.card ↥(kernelFrattini K))
(hchar :
¬∃ (lam : Module.Dual (ZMod 2) (sec7RawTowerPacketCanonical chief K).rawModuleData.R),
lam ≠ 0 ∧ ∀ (c : (sec7RawTowerPacketCanonical chief K).rawModuleData.C),
lam ∘ₗ ↑((sec7RawTowerPacketCanonical chief K).rawActionData.actR c) = lam)
(hlift : ∀ (a : Gen), (QuotientGroup.mk' (xrKernel chief K).N) (q a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a))
(hframe :
∀ (a : Gen),
p.fst.qYMap (q a) = (ProfiniteGrp.Hom.hom p.snd.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a)))
(hfaithNT :
∀ (W' W : Submodule (ZMod 2) (Lifting.NAdd (xrKernel chief K)))
(hW : ∀ (y : p.fst.Y), ∀ m ∈ W, ((Lifting.conjFamily (xrKernel chief K)).op y) m ∈ W)
(hW' : ∀ (y : p.fst.Y), ∀ m ∈ W', ((Lifting.conjFamily (xrKernel chief K)).op y) m ∈ W'),
W' < W →
(∀ U < W, W' ≤ U → (∀ (y : p.fst.Y), ∀ m ∈ U, ((Lifting.conjFamily (xrKernel chief K)).op y) m ∈ U) → U = W') →
(¬∀ (y : p.fst.Y), (Lifting.sectionFamily (Lifting.conjFamily (xrKernel chief K)) W' W hW hW').op y = 1) →
Lifting.dualPairingFaithful (Lifting.sectionFamily (Lifting.conjFamily (xrKernel chief K)) W' W hW hW') q)
(uv : Lifting.NAdd (xrKernel chief K) × Lifting.NAdd (xrKernel chief K))
:
∃ (n : Gen → Lifting.NAdd (xrKernel chief K)), (Lifting.famRowsMap (Lifting.conjFamily (xrKernel chief K)) q) n = uv
XR row surjectivity from the dévissage, conditional only on the nontrivial-simple faithfulness input.
theorem
Q2Presentation.Induction.xr_bockstein_witness_diamond
{p : FramedPair}
(chief : FirstNonScalarChiefFactor p)
(K : KernelMinimal chief.toNonScalarChiefFactor)
(g :
boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget p.fst (xrKernel chief K).N ⋯ ⋯)
(TorsorProgram.quotientFrame p.fst (xrKernel chief K).N ⋯ ⋯ p.snd))
(q : Marking p.fst.Y)
(hR : 1 < Nat.card ↥(kernelFrattini K))
(hchar :
¬∃ (lam : Module.Dual (ZMod 2) (sec7RawTowerPacketCanonical chief K).rawModuleData.R),
lam ≠ 0 ∧ ∀ (c : (sec7RawTowerPacketCanonical chief K).rawModuleData.C),
lam ∘ₗ ↑((sec7RawTowerPacketCanonical chief K).rawActionData.actR c) = lam)
(hlift : ∀ (a : Gen), (QuotientGroup.mk' (xrKernel chief K).N) (q a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a))
(hframe :
∀ (a : Gen),
p.fst.qYMap (q a) = (ProfiniteGrp.Hom.hom p.snd.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a)))
(hfaithNT :
∀ (W' W : Submodule (ZMod 2) (Lifting.NAdd (xrKernel chief K)))
(hW : ∀ (y : p.fst.Y), ∀ m ∈ W, ((Lifting.conjFamily (xrKernel chief K)).op y) m ∈ W)
(hW' : ∀ (y : p.fst.Y), ∀ m ∈ W', ((Lifting.conjFamily (xrKernel chief K)).op y) m ∈ W'),
W' < W →
(∀ U < W, W' ≤ U → (∀ (y : p.fst.Y), ∀ m ∈ U, ((Lifting.conjFamily (xrKernel chief K)).op y) m ∈ U) → U = W') →
(¬∀ (y : p.fst.Y), (Lifting.sectionFamily (Lifting.conjFamily (xrKernel chief K)) W' W hW hW').op y = 1) →
Lifting.dualPairingFaithful (Lifting.sectionFamily (Lifting.conjFamily (xrKernel chief K)) W' W hW hW') q)
(W : Submodule (ZMod 2) (Lifting.NAdd (xrKernel chief K)))
(w : Lifting.NAdd (xrKernel chief K))
:
∃ (n : Gen → Lifting.NAdd (xrKernel chief K)),
Lifting.foxShadowGen (Lifting.conjFamily (xrKernel chief K)).op q n Q2Word.tameRelator - w ∈ W ∧ Lifting.foxShadowGen (Lifting.conjFamily (xrKernel chief K)).op q n Q2Word.wildRelator ∈ W
The XR Bockstein witness in keep shape, conditional only on the nontrivial-simple faithfulness input — the relative fixedness is not even needed once the rows are surjective.