Boundary-framed marked targets and the exact-image inheritance lemma (Stage D)

This file realises manuscript Definition 4.1 (def:framed) and the structural content of Theorem 4.2 (thm:fixedframe) that is finite-group-theoretic and Q₂-independent: the boundary-framed marked targets, the boundary frame (α, ψ, β) cutting a finite target down to a fixed tame quotient H and a fixed elementary decoration E, the boundary-framed surjection count boundaryFramedSurj, and the exact-image inheritance lemma (exactImageTarget / exactImageTarget_boundaryFramed).

We deliberately do not prove the global induction of Theorem 4.2 (that is Stage H — it needs the linear lifting theory, exact-image recursion, Fourier inversion and strict decrease of marked 2-kernels). We only:

• define the data structures (BoundaryFramedTarget, BoundaryFrame, boundaryFramedSurj);
• prove that an exact-image stratum inherits the boundary-framed structure.

Manuscript Definition 4.1 (def:framed)

A boundary-framed marked target is a tuple 𝒴 = (Y, L_Y, π_Y, θ_Y) where L_Y ◁ Y is a finite 2-group, π_Y : Y ↠ H has kernel L_Y, and θ_Y : Y → E is a homomorphism. Put q_Y = (π_Y, θ_Y) : Y → H × E.

The frame fixes, via α : 𝕋_tame ↠ H and ψ̄ : Π → E, the induced β : ∂_bd → H × E, β(t, p) = (α t, ψ̄ p) (manuscript eq:beta). We compare only surjections f : Γ ↠ Y whose composite q_Y ∘ f equals β ∘ b_Γ (eq:eGamma): the boundary-framed count.

Manuscript exact-image inheritance (def:framed, paragraph after eq:eGamma)

An exact-image stratum consists of maps whose image is a specified subgroup J, rather than maps that merely land in J. If J ≤ Y projects onto H, then 𝒥 = (J, J ∩ L_Y, π_Y|_J, θ_Y|_J) inherits the same structure.

exactImageTarget builds 𝒥 as a genuine BoundaryFramedTarget — so the fact that it type-checks is exactly the inheritance — and exactImageTarget_boundaryFramed exposes the three substantive inherited facts (J ∩ L_Y is normal, is a 2-group, and is the kernel of the restricted π_Y|_J). Because H and E are preserved on the nose, the very same BoundaryFrame frames the stratum (exactImageFrame).

Boundary-framed marked targets (manuscript Definition 4.1)

structure Q2Presentation.BoundaryFramedTarget : Type 1

A boundary-framed marked target 𝒴 = (Y, L_Y, π_Y, θ_Y) (manuscript Definition 4.1, def:framed): a finite group Y with a normal finite 2-subgroup L_Y, a surjection π_Y : Y ↠ H onto a finite tame quotient with kernel exactly L_Y, and an elementary decoration θ_Y : Y → Multiplicative E into the multiplicative image of a finite 𝔽₂-vector space E. The pair q_Y = (π_Y, θ_Y) fixes both the tame quotient Y / L_Y ≅ H and the decoration.

• Y : Type

  The finite target group Y.

• groupY : Group self.Y
• finiteY : Finite self.Y
• LY : Subgroup self.Y

  The marked normal 2-subgroup L_Y ◁ Y (the wild part).

• LY_normal : self.LY.Normal

  L_Y is normal.

• LY_isTwoGroup : IsPGroup 2 ↥self.LY

  L_Y is a finite 2-group.

• H : Type

  The finite tame quotient group H.

• groupH : Group self.H
• finiteH : Finite self.H
• E : Type

  The elementary 𝔽₂-vector space E carrying the decoration.

• addCommGroupE : AddCommGroup self.E
• moduleE : Module (ZMod 2) self.E
• finiteE : Finite self.E
• piY : self.Y →* self.H

  The tame quotient map π_Y : Y ↠ H.

• piY_surj : Function.Surjective ⇑self.piY

  π_Y is surjective.

• ker_piY : self.piY.ker = self.LY

  The kernel of π_Y is exactly L_Y (so Y / L_Y ≅ H).

• thetaY : self.Y →* Multiplicative self.E

  The elementary decoration θ_Y : Y → Multiplicative E.

def Q2Presentation.BoundaryFramedTarget.qYMap (Yt : BoundaryFramedTarget) : Yt.Y →* Yt.H × Multiplicative Yt.E

The combined map q_Y = (π_Y, θ_Y) : Y →* H × Multiplicative E of manuscript Definition 4.1: the data the boundary-framed count holds fixed.

Equations

• Yt.qYMap = Yt.piY.prod Yt.thetaY

@[simp]

theorem Q2Presentation.BoundaryFramedTarget.qYMap_apply (Yt : BoundaryFramedTarget) (y : Yt.Y) : Yt.qYMap y = (Yt.piY y, Yt.thetaY y)

The boundary frame (α, ψ, β) (manuscript eq:beta)

noncomputable def Q2Presentation.boundaryBeta {Yt : BoundaryFramedTarget} (alpha : Ttame ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of Yt.H)) (psi : PiGrp ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Multiplicative Yt.E))) : Boundary ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Yt.H × Multiplicative Yt.E))

The induced map β : ∂_bd → H × E, β(t, p) = (α t, ψ̄ p) (manuscript eq:beta), built from a fixed tame surjection α : 𝕋_tame ↠ H and a fixed elementary marking ψ : Π → Multiplicative E by pairing the two boundary projections. Continuity into the finite (discrete) target is via local constancy of each coordinate.

Equations

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

@[simp]

theorem Q2Presentation.boundaryBeta_apply {Yt : BoundaryFramedTarget} (alpha : Ttame ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of Yt.H)) (psi : PiGrp ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Multiplicative Yt.E))) (b : ↑Boundary.toProfinite.toTop) : (ProfiniteGrp.Hom.hom (boundaryBeta alpha psi)) b = ((ProfiniteGrp.Hom.hom alpha) ((ProfiniteGrp.Hom.hom (CategoryTheory.Limits.pullback.fst nu_t nu_2)) b), (ProfiniteGrp.Hom.hom psi) ((ProfiniteGrp.Hom.hom (CategoryTheory.Limits.pullback.snd nu_t nu_2)) b))

structure Q2Presentation.BoundaryFrame (Yt : BoundaryFramedTarget) : Type

A boundary frame on a boundary-framed target 𝒴 (manuscript eq:beta): the fixed compatible data α : 𝕋_tame ↠ H, ψ : Π → Multiplicative E, and the induced β : ∂_bd → H × Multiplicative E. Surjectivity of α records that H really is a tame quotient (manuscript: "Fix a finite tame quotient H, an epimorphism α : 𝕋_A ↠ H").

• alpha : Ttame ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of Yt.H)

  The fixed tame surjection α : 𝕋_tame ↠ H.

• alpha_surj : Function.Surjective ⇑(ProfiniteGrp.Hom.hom self.alpha)

  α is surjective.

• psi : PiGrp ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Multiplicative Yt.E))

  The fixed elementary marking ψ : Π → Multiplicative E.

• beta : Boundary ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Yt.H × Multiplicative Yt.E))

  The induced boundary map β : ∂_bd → H × Multiplicative E.

• beta_def : self.beta = boundaryBeta self.alpha self.psi

  β is the pairing β(t, p) = (α t, ψ p) (manuscript eq:beta).

The boundary-framed surjection count (manuscript eq:eGamma)

def Q2Presentation.boundaryFramedSurj {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (Yt : BoundaryFramedTarget) (F : BoundaryFrame Yt) : Type

The boundary-framed surjections e_Γ^β(𝒴) (manuscript eq:eGamma): the continuous surjections f : Γ ↠ Y whose induced map to H × E is the prescribed β ∘ b_Γ, i.e. q_Y ∘ f = β ∘ b_Γ. This is the subtype counted in Theorem 4.2; its cardinality is e_Γ^β(𝒴).

Equations

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

Exact-image inheritance (manuscript Definition 4.1, exact-image paragraph)

def Q2Presentation.BoundaryFramedTarget.subgroupOfInclToLY (Yt : BoundaryFramedTarget) (J : Subgroup Yt.Y) : ↥(Yt.LY.subgroupOf J) →* ↥Yt.LY

The inclusion J ∩ L_Y ↪ L_Y (corestricted), as a monoid hom (L_Y.subgroupOf J) →* L_Y: ⟨⟨y, y∈J⟩, y∈L_Y⟩ ↦ ⟨y, y∈L_Y⟩. Injective, used to transport the 2-group property from L_Y to J ∩ L_Y.

Equations

• Yt.subgroupOfInclToLY J = { toFun := fun (x : ↥(Yt.LY.subgroupOf J)) => ⟨↑↑x, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

theorem Q2Presentation.BoundaryFramedTarget.subgroupOfInclToLY_injective (Yt : BoundaryFramedTarget) (J : Subgroup Yt.Y) : Function.Injective ⇑(Yt.subgroupOfInclToLY J)

theorem Q2Presentation.BoundaryFramedTarget.subgroupOf_LY_isTwoGroup (Yt : BoundaryFramedTarget) (J : Subgroup Yt.Y) : IsPGroup 2 ↥(Yt.LY.subgroupOf J)

J ∩ L_Y is a 2-group (inherited from L_Y): it injects into the 2-group L_Y, so IsPGroup.of_injective applies.

theorem Q2Presentation.BoundaryFramedTarget.ker_piY_comp_subtype (Yt : BoundaryFramedTarget) (J : Subgroup Yt.Y) : (Yt.piY.comp J.subtype).ker = Yt.LY.subgroupOf J

The restricted kernel ker (π_Y|_J) = J ∩ L_Y: π_Y|_J = π_Y ∘ ι_J, so its kernel is (ker π_Y).subgroupOf J = L_Y.subgroupOf J.

def Q2Presentation.BoundaryFramedTarget.exactImageTarget (Yt : BoundaryFramedTarget) (J : Subgroup Yt.Y) (hJ : Function.Surjective ⇑(Yt.piY.comp J.subtype)) : BoundaryFramedTarget

The exact-image stratum 𝒥 = (J, J ∩ L_Y, π_Y|_J, θ_Y|_J) (manuscript Definition 4.1, exact-image paragraph), as a genuine BoundaryFramedTarget.

The hypothesis hJ says J projects onto H (π_Y|_J surjective), which is the manuscript's "J ≤ Y projects onto H". All four boundary-framed axioms are inherited:

• J ∩ L_Y is normal in J (Normal.subgroupOf);
• J ∩ L_Y is a 2-group (subgroupOf_LY_isTwoGroup);
• π_Y|_J : J ↠ H is surjective (the hypothesis hJ) with kernel J ∩ L_Y (ker_piY_comp_subtype).

The tame quotient H and the elementary decoration E are preserved on the nose. This is the inheritance lemma: it being well-typed is the content.

Equations

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

@[simp]

theorem Q2Presentation.BoundaryFramedTarget.exactImageTarget_Y (Yt : BoundaryFramedTarget) (J : Subgroup Yt.Y) (hJ : Function.Surjective ⇑(Yt.piY.comp J.subtype)) : (Yt.exactImageTarget J hJ).Y = ↥J

@[simp]

theorem Q2Presentation.BoundaryFramedTarget.exactImageTarget_H (Yt : BoundaryFramedTarget) (J : Subgroup Yt.Y) (hJ : Function.Surjective ⇑(Yt.piY.comp J.subtype)) : (Yt.exactImageTarget J hJ).H = Yt.H

@[simp]

theorem Q2Presentation.BoundaryFramedTarget.exactImageTarget_E (Yt : BoundaryFramedTarget) (J : Subgroup Yt.Y) (hJ : Function.Surjective ⇑(Yt.piY.comp J.subtype)) : (Yt.exactImageTarget J hJ).E = Yt.E

@[simp]

theorem Q2Presentation.BoundaryFramedTarget.exactImageTarget_LY (Yt : BoundaryFramedTarget) (J : Subgroup Yt.Y) (hJ : Function.Surjective ⇑(Yt.piY.comp J.subtype)) : (Yt.exactImageTarget J hJ).LY = Yt.LY.subgroupOf J

@[simp]

theorem Q2Presentation.BoundaryFramedTarget.exactImageTarget_piY (Yt : BoundaryFramedTarget) (J : Subgroup Yt.Y) (hJ : Function.Surjective ⇑(Yt.piY.comp J.subtype)) : (Yt.exactImageTarget J hJ).piY = Yt.piY.comp J.subtype

@[simp]

theorem Q2Presentation.BoundaryFramedTarget.exactImageTarget_thetaY (Yt : BoundaryFramedTarget) (J : Subgroup Yt.Y) (hJ : Function.Surjective ⇑(Yt.piY.comp J.subtype)) : (Yt.exactImageTarget J hJ).thetaY = Yt.thetaY.comp J.subtype

theorem Q2Presentation.BoundaryFramedTarget.exactImageTarget_boundaryFramed (Yt : BoundaryFramedTarget) (J : Subgroup Yt.Y) (hJ : Function.Surjective ⇑(Yt.piY.comp J.subtype)) : (Yt.exactImageTarget J hJ).LY = Yt.LY.subgroupOf J ∧ (Yt.exactImageTarget J hJ).LY.Normal ∧ IsPGroup 2 ↥(Yt.exactImageTarget J hJ).LY ∧ (Yt.exactImageTarget J hJ).piY.ker = (Yt.exactImageTarget J hJ).LY

Exact-image inheritance lemma (manuscript Definition 4.1: "If J ≤ Y projects onto H, then 𝒥 = (J, J ∩ L_Y, π_Y|_J, θ_Y|_J) inherits the same structure"). The exact-image stratum is again boundary-framed: its marked normal subgroup J ∩ L_Y is normal and a 2-group, and is exactly the kernel of the restricted tame quotient π_Y|_J : J ↠ H. Consequently partitioning maps by their image subgroup stays inside the boundary-framed category.

def Q2Presentation.BoundaryFramedTarget.exactImageFrame (Yt : BoundaryFramedTarget) (J : Subgroup Yt.Y) (hJ : Function.Surjective ⇑(Yt.piY.comp J.subtype)) (F : BoundaryFrame Yt) : BoundaryFrame (Yt.exactImageTarget J hJ)

The stratum stays boundary-framed by the same frame. Because the exact-image target preserves H and E definitionally, every BoundaryFrame of 𝒴 is, verbatim, a BoundaryFrame of the exact-image stratum 𝒥. This is the categorical form of "exact-image strata inherit the same boundary-framed structure".

Equations

• Yt.exactImageFrame J hJ F = { alpha := F.alpha, alpha_surj := ⋯, psi := F.psi, beta := F.beta, beta_def := ⋯ }