theorem Q2Presentation.Induction.xr_hodd {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Odd (omega2Mod (Nat.card p.fst.Y)).val

The oddness input for the rows diagonal.

theorem Q2Presentation.Induction.xr_rowMap_range_eq {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)) (hR : 1 < Nat.card ↥(kernelFrattini K)) (q : Marking p.fst.Y) (hlift : ∀ (a : Gen), (QuotientGroup.mk' (xrKernel chief K).N) (q a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a)) : (Lifting.rowMap (xrKernel chief K) q).range = Submodule.comap (LinearMap.fst (ZMod 2) (Lifting.NAdd (xrKernel chief K)) (Lifting.NAdd (xrKernel chief K)) + LinearMap.snd (ZMod 2) (Lifting.NAdd (xrKernel chief K)) (Lifting.NAdd (xrKernel chief K))) (Lifting.conjInvDuals (xrKernel chief K)).dualCoannihilator

(♦=) The row image at a kernel-compatible marking: exactly the pairs whose sum is killed by every invariant dual.

theorem Q2Presentation.Induction.xr_ker_rowMap_card {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)) (hR : 1 < Nat.card ↥(kernelFrattini K)) : Nat.card ↥(Lifting.rowMap (xrKernel chief K) (Lifting.baseMarking (xrKernel chief K) p.snd g)).ker = 2 ^ (2 * Module.finrank (ZMod 2) (Lifting.NAdd (xrKernel chief K))) * Nat.card ↥(Lifting.conjInvDuals (xrKernel chief K))

The kernel count |ker (rowMap)| = 2^{2·dim R}·|𝒳_R| (prop:finalfourier l.4243–4245): rank–nullity against the sum-line size of the row image and the coannihilator dimension count.

noncomputable def Q2Presentation.Induction.xrObstructionDual {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)) : Module.Dual (ZMod 2) ↥(Lifting.conjInvDuals (xrKernel chief K))

The canonical candidate obstruction, valued in the dual of the invariant duals (lem:obstructionseparation): pair the base-marking defect sum against 𝒳_R.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Q2Presentation.Induction.xrObstructionDual_apply {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)) (f : ↥(Lifting.conjInvDuals (xrKernel chief K))) : (xrObstructionDual chief K g) f = ↑f ((Lifting.defectPair (xrKernel chief K) p.snd g (Lifting.baseMarking (xrKernel chief K) p.snd g) ⋯).1 + (Lifting.defectPair (xrKernel chief K) p.snd g (Lifting.baseMarking (xrKernel chief K) p.snd g) ⋯).2)

theorem Q2Presentation.Induction.xrObstructionDual_eq_zero_iff {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)) (hR : 1 < Nat.card ↥(kernelFrattini K)) : xrObstructionDual chief K g = 0 ↔ Nonempty (TorsorProgram.liftHom p.fst (xrKernel chief K).N ⋯ ⋯ boundaryPackage_GammaA p.snd g)

[A1] Separation: the obstruction vanishes iff framed candidate lifts exist.

theorem Q2Presentation.Induction.xr_Z1_card_gammaA {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)) (hR : 1 < Nat.card ↥(kernelFrattini K)) (f₀ : TorsorProgram.liftHom p.fst (xrKernel chief K).N ⋯ ⋯ boundaryPackage_GammaA p.snd g) : Nat.card (TorsorProgram.Z1 p.fst (xrKernel chief K).N ⋯ ⋯ boundaryPackage_GammaA p.snd g f₀) = 2 ^ (2 * Module.finrank (ZMod 2) (Lifting.NAdd (xrKernel chief K))) * Nat.card ↥(Lifting.conjInvDuals (xrKernel chief K))

[A2] The uniform count: every base lift's twisted-cocycle set has size z_R = 2^{2·dim R}·|𝒳_R|.