Documentation

Q2Presentation.Induction.ProperImageSubtraction

def Q2Presentation.Induction.sigmaSubtypeCongr {ι : Type u_1} {F : ι → Type u_2} (P : (i : ι) → F i → Prop) :

{ x : (i : ι) × F i // P x.fst x.snd } ≃ (i : ι) × { f : F i // P i f }

Sigma-subtype reassociation, fibre-predicate version (Equiv.subtypeSigmaEquiv predicates on .1 only; idiom: the packet's sigmaRestrict).

Equations

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

Instances For

@[reducible, inline]

abbrev Q2Presentation.Induction.mLiftTotal {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) :

The W2a total space at the child M-kernel (the Zcount carrier of P3-U5), abbreviated for the partition chain.

Equations

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

Instances For

@[reducible, inline]

noncomputable abbrev Q2Presentation.Induction.mLiftStratum {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (t : mLiftTotal chief K B) :

mImageStrata chief K

The exact-image stratum of a total point, abbreviated.

Equations

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

Instances For

def Q2Presentation.Induction.properCoverLiftable {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (J : mImageStrata chief K) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (h : boundaryFramedSurj B (mImageStratumPair chief K J).fst (mImageStratumPair chief K J).snd) :

Per-stratum λ-liftability (the m_{Γ,λ}(J)-condition of prop:finalfourier l.4246–4248, lem:obstructionseparation reading): some framed hom into B_λ projects to the stratum surjection's values. Same ∃-raw-hom shape as coverLiftableWeak (P3-U5) and restrictLiftHom_iff_exists (P4-V2).

Equations

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

Instances For

noncomputable def Q2Presentation.Induction.mCount {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (J : mImageStrata chief K) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) :

m_{Γ,λ}(J) (eq:recursionR2's summand).

Equations

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

Instances For

theorem Q2Presentation.Induction.coverLiftableWeak_iff_corestrict {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (J : mImageStrata chief K) (t : mLiftTotal chief K B) (ht : mLiftStratum chief K B t = J) :

coverLiftableWeak chief K lam hinv B t ↔ properCoverLiftable chief K lam hinv J B (TorsorProgram.stratumCorestrict (XRZero.xrChild chief K).fst (mChildKernel chief K).N ⋯ B (XRZero.xrChild chief K).snd J t ht)

Liftability is corestriction-invariant: a total point is coverLiftableWeak iff its stratum corestriction is properCoverLiftable (both conditions read the same underlying values — stratumCorestrict_val_hom_apply is rfl).

theorem Q2Presentation.Induction.sec7_properImagePartition {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (hfinS : ∀ (J : mImageStrata chief K), Finite (boundaryFramedSurj B (mImageStratumPair chief K J).fst (mImageStratumPair chief K J).snd)) :

Zcount chief K lam hinv B = ∑ J : mImageStrata chief K, mCount chief K lam hinv J B

eq:recursionR2, additive form (the manuscript proof's literal content: "partition the relation-compatible maps to B by their exact image"). hne-free (tautological partition), source-generic modulo the strata bFS-finiteness hypothesis.

The top stratum is the keep's set #

theorem Q2Presentation.Induction.mLiftStratum_coverSurjEmbed {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (g : boundaryFramedSurj B (XRZero.xrChild chief K).fst (XRZero.xrChild chief K).snd) :

mLiftStratum chief K B (coverSurjEmbed chief K B g) = mImageTop chief K

The embedded total point of a framed surjection has top exact image.

def Q2Presentation.Induction.coverSurjOfTop {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (t : mLiftTotal chief K B) (ht : mLiftStratum chief K B t = mImageTop chief K) :

boundaryFramedSurj B (XRZero.xrChild chief K).fst (XRZero.xrChild chief K).snd

Repackaging of a top-stratum total point as a framed surjection.

Equations

Q2Presentation.Induction.coverSurjOfTop chief K B t ht = ⟨{ hom := ↑t, surj := ⋯ }, ⋯⟩

Instances For

theorem Q2Presentation.Induction.coverSurjEmbed_coverSurjOfTop {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (t : mLiftTotal chief K B) (ht : mLiftStratum chief K B t = mImageTop chief K) :

coverSurjEmbed chief K B (coverSurjOfTop chief K B t ht) = t

theorem Q2Presentation.Induction.mCount_top_eq {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) :

mCount chief K lam hinv (mImageTop chief K) B = Nat.card { g : boundaryFramedSurj B (XRZero.xrChild chief K).fst (XRZero.xrChild chief K).snd // Nonempty (Lifting.scalarCoverLiftHom (xrKernel chief K) lam hinv B p.snd g) }

The top stratum is the keep's set: m_{Γ,λ}(B) in the keep's scalarCoverLiftHom spelling (through P3-U5's coverLiftableWeak_of_surj).

The isolation form (subtraction-free `eq:recursionR2`) #

theorem Q2Presentation.Induction.sec7_properImageSubtraction {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (hfinS : ∀ (J : mImageStrata chief K), Finite (boundaryFramedSurj B (mImageStratumPair chief K J).fst (mImageStratumPair chief K J).snd)) :

Nat.card { g : boundaryFramedSurj B (XRZero.xrChild chief K).fst (XRZero.xrChild chief K).snd // Nonempty (Lifting.scalarCoverLiftHom (xrKernel chief K) lam hinv B p.snd g) } + ∑ J ∈ Finset.univ.erase (mImageTop chief K), mCount chief K lam hinv J B = Zcount chief K lam hinv B

eq:recursionR2, isolation form: the keep's count plus the proper sum is Z (m_{Γ,λ}(B) = Z − Σ_proper m_J, rearranged additively).

The per-source discharges #

theorem Q2Presentation.Induction.mImageStratumPair_bFS_finite_gammaA {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (J : mImageStrata chief K) :

Finite (boundaryFramedSurj boundaryPackage_GammaA (mImageStratumPair chief K J).fst (mImageStratumPair chief K J).snd)

Candidate-side strata finiteness (the generic carrier at the stratum pair).

theorem Q2Presentation.Induction.mImageStratumPair_bFS_finite_gq2 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (J : mImageStrata chief K) :

Finite (boundaryFramedSurj boundaryPackage_GQ2 (mImageStratumPair chief K J).fst (mImageStratumPair chief K J).snd)

Local-side strata finiteness.

theorem Q2Presentation.Induction.sec7_properImageSubtraction_gammaA {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) :

Nat.card { g : boundaryFramedSurj boundaryPackage_GammaA (XRZero.xrChild chief K).fst (XRZero.xrChild chief K).snd // Nonempty (Lifting.scalarCoverLiftHom (xrKernel chief K) lam hinv boundaryPackage_GammaA p.snd g) } + ∑ J ∈ Finset.univ.erase (mImageTop chief K), mCount chief K lam hinv J boundaryPackage_GammaA = Zcount chief K lam hinv boundaryPackage_GammaA

eq:recursionR2, isolation form, candidate source (finiteness discharged).

theorem Q2Presentation.Induction.sec7_properImageSubtraction_gq2 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) :

Nat.card { g : boundaryFramedSurj boundaryPackage_GQ2 (XRZero.xrChild chief K).fst (XRZero.xrChild chief K).snd // Nonempty (Lifting.scalarCoverLiftHom (xrKernel chief K) lam hinv boundaryPackage_GQ2 p.snd g) } + ∑ J ∈ Finset.univ.erase (mImageTop chief K), mCount chief K lam hinv J boundaryPackage_GQ2 = Zcount chief K lam hinv boundaryPackage_GQ2

eq:recursionR2, isolation form, local source (finiteness discharged).