The cover projection: surjectivity and kernel (missing from P1)

theorem Q2Presentation.Lifting.scalarProj_surjective_generic {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) : Function.Surjective ⇑(scalarProj E lam hinv)

The scalar projection is surjective (generic form of scalarProj_surjective, RadicalEdgeTower.lean:284).

theorem Q2Presentation.Lifting.scalarCoverProj_scalarProj {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (y : Yt.Y) : (scalarCoverProj E lam hinv) ((scalarProj E lam hinv) y) = (QuotientGroup.mk' E.N) y

The cover projection on a single-level class (mk-chase through scalarCollapse_mk/scalarCollapse_mk_mk).

theorem Q2Presentation.Lifting.scalarCoverProj_surjective {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) : Function.Surjective ⇑(scalarCoverProj E lam hinv)

p_λ is surjective.

theorem Q2Presentation.Lifting.ker_scalarCoverProj {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) : (scalarCoverProj E lam hinv).ker = (scalarRelKernel E lam hinv).N

ker p_λ = R/ker λ (via injectivity of the Noether collapse).

theorem Q2Presentation.Lifting.piY_scalarCoverProj {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (x : (scalarCoverTarget E lam hinv).Y) : (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).piY ((scalarCoverProj E lam hinv) x) = (scalarCoverTarget E lam hinv).piY x

π̃-compatibility: the child tame projection factors through p_λ.

theorem Q2Presentation.Lifting.thetaY_scalarCoverProj {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (x : (scalarCoverTarget E lam hinv).Y) : (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).thetaY ((scalarCoverProj E lam hinv) x) = (scalarCoverTarget E lam hinv).thetaY x

θ̃-compatibility mirror.

The ambient restricted cover p_λ⁻¹(J) and its corestricted projection

def Q2Presentation.Lifting.coverRestrictAmb {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) : Subgroup (scalarCoverTarget E lam hinv).Y

The ambient restricted cover p_λ⁻¹(J) ≤ B_λ.

Equations

• Q2Presentation.Lifting.coverRestrictAmb E lam hinv J = Subgroup.comap (Q2Presentation.Lifting.scalarCoverProj E lam hinv) J

theorem Q2Presentation.Lifting.mem_coverRestrictAmb {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) (x : (scalarCoverTarget E lam hinv).Y) : x ∈ coverRestrictAmb E lam hinv J ↔ (scalarCoverProj E lam hinv) x ∈ J

theorem Q2Presentation.Lifting.relN_le_coverRestrictAmb {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) : (scalarRelKernel E lam hinv).N ≤ coverRestrictAmb E lam hinv J

The deck kernel sits inside the restricted cover (ker ≤ comap of anything).

theorem Q2Presentation.Lifting.coverRestrictAmb_map_proj {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) : Subgroup.map (scalarCoverProj E lam hinv) (coverRestrictAmb E lam hinv J) = J

p_λ(p_λ⁻¹(J)) = J (surjectivity of the cover projection).

def Q2Presentation.Lifting.restrictProj {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) : ↥(coverRestrictAmb E lam hinv J) →* ↥J

The corestricted projection p_λ⁻¹(J) →* J.

Equations

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

theorem Q2Presentation.Lifting.restrictProj_surjective {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) : Function.Surjective ⇑(restrictProj E lam hinv J)

theorem Q2Presentation.Lifting.restrictProj_eq_one_iff {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) (x : ↥(coverRestrictAmb E lam hinv J)) : (restrictProj E lam hinv J) x = 1 ↔ x ∈ (scalarRelKernel E lam hinv).N.subgroupOf (coverRestrictAmb E lam hinv J)

The corestricted projection dies exactly on the restricted deck kernel.

The restricted cover as a framed target with its deck kernel

theorem Q2Presentation.Lifting.coverRestrictAmb_piY_surjective {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) (hJpi : Function.Surjective ⇑((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).piY.comp J.subtype)) : Function.Surjective ⇑((scalarCoverTarget E lam hinv).piY.comp (coverRestrictAmb E lam hinv J).subtype)

p_λ⁻¹(J) projects onto H when J does.

@[reducible, inline]

noncomputable abbrev Q2Presentation.Lifting.restrictTarget {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) (hJpi : Function.Surjective ⇑((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).piY.comp J.subtype)) : BoundaryFramedTarget

The restricted cover as a framed target (manuscript: the central double cover p_λ⁻¹(J) ↠ J of eq:recursionR3).

Equations

• Q2Presentation.Lifting.restrictTarget E lam hinv J hJpi = (Q2Presentation.Lifting.scalarCoverTarget E lam hinv).exactImageTarget (Q2Presentation.Lifting.coverRestrictAmb E lam hinv J) ⋯

@[reducible, inline]

noncomputable abbrev Q2Presentation.Lifting.restrictFrame {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) (hJpi : Function.Surjective ⇑((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).piY.comp J.subtype)) (F : BoundaryFrame Yt) : BoundaryFrame (restrictTarget E lam hinv J hJpi)

The frame transports verbatim to the restricted cover.

Equations

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

noncomputable def Q2Presentation.Lifting.restrictKernel {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) (hJpi : Function.Surjective ⇑((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).piY.comp J.subtype)) : ElementaryKernel (restrictTarget E lam hinv J hJpi)

The restricted deck kernel: R/ker λ seen inside p_λ⁻¹(J), an elementary kernel of the restricted target (all fields restrict from scalarRelKernel's; hne-free).

Equations

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

theorem Q2Presentation.Lifting.card_restrictKernel_eq_two {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) (hJpi : Function.Surjective ⇑((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).piY.comp J.subtype)) (hne : lam ≠ 0) : Nat.card (NAdd (restrictKernel E lam hinv J hJpi)) = 2

The restricted deck kernel has order 2 for λ ≠ 0 (the sole hne-consumer of this file; the huni := 8 input of eq:recursionR3).

Noether at the stratum: (p_λ⁻¹(J))/(R/ker λ) ≃* J

noncomputable def Q2Presentation.Lifting.restrictDescend {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) (hJpi : Function.Surjective ⇑((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).piY.comp J.subtype)) : (restrictTarget E lam hinv J hJpi).Y ⧸ (restrictKernel E lam hinv J hJpi).N →* ↥J

The descended hom (the mChildDescend idiom, MChildPair.lean:245).

Equations

• Q2Presentation.Lifting.restrictDescend E lam hinv J hJpi = QuotientGroup.lift (Q2Presentation.Lifting.restrictKernel E lam hinv J hJpi).N (Q2Presentation.Lifting.restrictProj E lam hinv J) ⋯

@[simp]

theorem Q2Presentation.Lifting.restrictDescend_mk {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) (hJpi : Function.Surjective ⇑((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).piY.comp J.subtype)) (z : (restrictTarget E lam hinv J hJpi).Y) : (restrictDescend E lam hinv J hJpi) ((QuotientGroup.mk' (restrictKernel E lam hinv J hJpi).N) z) = (restrictProj E lam hinv J) z

theorem Q2Presentation.Lifting.restrictDescend_bijective {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) (hJpi : Function.Surjective ⇑((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).piY.comp J.subtype)) : Function.Bijective ⇑(restrictDescend E lam hinv J hJpi)

noncomputable def Q2Presentation.Lifting.restrictCollapse {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) (hJpi : Function.Surjective ⇑((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).piY.comp J.subtype)) : (restrictTarget E lam hinv J hJpi).Y ⧸ (restrictKernel E lam hinv J hJpi).N ≃* ↥J

Noether at the stratum (P2 §7.4's recorded gap): the restricted cover collapses onto the image stratum.

Equations

• Q2Presentation.Lifting.restrictCollapse E lam hinv J hJpi = MulEquiv.ofBijective (Q2Presentation.Lifting.restrictDescend E lam hinv J hJpi) ⋯

theorem Q2Presentation.Lifting.restrictCollapse_mk {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) (hJpi : Function.Surjective ⇑((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).piY.comp J.subtype)) (z : (restrictTarget E lam hinv J hJpi).Y) : (restrictCollapse E lam hinv J hJpi) ((QuotientGroup.mk' (restrictKernel E lam hinv J hJpi).N) z) = (restrictProj E lam hinv J) z

theorem Q2Presentation.Lifting.qYMap_restrictCollapse_symm {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) (hJpi : Function.Surjective ⇑((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).piY.comp J.subtype)) (x : ↥J) : (TorsorProgram.quotientFramedTarget (restrictTarget E lam hinv J hJpi) (restrictKernel E lam hinv J hJpi).N ⋯ ⋯).qYMap ((restrictCollapse E lam hinv J hJpi).symm x) = ((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).exactImageTarget J hJpi).qYMap x

Framing data of the restricted-cover child agrees with the framing data of the image stratum across the collapse (idiom: qYMap_scalarCollapse_symm, ScalarPushout.lean:403).

The marked-kernel transport (measure leg)

theorem Q2Presentation.Lifting.restrictCollapse_mem_childLY {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) (hJpi : Function.Surjective ⇑((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).piY.comp J.subtype)) (x : (restrictTarget E lam hinv J hJpi).Y ⧸ (restrictKernel E lam hinv J hJpi).N) (hx : x ∈ (TorsorProgram.quotientFramedTarget (restrictTarget E lam hinv J hJpi) (restrictKernel E lam hinv J hJpi).N ⋯ ⋯).LY) : (restrictCollapse E lam hinv J hJpi) x ∈ (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).LY.subgroupOf J

The collapse carries the restricted-cover child's marked kernel into the stratum's marked kernel (idiom: scalarCollapse_mem_childLY).

theorem Q2Presentation.Lifting.restrictCollapse_symm_mem_childLY {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) (hJpi : Function.Surjective ⇑((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).piY.comp J.subtype)) (y : ↥J) (hy : y ∈ (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).LY.subgroupOf J) : (restrictCollapse E lam hinv J hJpi).symm y ∈ (TorsorProgram.quotientFramedTarget (restrictTarget E lam hinv J hJpi) (restrictKernel E lam hinv J hJpi).N ⋯ ⋯).LY

The inverse collapse carries the stratum's marked kernel into the restricted-cover child's marked kernel.

noncomputable def Q2Presentation.Lifting.restrictChildLYEquiv {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) (hJpi : Function.Surjective ⇑((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).piY.comp J.subtype)) : ↥(TorsorProgram.quotientFramedTarget (restrictTarget E lam hinv J hJpi) (restrictKernel E lam hinv J hJpi).N ⋯ ⋯).LY ≃ ↥((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).LY.subgroupOf J)

The collapse restricts to a bijection of marked kernels: the restricted child and the image stratum have the SAME framed measure.

Equations

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

theorem Q2Presentation.Lifting.restrictChild_LY_card {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) (hJpi : Function.Surjective ⇑((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).piY.comp J.subtype)) : Nat.card ↥(TorsorProgram.quotientFramedTarget (restrictTarget E lam hinv J hJpi) (restrictKernel E lam hinv J hJpi).N ⋯ ⋯).LY = Nat.card ↥((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).LY.subgroupOf J)

Child-LY transport (the measure leg of eq:properweighteddescent): the restricted child's marked kernel has the stratum's card.

The child bridge (the scalarCoverChildEquiv idiom)

def Q2Presentation.Lifting.restrictCollapseHom {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) (hJpi : Function.Surjective ⇑((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).piY.comp J.subtype)) : ProfiniteGrp.ofFiniteGrp (FiniteGrp.of ((restrictTarget E lam hinv J hJpi).Y ⧸ (restrictKernel E lam hinv J hJpi).N)) ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of ((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).exactImageTarget J hJpi).Y)

The forward collapse as a hom of finite discrete profinite groups.

Equations

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

def Q2Presentation.Lifting.restrictCollapseInvHom {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) (hJpi : Function.Surjective ⇑((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).piY.comp J.subtype)) : ProfiniteGrp.ofFiniteGrp (FiniteGrp.of ((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).exactImageTarget J hJpi).Y) ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of ((restrictTarget E lam hinv J hJpi).Y ⧸ (restrictKernel E lam hinv J hJpi).N))

The inverse collapse as a hom of finite discrete profinite groups.

Equations

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

noncomputable def Q2Presentation.Lifting.restrictChildEquiv {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) (hJpi : Function.Surjective ⇑((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).piY.comp J.subtype)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) : boundaryFramedSurj B ((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).exactImageTarget J hJpi) ((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).exactImageFrame J hJpi (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) ≃ boundaryFramedSurj B (TorsorProgram.quotientFramedTarget (restrictTarget E lam hinv J hJpi) (restrictKernel E lam hinv J hJpi).N ⋯ ⋯) (TorsorProgram.quotientFrame (restrictTarget E lam hinv J hJpi) (restrictKernel E lam hinv J hJpi).N ⋯ ⋯ (restrictFrame E lam hinv J hJpi F))

The child bridge: framed surjections onto the image stratum J (child level) biject with framed surjections onto the restricted cover's child (post-composition with the collapse; idiom: scalarCoverChildEquiv, ScalarCoverPartition.lean:83).

Equations

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

Liftability transport (the ∃-raw-hom shape)

theorem Q2Presentation.Lifting.restrictTarget_qYMap {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) (hJpi : Function.Surjective ⇑((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).piY.comp J.subtype)) (z : (restrictTarget E lam hinv J hJpi).Y) : (restrictTarget E lam hinv J hJpi).qYMap z = (scalarCoverTarget E lam hinv).qYMap ((coverRestrictAmb E lam hinv J).subtype z)

qYMap-readout of the restricted target (single-step reduction).

def Q2Presentation.Lifting.coverCorestrict {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) (hJpi : Function.Surjective ⇑((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).piY.comp J.subtype)) {Γ : ProfiniteGrp.{0}} (f : Γ ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (scalarCoverTarget E lam hinv).Y)) (hf : ∀ (γ : ↑Γ.toProfinite.toTop), (ProfiniteGrp.Hom.hom f) γ ∈ coverRestrictAmb E lam hinv J) : Γ ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (restrictTarget E lam hinv J hJpi).Y)

Corestriction of an ambient hom with values in p_λ⁻¹(J) into the restricted target (the stratumCorestrict continuity pattern, weak-map version — no surjectivity).

Equations

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

@[simp]

theorem Q2Presentation.Lifting.coverCorestrict_val {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) (hJpi : Function.Surjective ⇑((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).piY.comp J.subtype)) {Γ : ProfiniteGrp.{0}} (f : Γ ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (scalarCoverTarget E lam hinv).Y)) (hf : ∀ (γ : ↑Γ.toProfinite.toTop), (ProfiniteGrp.Hom.hom f) γ ∈ coverRestrictAmb E lam hinv J) (γ : ↑Γ.toProfinite.toTop) : (coverRestrictAmb E lam hinv J).subtype ((ProfiniteGrp.Hom.hom (coverCorestrict E lam hinv J hJpi f hf)) γ) = (ProfiniteGrp.Hom.hom f) γ

theorem Q2Presentation.Lifting.restrictLiftHom_iff_exists {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (J : Subgroup (Yt.Y ⧸ E.N)) (hJpi : Function.Surjective ⇑((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).piY.comp J.subtype)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (h : boundaryFramedSurj B ((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).exactImageTarget J hJpi) ((TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).exactImageFrame J hJpi (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F))) : Nonempty (TorsorProgram.liftHom (restrictTarget E lam hinv J hJpi) (restrictKernel E lam hinv J hJpi).N ⋯ ⋯ B (restrictFrame E lam hinv J hJpi F) ((restrictChildEquiv E lam hinv J hJpi B F) h)) ↔ ∃ (ft : Γ ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (scalarCoverTarget E lam hinv).Y)), (∀ (γ : ↑Γ.toProfinite.toTop), (scalarCoverProj E lam hinv) ((ProfiniteGrp.Hom.hom ft) γ) = TorsorProgram.stratumVal (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) ((ProfiniteGrp.Hom.hom (↑h).hom) γ)) ∧ ∀ (γ : ↑Γ.toProfinite.toTop), (scalarCoverTarget E lam hinv).qYMap ((ProfiniteGrp.Hom.hom ft) γ) = (ProfiniteGrp.Hom.hom F.beta) ((ProfiniteGrp.Hom.hom B.toBoundary) γ)

Liftability transport: a stratum surjection h admits a weak lift through the RESTRICTED cover iff some framed hom into B_λ projects onto h's values — the raw-hom ∃-shape of scalarCoverLiftHom_iff_exists, so that P4-V3's properCoverLiftable bridges by pointwise Iff (design §6.3: the corestriction is a THEOREM, not baked into the predicate).