instance Q2Presentation.TorsorProgram.instFiniteSubgroupY (Yt : BoundaryFramedTarget) : Finite (Subgroup Yt.Y)

The subgroup lattice of a finite framed target is finite (local helper; subgroups embed into the finite powerset).

@[reducible, inline]

abbrev Q2Presentation.TorsorProgram.coverStrata (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] : Type

The exact-image strata index: subgroups of the ambient target mapping ONTO the child (J̃ ≤ p⁻¹(J) with p(J̃) = J at J = the full child; manuscript sum index of eq:covertransform).

Equations

• Q2Presentation.TorsorProgram.coverStrata Yt N = { J : Subgroup Yt.Y // Subgroup.map (QuotientGroup.mk' N) J = ⊤ }

instance Q2Presentation.TorsorProgram.instFiniteCoverStrata (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] : Finite (coverStrata Yt N)

instance Q2Presentation.TorsorProgram.instFintypeCoverStrata (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] : Fintype (coverStrata Yt N)

The canonical (noncomputable) enumeration of the strata; global so that every strata sum downstream elaborates against the same instance.

Equations

• Q2Presentation.TorsorProgram.instFintypeCoverStrata Yt N = Fintype.ofFinite (Q2Presentation.TorsorProgram.coverStrata Yt N)

theorem Q2Presentation.TorsorProgram.coverStrata_piY_surjective (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) (J : coverStrata Yt N) : Function.Surjective ⇑(Yt.piY.comp (↑J).subtype)

A stratum projects onto the tame quotient H, so exactImageTarget applies: a preimage of h differs from a stratum element by N ≤ L_Y.

Stratum carrier plumbing (mirror of MStage.imgY)

def Q2Presentation.TorsorProgram.stratumVal (Yt : BoundaryFramedTarget) {J : Subgroup Yt.Y} {hJ : Function.Surjective ⇑(Yt.piY.comp J.subtype)} (x : ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Yt.exactImageTarget J hJ).Y)).toProfinite.toTop) : Yt.Y

Carrier readout of a stratum-valued element (direct subtype application; mirror of MStage.imgY, Induction/MStagePartitionAssembly.lean).

Equations

• Q2Presentation.TorsorProgram.stratumVal Yt x = J.subtype x

theorem Q2Presentation.TorsorProgram.stratumVal_mem (Yt : BoundaryFramedTarget) {J : Subgroup Yt.Y} {hJ : Function.Surjective ⇑(Yt.piY.comp J.subtype)} (x : ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Yt.exactImageTarget J hJ).Y)).toProfinite.toTop) : stratumVal Yt x ∈ J

def Q2Presentation.TorsorProgram.stratumInclHom (Yt : BoundaryFramedTarget) (J : Subgroup Yt.Y) (hJ : Function.Surjective ⇑(Yt.piY.comp J.subtype)) : ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Yt.exactImageTarget J hJ).Y) ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of Yt.Y)

The stratum inclusion as a hom of finite discrete profinite groups (idiom: projHom, Boundary/LiftFibration.lean).

Equations

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

@[simp]

theorem Q2Presentation.TorsorProgram.stratumInclHom_apply (Yt : BoundaryFramedTarget) (J : Subgroup Yt.Y) (hJ : Function.Surjective ⇑(Yt.piY.comp J.subtype)) (x : ↑(ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Yt.exactImageTarget J hJ).Y)).toProfinite.toTop) : (ProfiniteGrp.Hom.hom (stratumInclHom Yt J hJ)) x = stratumVal Yt x

The total space and fibration 1 (over the child surjections)

def Q2Presentation.TorsorProgram.coverLiftTotal (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) : Type

The cover-lift total space: framed continuous homs into the AMBIENT target whose projection to the child is onto (lem:covertransform: all lifts of all unobstructed exact-image maps at once; surjectivity onto the ambient target NOT imposed — these are the weak lifts).

Equations

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

def Q2Presentation.TorsorProgram.coverLiftBase (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (t : coverLiftTotal Yt N B F) : boundaryFramedSurj B (quotientFramedTarget Yt N hNLY hNθ) (quotientFrame Yt N hNLY hNθ F)

Fibration base 1: the induced child-framed surjection (mirror of restrictSurj, Boundary/LiftFibration.lean).

Equations

• Q2Presentation.TorsorProgram.coverLiftBase Yt N hNLY hNθ B F t = ⟨{ hom := CategoryTheory.CategoryStruct.comp (↑t) (Q2Presentation.TorsorProgram.projHom Yt N), surj := ⋯ }, ⋯⟩

@[simp]

theorem Q2Presentation.TorsorProgram.coverLiftBase_hom_apply (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (t : coverLiftTotal Yt N B F) (γ : ↑Γ.toProfinite.toTop) : (ProfiniteGrp.Hom.hom (↑(coverLiftBase Yt N hNLY hNθ B F t)).hom) γ = (QuotientGroup.mk' N) ((ProfiniteGrp.Hom.hom ↑t) γ)

def Q2Presentation.TorsorProgram.coverLiftFibreEquiv (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (quotientFramedTarget Yt N hNLY hNθ) (quotientFrame Yt N hNLY hNθ F)) : { t : coverLiftTotal Yt N B F // coverLiftBase Yt N hNLY hNθ B F t = g } ≃ liftHom Yt N hNLY hNθ B F g

The fibre of the base map over a child surjection is exactly the framed lift set (idiom: liftFibre_equiv_liftHom, Boundary/LiftFibration.lean).

Equations

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

def Q2Presentation.TorsorProgram.coverLiftTotal_equiv_sigma_liftHom (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) : coverLiftTotal Yt N B F ≃ (g : boundaryFramedSurj B (quotientFramedTarget Yt N hNLY hNθ) (quotientFrame Yt N hNLY hNθ F)) × liftHom Yt N hNLY hNθ B F g

Fibration 1: the total space is the sigma of ALL framed lifts over the child surjections.

Equations

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

Fibration 2 (over the exact-image strata)

def Q2Presentation.TorsorProgram.coverLiftStratum (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (t : coverLiftTotal Yt N B F) : coverStrata Yt N

Fibration base 2: the exact image of a total point is a stratum.

Equations

• Q2Presentation.TorsorProgram.coverLiftStratum Yt N B F t = ⟨(ProfiniteGrp.Hom.hom ↑t).range, ⋯⟩

def Q2Presentation.TorsorProgram.stratumCorestrict (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (J : coverStrata Yt N) (t : coverLiftTotal Yt N B F) (ht : coverLiftStratum Yt N B F t = J) : boundaryFramedSurj B (Yt.exactImageTarget ↑J ⋯) (Yt.exactImageFrame ↑J ⋯ F)

Corestriction of a total point onto its exact-image stratum, as a framed surjection of the stratum target (mirror of MStage.corestrict).

Equations

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

theorem Q2Presentation.TorsorProgram.stratumCorestrict_val_hom_apply (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (J : coverStrata Yt N) (t : coverLiftTotal Yt N B F) (ht : coverLiftStratum Yt N B F t = J) (γ : ↑Γ.toProfinite.toTop) : stratumVal Yt ((ProfiniteGrp.Hom.hom (↑(stratumCorestrict Yt N hNLY B F J t ht)).hom) γ) = (ProfiniteGrp.Hom.hom ↑t) γ

Value readout of the corestriction (single-step reduction lemma; idiom: restrictSurj_hom_apply).

def Q2Presentation.TorsorProgram.stratumExtend (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (J : coverStrata Yt N) (h : boundaryFramedSurj B (Yt.exactImageTarget ↑J ⋯) (Yt.exactImageFrame ↑J ⋯ F)) : coverLiftTotal Yt N B F

Extension of a stratum-framed surjection to a total point (composition with the stratum inclusion; mirror of MStage.ofImageSurj, stage 2).

Equations

• Q2Presentation.TorsorProgram.stratumExtend Yt N hNLY B F J h = ⟨CategoryTheory.CategoryStruct.comp (↑h).hom (Q2Presentation.TorsorProgram.stratumInclHom Yt ↑J ⋯), ⋯⟩

theorem Q2Presentation.TorsorProgram.stratumExtend_val_apply (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (J : coverStrata Yt N) (h : boundaryFramedSurj B (Yt.exactImageTarget ↑J ⋯) (Yt.exactImageFrame ↑J ⋯ F)) (γ : ↑Γ.toProfinite.toTop) : (ProfiniteGrp.Hom.hom ↑(stratumExtend Yt N hNLY B F J h)) γ = stratumVal Yt ((ProfiniteGrp.Hom.hom (↑h).hom) γ)

Value readout of the extension (single-step reduction lemma).

theorem Q2Presentation.TorsorProgram.coverLiftStratum_stratumExtend (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (J : coverStrata Yt N) (h : boundaryFramedSurj B (Yt.exactImageTarget ↑J ⋯) (Yt.exactImageFrame ↑J ⋯ F)) : coverLiftStratum Yt N B F (stratumExtend Yt N hNLY B F J h) = J

The extension has exact image exactly the stratum (mirror of MStage.rangeOf_ofImageSurj).

def Q2Presentation.TorsorProgram.stratumFibreEquiv (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (J : coverStrata Yt N) : { t : coverLiftTotal Yt N B F // coverLiftStratum Yt N B F t = J } ≃ boundaryFramedSurj B (Yt.exactImageTarget ↑J ⋯) (Yt.exactImageFrame ↑J ⋯ F)

The fibre of the exact-image map over a stratum is exactly the stratum's boundary-framed surjection set.

Equations

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

def Q2Presentation.TorsorProgram.coverLiftTotal_equiv_sigma_strata (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) : coverLiftTotal Yt N B F ≃ (J : coverStrata Yt N) × boundaryFramedSurj B (Yt.exactImageTarget ↑J ⋯) (Yt.exactImageFrame ↑J ⋯ F)

Fibration 2: the total space is the sigma of the framed exact-image counts over the strata.

Equations

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

The abstract multiplicity-count core

theorem Q2Presentation.TorsorProgram.coverPartition_card_of_uniform (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) [Fintype (boundaryFramedSurj B (quotientFramedTarget Yt N hNLY hNθ) (quotientFrame Yt N hNLY hNθ F))] (hfinL : ∀ (g : boundaryFramedSurj B (quotientFramedTarget Yt N hNLY hNθ) (quotientFrame Yt N hNLY hNθ F)), Finite (liftHom Yt N hNLY hNθ B F g)) (hfinS : ∀ (J : coverStrata Yt N), Finite (boundaryFramedSurj B (Yt.exactImageTarget ↑J ⋯) (Yt.exactImageFrame ↑J ⋯ F))) (c : ℕ) (huni : ∀ (g : boundaryFramedSurj B (quotientFramedTarget Yt N hNLY hNθ) (quotientFrame Yt N hNLY hNθ F)), Nonempty (liftHom Yt N hNLY hNθ B F g) → Nat.card (liftHom Yt N hNLY hNθ B F g) = c) : c * Nat.card { g : boundaryFramedSurj B (quotientFramedTarget Yt N hNLY hNθ) (quotientFrame Yt N hNLY hNθ F) // Nonempty (liftHom Yt N hNLY hNθ B F g) } = ∑ J : coverStrata Yt N, Nat.card (boundaryFramedSurj B (Yt.exactImageTarget ↑J ⋯) (Yt.exactImageFrame ↑J ⋯ F))

The generic count core (eq:covertransform l.3834–3840 with an abstract uniform multiplicity c; instantiated at c := 8 by lem:commonscalars via W2b/W2c/W2d): counting the total space along both fibrations, c · #{liftable children} = Σ_{J̃} e_Γ^β(J̃-stratum). This is the manuscript's "literal partition of the eight lifts … without an equidistribution assumption" — no Hom(Γ,𝔽₂)-action is used, only the uniform fibre count.

The generic strict-decrease ingredient

def Q2Presentation.TorsorProgram.stratumLYProj (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (J : Subgroup Yt.Y) : ↥(Yt.LY.subgroupOf J) →* Yt.Y ⧸ N

The stratum-kernel comparison hom J̃ ∩ L̃ →* Ỹ/N (composite of the two subtype inclusions with the projection; a top-level def so that its applications are defeq-unfoldable in the counting proof below).

Equations

• Q2Presentation.TorsorProgram.stratumLYProj Yt N J = (QuotientGroup.mk' N).comp (J.subtype.comp (Yt.LY.subgroupOf J).subtype)

theorem Q2Presentation.TorsorProgram.coverStrata_LY_card_le (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) (J : coverStrata Yt N) : Nat.card ↥(Yt.exactImageTarget ↑J ⋯).LY ≤ Nat.card ↥N * Nat.card ↥(quotientFramedTarget Yt N hNLY hNθ).LY

Generic stratum measure bound (lem:strictdecrease eq:properweighteddescent engine, l.4407): a stratum's marked kernel J̃ ∩ L̃ is at most |N| times the child's marked kernel — the exact-sequence count |J̃ ∩ L̃| = |ker| · |image| with the kernel side inside N and the image side inside the child L.