theorem Q2Presentation.Lifting.NAdd_add_eq_zero_iff {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (a b : NAdd E) : a + b = 0 ↔ a = b

Char-2 cancellation in the kernel module: a sum vanishes iff the summands agree.

ker λ as an ambient subgroup

def Q2Presentation.Lifting.scalarKernel {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) : Subgroup Yt.Y

ker λ as a subgroup of the ambient target: the additive kernel of lam inside NAdd E, read back multiplicatively and pushed along the subtype.

Equations

• Q2Presentation.Lifting.scalarKernel E lam = Subgroup.map E.N.subtype (AddSubgroup.toSubgroup' (LinearMap.ker lam).toAddSubgroup)

theorem Q2Presentation.Lifting.scalarKernel_le {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) : scalarKernel E lam ≤ E.N

theorem Q2Presentation.Lifting.mem_scalarKernel_of_ker {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (x : ↥E.N) (hx : lam (Additive.ofMul x) = 0) : ↑x ∈ scalarKernel E lam

Kernel elements of lam land in ker λ (bundled form).

theorem Q2Presentation.Lifting.lam_eq_zero_of_mem_scalarKernel {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (x : ↥E.N) (hx : ↑x ∈ scalarKernel E lam) : lam (Additive.ofMul x) = 0

lam kills ker λ (bundled form).

theorem Q2Presentation.Lifting.mem_scalarKernel {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (y : Yt.Y) : y ∈ scalarKernel E lam ↔ ∃ (h : y ∈ E.N), lam (Additive.ofMul ⟨y, h⟩) = 0

theorem Q2Presentation.Lifting.scalarKernel_le_LY {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) : scalarKernel E lam ≤ Yt.LY

theorem Q2Presentation.Lifting.scalarKernel_theta {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (n : Yt.Y) : n ∈ scalarKernel E lam → Yt.thetaY n = 1

theorem Q2Presentation.Lifting.scalarKernel_normal {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) : (scalarKernel E lam).Normal

Normality from invariance (lem:obstructionseparation l.4230–4231): λ ∈ (R^∨)^Y makes ker λ conjugation-stable. Mind the right-conjugation orientation conjEndN E y m = y⁻¹ m y: normality needs y n y⁻¹ ∈ ker λ, so invariance is applied at y⁻¹.

The cover target and its frame

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

The scalar pushout target B_λ = Y/ker λ as a framed target (same H, E, frame; eq:targettower refined by l.4219–4223).

Equations

• Q2Presentation.Lifting.scalarCoverTarget E lam hinv = Q2Presentation.TorsorProgram.quotientFramedTarget Yt (Q2Presentation.Lifting.scalarKernel E lam) ⋯ ⋯

def Q2Presentation.Lifting.scalarCoverFrame {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (F : BoundaryFrame Yt) : BoundaryFrame (scalarCoverTarget E lam hinv)

The frame transports verbatim to the scalar pushout target.

Equations

• Q2Presentation.Lifting.scalarCoverFrame E lam hinv F = Q2Presentation.TorsorProgram.quotientFrame Yt (Q2Presentation.Lifting.scalarKernel E lam) ⋯ ⋯ F

instance Q2Presentation.Lifting.instFiniteYScalarCoverTarget {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) : Finite (scalarCoverTarget E lam hinv).Y

def Q2Presentation.Lifting.scalarProj {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) : Yt.Y →* (scalarCoverTarget E lam hinv).Y

The scalar projection Y → B_λ = Y/ker λ (the quotient map, with the normality instance packaged so statements stay instance-clean).

Equations

• Q2Presentation.Lifting.scalarProj E lam hinv = QuotientGroup.mk' (Q2Presentation.Lifting.scalarKernel E lam)

The relative kernel R/ker λ

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

The relative kernel R/ker λ ≤ B_λ — the deck kernel of the central double cover, as an elementary kernel of the cover target. It is Subgroup.map-spelled so Noether III applies on the nose.

Equations

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

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

The multiplicative projection R → R/ker λ (corestricted).

Equations

• Q2Presentation.Lifting.scalarRelProjMul E lam hinv = { toFun := fun (x : ↥E.N) => ⟨(QuotientGroup.mk' (Q2Presentation.Lifting.scalarKernel E lam)) ↑x, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

def Q2Presentation.Lifting.scalarRelProj {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) : NAdd E →ₗ[ZMod 2] NAdd (scalarRelKernel E lam hinv)

The induced 𝔽₂-linear surjection mkN : NAdd E →ₗ NAdd (R/ker λ) (idiom: conjEndN, CocycleBridge.lean).

Equations

• Q2Presentation.Lifting.scalarRelProj E lam hinv = { toFun := ⇑(MonoidHom.toAdditive (Q2Presentation.Lifting.scalarRelProjMul E lam hinv)), map_add' := ⋯, map_smul' := ⋯ }

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

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

The kernel of the induced projection is exactly ker λ (membership chase through QuotientGroup.eq_one_iff).

The double cover is double, and central

theorem Q2Presentation.Lifting.card_relKernel_eq_two {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (hne : lam ≠ 0) : Nat.card (NAdd (scalarRelKernel E lam hinv)) = 2

The double cover is double: |R/ker λ| = 2 for λ ≠ 0.

theorem Q2Presentation.Lifting.conjEndN_relKernel_eq_one {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (hne : lam ≠ 0) (y : (scalarCoverTarget E lam hinv).Y) : conjEndN (scalarRelKernel E lam hinv) y = 1

Every conjugation operator on the relative kernel is the identity ("C acts trivially on R/ker λ", l.4231; free from card 2 + bijectivity — invariance is not consumed here).

theorem Q2Presentation.Lifting.scalarRelKernel_le_center {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (hne : lam ≠ 0) : (scalarRelKernel E lam hinv).N ≤ Subgroup.center (scalarCoverTarget E lam hinv).Y

The double cover is central: R/ker λ ≤ Z(B_λ).

theorem Q2Presentation.Lifting.card_scalarCoverTarget_even {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (hne : lam ≠ 0) : 2 ∣ Nat.card (scalarCoverTarget E lam hinv).Y

theorem Q2Presentation.Lifting.scalarCover_hodd {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (hne : lam ≠ 0) : Odd (omega2Mod (Nat.card (scalarCoverTarget E lam hinv).Y)).val

The oddness input for the rows diagonal at the cover target: no card_Y_even-style input is needed — Lagrange at the order-2 relative kernel supplies evenness (idiom: xr_hodd, XRObstruction.lean).

The child transport (Noether III) and the cover-lift type

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

Noether III at the tower ker λ ≤ R ≤ Y: (Y/ker λ)/(R/ker λ) ≃* Y/R. The relative kernel is Subgroup.map-spelled, so the Mathlib equivalence applies on the nose.

Equations

• Q2Presentation.Lifting.scalarCollapse E lam hinv = QuotientGroup.quotientQuotientEquivQuotient (Q2Presentation.Lifting.scalarKernel E lam) E.N ⋯

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

The cover projection p_λ : B_λ → B = Y/R, descended along the identity (QuotientGroup.map).

Equations

• Q2Presentation.Lifting.scalarCoverProj E lam hinv = QuotientGroup.map (Q2Presentation.Lifting.scalarKernel E lam) E.N (MonoidHom.id Yt.Y) ⋯

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

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

The forward collapse of a single-level class is the cover projection (quotientQuotientEquivQuotientAux_mk).

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

def Q2Presentation.Lifting.scalarCollapseInvHom {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) : ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Yt.Y ⧸ E.N)) ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of ((scalarCoverTarget E lam hinv).Y ⧸ (scalarRelKernel E lam hinv).N))

The inverse collapse as a hom of finite discrete profinite groups (idiom: projHom, LiftFibration.lean).

Equations

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

theorem Q2Presentation.Lifting.qYMap_scalarCollapse_symm {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (x : Yt.Y ⧸ E.N) : (TorsorProgram.quotientFramedTarget (scalarCoverTarget E lam hinv) (scalarRelKernel E lam hinv).N ⋯ ⋯).qYMap ((scalarCollapse E lam hinv).symm x) = (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯).qYMap x

The framing data of the double-quotient cover target agrees with the framing data of the plain child target across the collapse.

def Q2Presentation.Lifting.scalarCoverChild {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget (scalarCoverTarget E lam hinv) (scalarRelKernel E lam hinv).N ⋯ ⋯) (TorsorProgram.quotientFrame (scalarCoverTarget E lam hinv) (scalarRelKernel E lam hinv).N ⋯ ⋯ (scalarCoverFrame E lam hinv F))

The child seen below the cover: transport a child-framed surjection across the collapse (B_λ)/(R/ker λ) ≃* Y/R.

Equations

• Q2Presentation.Lifting.scalarCoverChild E lam hinv B F g = ⟨{ hom := CategoryTheory.CategoryStruct.comp (↑g).hom (Q2Presentation.Lifting.scalarCollapseInvHom E lam hinv), surj := ⋯ }, ⋯⟩

theorem Q2Presentation.Lifting.scalarCoverChild_hom_apply {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (γ : ↑Γ.toProfinite.toTop) : (ProfiniteGrp.Hom.hom (↑(scalarCoverChild E lam hinv B F g)).hom) γ = (scalarCollapse E lam hinv).symm ((ProfiniteGrp.Hom.hom (↑g).hom) γ)

def Q2Presentation.Lifting.scalarCoverLiftHom {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) : Type

Cover lifts of g (lem:obstructionseparation l.4219–4223): framed homs Γ ⟶ B_λ over g — surjectivity NOT imposed (the manuscript's compatible lifts: λ_*o measures weak liftability; images are stratified by eq:recursionR2/R3 later).

Equations

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

theorem Q2Presentation.Lifting.scalarCoverLiftHom_iff_exists {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) : Nonempty (scalarCoverLiftHom E lam hinv B F g) ↔ ∃ (f : Γ ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (scalarCoverTarget E lam hinv).Y)), (∀ (γ : ↑Γ.toProfinite.toTop), (scalarCoverProj E lam hinv) ((ProfiniteGrp.Hom.hom f) γ) = (ProfiniteGrp.Hom.hom (↑g).hom) γ) ∧ ∀ (γ : ↑Γ.toProfinite.toTop), (scalarCoverTarget E lam hinv).qYMap ((ProfiniteGrp.Hom.hom f) γ) = (ProfiniteGrp.Hom.hom F.beta) ((ProfiniteGrp.Hom.hom B.toBoundary) γ)

Unfolding for P2 consumers: a cover lift is an honest framed hom to B_λ whose composite with the cover projection is g.