structure Q2Presentation.Lifting.CocycleExt (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) : Type

The carrier of the central extension Yt.Y ×_ζ 𝔽₂ determined by a normalized 2-cocycle ζ (manuscript l.4371–4372). A structure rather than a product-type synonym, so the twisted group instance below is canonical (keyed on the full cocycle datum) and cannot collide with the product instances; the normalization and cocycle laws are phantom parameters.

• base : Yt.Y

  The base coordinate.

• scal : ZMod 2

  The scalar (deck) coordinate.

theorem Q2Presentation.Lifting.CocycleExt.ext_iff {Yt : BoundaryFramedTarget} {zeta : Yt.Y → Yt.Y → ZMod 2} {hz1 : ∀ (y : Yt.Y), zeta 1 y = 0} {hz2 : ∀ (y : Yt.Y), zeta y 1 = 0} {hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)} {x y : CocycleExt Yt zeta hz1 hz2 hzc} : x = y ↔ x.base = y.base ∧ x.scal = y.scal

theorem Q2Presentation.Lifting.CocycleExt.ext {Yt : BoundaryFramedTarget} {zeta : Yt.Y → Yt.Y → ZMod 2} {hz1 : ∀ (y : Yt.Y), zeta 1 y = 0} {hz2 : ∀ (y : Yt.Y), zeta y 1 = 0} {hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)} {x y : CocycleExt Yt zeta hz1 hz2 hzc} (base : x.base = y.base) (scal : x.scal = y.scal) : x = y

The twisted group law

instance Q2Presentation.Lifting.instGroupCocycleExt (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) : Group (CocycleExt Yt zeta hz1 hz2 hzc)

Equations

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

@[simp]

theorem Q2Presentation.Lifting.CocycleExt.mul_base (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) (a b : CocycleExt Yt zeta hz1 hz2 hzc) : (a * b).base = a.base * b.base

@[simp]

theorem Q2Presentation.Lifting.CocycleExt.mul_scal (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) (a b : CocycleExt Yt zeta hz1 hz2 hzc) : (a * b).scal = a.scal + b.scal + zeta a.base b.base

@[simp]

theorem Q2Presentation.Lifting.CocycleExt.one_base (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) : base 1 = 1

@[simp]

theorem Q2Presentation.Lifting.CocycleExt.one_scal (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) : scal 1 = 0

instance Q2Presentation.Lifting.instFiniteCocycleExt (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) : Finite (CocycleExt Yt zeta hz1 hz2 hzc)

The deck projection and its kernel

def Q2Presentation.Lifting.cocycleProj (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) : CocycleExt Yt zeta hz1 hz2 hzc →* Yt.Y

First projection as a hom — the deck projection p_ζ (the scalar twist cancels in the base coordinate).

Equations

• Q2Presentation.Lifting.cocycleProj Yt zeta hz1 hz2 hzc = { toFun := Q2Presentation.Lifting.CocycleExt.base, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Q2Presentation.Lifting.cocycleProj_apply (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) (x : CocycleExt Yt zeta hz1 hz2 hzc) : (cocycleProj Yt zeta hz1 hz2 hzc) x = x.base

def Q2Presentation.Lifting.cocycleSec (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) (y : Yt.Y) : CocycleExt Yt zeta hz1 hz2 hzc

The tautological set-section y ↦ (y, 0) (not a hom; hygiene def for statements mixing the two carriers).

Equations

• Q2Presentation.Lifting.cocycleSec Yt zeta hz1 hz2 hzc y = { base := y, scal := 0 }

@[simp]

theorem Q2Presentation.Lifting.cocycleProj_sec (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) (y : Yt.Y) : (cocycleProj Yt zeta hz1 hz2 hzc) (cocycleSec Yt zeta hz1 hz2 hzc y) = y

theorem Q2Presentation.Lifting.cocycleProj_surjective (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) : Function.Surjective ⇑(cocycleProj Yt zeta hz1 hz2 hzc)

theorem Q2Presentation.Lifting.base_eq_one_of_mem_ker (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) {x : CocycleExt Yt zeta hz1 hz2 hzc} (hx : x ∈ (cocycleProj Yt zeta hz1 hz2 hzc).ker) : x.base = 1

Deck-kernel membership reads as base-triviality.

theorem Q2Presentation.Lifting.mul_self_of_base_one (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) (x : CocycleExt Yt zeta hz1 hz2 hzc) (hx : x.base = 1) : x * x = 1

Base-trivial elements square to 1 (char-2 fibre + normalization).

theorem Q2Presentation.Lifting.cocycleProj_ker_isTwoGroup (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) : IsPGroup 2 ↥(cocycleProj Yt zeta hz1 hz2 hzc).ker

The deck kernel is a 2-group (feeds the pulled-back L̃'s 2-group property through IsPGroup.comap_of_ker_isPGroup).

The framed cover target (pulled-back framing)

def Q2Presentation.Lifting.cocycleCoverTarget (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) : BoundaryFramedTarget

The cocycle-cover framed target: the extension carries the PULLED-BACK boundary framing of lem:covertransform (l.3822–3830): L̃ = p_ζ⁻¹(L), π̃ = π ∘ p_ζ, θ̃ = θ ∘ p_ζ, same H and E.

Equations

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

The order-2 elementary deck kernel

def Q2Presentation.Lifting.cocycleKernel (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) : ElementaryKernel (cocycleCoverTarget Yt zeta hz1 hz2 hzc)

The deck kernel as an order-2 elementary kernel — discharging exactly the obligation P2 recorded for P7 (BLOCKR_P2_DESIGN.md §7.4): comm and exp2 come from the normalized-cocycle law on base-trivial elements, so no centrality is assumed anywhere.

Equations

• Q2Presentation.Lifting.cocycleKernel Yt zeta hz1 hz2 hzc = { N := (Q2Presentation.Lifting.cocycleProj Yt zeta hz1 hz2 hzc).ker, normal := ⋯, le_LY := ⋯, theta_dies := ⋯, comm := ⋯, exp2 := ⋯ }

def Q2Presentation.Lifting.cocycleKerEquiv (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) : ↥(cocycleProj Yt zeta hz1 hz2 hzc).ker ≃ ZMod 2

The deck kernel is 𝔽₂ on the nose: (1, t) ↦ t.

Equations

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

theorem Q2Presentation.Lifting.card_cocycleKernel_eq_two (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) : Nat.card (NAdd (cocycleKernel Yt zeta hz1 hz2 hzc)) = 2

The deck kernel has order 2 — the hcard input of the GREEN uniform-8 counts (cover_Z1_card_gammaA / cover_Z1_card_gq2).

The collapse C_ζ/ker p_ζ ≃* C and the transported frame

def Q2Presentation.Lifting.cocycleCollapse (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) : (cocycleCoverTarget Yt zeta hz1 hz2 hzc).Y ⧸ (cocycleKernel Yt zeta hz1 hz2 hzc).N ≃* Yt.Y

The collapse of the cover child onto the base (Noether I at the deck projection p_ζ).

Equations

• Q2Presentation.Lifting.cocycleCollapse Yt zeta hz1 hz2 hzc = QuotientGroup.quotientKerEquivOfSurjective (Q2Presentation.Lifting.cocycleProj Yt zeta hz1 hz2 hzc) ⋯

@[simp]

theorem Q2Presentation.Lifting.cocycleCollapse_mk (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) (z : (cocycleCoverTarget Yt zeta hz1 hz2 hzc).Y) : (cocycleCollapse Yt zeta hz1 hz2 hzc) ((QuotientGroup.mk' (cocycleKernel Yt zeta hz1 hz2 hzc).N) z) = (cocycleProj Yt zeta hz1 hz2 hzc) z

theorem Q2Presentation.Lifting.cocycleCollapse_symm_mk (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) (y : Yt.Y) : (cocycleCollapse Yt zeta hz1 hz2 hzc).symm y = (QuotientGroup.mk' (cocycleKernel Yt zeta hz1 hz2 hzc).N) (cocycleSec Yt zeta hz1 hz2 hzc y)

def Q2Presentation.Lifting.cocycleCollapseHom (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) : ProfiniteGrp.ofFiniteGrp (FiniteGrp.of ((cocycleCoverTarget Yt zeta hz1 hz2 hzc).Y ⧸ (cocycleKernel Yt zeta hz1 hz2 hzc).N)) ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of Yt.Y)

The forward collapse as a hom of finite discrete profinite groups (idiom: scalarCollapseHom, Induction/ScalarCoverPartition.lean).

Equations

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

@[simp]

theorem Q2Presentation.Lifting.cocycleCollapseHom_apply (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) (x : (cocycleCoverTarget Yt zeta hz1 hz2 hzc).Y ⧸ (cocycleKernel Yt zeta hz1 hz2 hzc).N) : (ProfiniteGrp.Hom.hom (cocycleCollapseHom Yt zeta hz1 hz2 hzc)) x = (cocycleCollapse Yt zeta hz1 hz2 hzc) x

def Q2Presentation.Lifting.cocycleCollapseInvHom (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) : ProfiniteGrp.ofFiniteGrp (FiniteGrp.of Yt.Y) ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of ((cocycleCoverTarget Yt zeta hz1 hz2 hzc).Y ⧸ (cocycleKernel Yt zeta hz1 hz2 hzc).N))

The inverse collapse as a hom of finite discrete profinite groups (idiom: scalarCollapseInvHom, Lifting/ScalarPushout.lean).

Equations

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

theorem Q2Presentation.Lifting.qYMap_cocycleCollapse_symm (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) (x : Yt.Y) : (TorsorProgram.quotientFramedTarget (cocycleCoverTarget Yt zeta hz1 hz2 hzc) (cocycleKernel Yt zeta hz1 hz2 hzc).N ⋯ ⋯).qYMap ((cocycleCollapse Yt zeta hz1 hz2 hzc).symm x) = Yt.qYMap x

The framing data of the cover child agrees with the base framing across the collapse (mirror of qYMap_scalarCollapse_symm).

def Q2Presentation.Lifting.cocycleCoverFrame (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) (F : BoundaryFrame Yt) : BoundaryFrame (cocycleCoverTarget Yt zeta hz1 hz2 hzc)

The same boundary frame frames the cover: H and E are unchanged on the nose (mirror of quotientFrame/exactImageFrame).

Equations

• Q2Presentation.Lifting.cocycleCoverFrame Yt zeta hz1 hz2 hzc F = { alpha := F.alpha, alpha_surj := ⋯, psi := F.psi, beta := F.beta, beta_def := ⋯ }

Child transport and the weak cover-lift set

def Q2Presentation.Lifting.cocycleCoverChild (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B Yt F) : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget (cocycleCoverTarget Yt zeta hz1 hz2 hzc) (cocycleKernel Yt zeta hz1 hz2 hzc).N ⋯ ⋯) (TorsorProgram.quotientFrame (cocycleCoverTarget Yt zeta hz1 hz2 hzc) (cocycleKernel Yt zeta hz1 hz2 hzc).N ⋯ ⋯ (cocycleCoverFrame Yt zeta hz1 hz2 hzc F))

The base child seen below the cover: transport of a base framed surjection across the collapse (mirror of scalarCoverChild).

Equations

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

theorem Q2Presentation.Lifting.cocycleCoverChild_hom_apply (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B Yt F) (γ : ↑Γ.toProfinite.toTop) : (ProfiniteGrp.Hom.hom (↑(cocycleCoverChild Yt zeta hz1 hz2 hzc B F g)).hom) γ = (cocycleCollapse Yt zeta hz1 hz2 hzc).symm ((ProfiniteGrp.Hom.hom (↑g).hom) γ)

def Q2Presentation.Lifting.cocycleChildEquiv (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) : boundaryFramedSurj B Yt F ≃ boundaryFramedSurj B (TorsorProgram.quotientFramedTarget (cocycleCoverTarget Yt zeta hz1 hz2 hzc) (cocycleKernel Yt zeta hz1 hz2 hzc).N ⋯ ⋯) (TorsorProgram.quotientFrame (cocycleCoverTarget Yt zeta hz1 hz2 hzc) (cocycleKernel Yt zeta hz1 hz2 hzc).N ⋯ ⋯ (cocycleCoverFrame Yt zeta hz1 hz2 hzc F))

Child transport is a bijection (mirror of scalarCoverChildEquiv): post-composition with the collapse identifies the base framed surjections with the cover's own child framed surjections.

Equations

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

@[reducible, inline]

noncomputable abbrev Q2Presentation.Lifting.cocycleCoverLiftHom (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B Yt F) : Type

The weak cover-lift set of a base framed surjection — the splitting-indicator carrier of lem:phasecover: Nonempty ⟺ ρ*ζ is unobstructed (l.4377–4379). Surjectivity onto C_ζ is NOT imposed (weak lifts, the P1 §5.1-vetted reading).

Equations

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

theorem Q2Presentation.Lifting.cocycleCoverLiftHom_iff_exists (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B Yt F) : Nonempty (cocycleCoverLiftHom Yt zeta hz1 hz2 hzc B F g) ↔ ∃ (f : Γ ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (cocycleCoverTarget Yt zeta hz1 hz2 hzc).Y)), (∀ (γ : ↑Γ.toProfinite.toTop), (cocycleProj Yt zeta hz1 hz2 hzc) ((ProfiniteGrp.Hom.hom f) γ) = (ProfiniteGrp.Hom.hom (↑g).hom) γ) ∧ ∀ (γ : ↑Γ.toProfinite.toTop), (cocycleCoverTarget Yt zeta hz1 hz2 hzc).qYMap ((ProfiniteGrp.Hom.hom f) γ) = (ProfiniteGrp.Hom.hom F.beta) ((ProfiniteGrp.Hom.hom B.toBoundary) γ)

Raw-hom unfolding (mirror of scalarCoverLiftHom_iff_exists): unobstructedness is literally "a framed hom to C_ζ over g exists" — the manuscript's split-pullback form.

The marked-kernel cardinalities (eq:phasecoverdescent bookkeeping)

def Q2Presentation.Lifting.cocycleLYEquiv (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) : ↥(Subgroup.comap (cocycleProj Yt zeta hz1 hz2 hzc) Yt.LY) ≃ ↥Yt.LY × ZMod 2

The pulled-back wild kernel is L × 𝔽₂ as a set.

Equations

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

theorem Q2Presentation.Lifting.cocycleCover_LY_card (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) : Nat.card ↥(cocycleCoverTarget Yt zeta hz1 hz2 hzc).LY = 2 * Nat.card ↥Yt.LY

|L̃| = 2·|L| — the equality half of eq:phasecoverdescent (l.4411–4413): the pulled-back wild kernel doubles the base one.

theorem Q2Presentation.Lifting.cocycleCollapse_mem_LY (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) (x : (cocycleCoverTarget Yt zeta hz1 hz2 hzc).Y ⧸ (cocycleKernel Yt zeta hz1 hz2 hzc).N) (hx : x ∈ (TorsorProgram.quotientFramedTarget (cocycleCoverTarget Yt zeta hz1 hz2 hzc) (cocycleKernel Yt zeta hz1 hz2 hzc).N ⋯ ⋯).LY) : (cocycleCollapse Yt zeta hz1 hz2 hzc) x ∈ Yt.LY

The collapse carries the cover-child marked kernel into the base marked kernel (mirror of scalarCollapse_mem_childLY).

theorem Q2Presentation.Lifting.cocycleCollapse_symm_mem_LY (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) (y : Yt.Y) (hy : y ∈ Yt.LY) : (cocycleCollapse Yt zeta hz1 hz2 hzc).symm y ∈ (TorsorProgram.quotientFramedTarget (cocycleCoverTarget Yt zeta hz1 hz2 hzc) (cocycleKernel Yt zeta hz1 hz2 hzc).N ⋯ ⋯).LY

The inverse collapse carries the base marked kernel into the cover-child marked kernel.

def Q2Presentation.Lifting.cocycleChildLYEquiv (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) : ↥(TorsorProgram.quotientFramedTarget (cocycleCoverTarget Yt zeta hz1 hz2 hzc) (cocycleKernel Yt zeta hz1 hz2 hzc).N ⋯ ⋯).LY ≃ ↥Yt.LY

The collapse restricts to a bijection of marked kernels — the cover child and the base have the SAME framed measure (mirror of scalarChildLYEquiv).

Equations

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

theorem Q2Presentation.Lifting.cocycleCover_child_LY_card (Yt : BoundaryFramedTarget) (zeta : Yt.Y → Yt.Y → ZMod 2) (hz1 : ∀ (y : Yt.Y), zeta 1 y = 0) (hz2 : ∀ (y : Yt.Y), zeta y 1 = 0) (hzc : ∀ (a b c : Yt.Y), zeta a b + zeta (a * b) c = zeta b c + zeta a (b * c)) : Nat.card ↥(TorsorProgram.quotientFramedTarget (cocycleCoverTarget Yt zeta hz1 hz2 hzc) (cocycleKernel Yt zeta hz1 hz2 hzc).N ⋯ ⋯).LY = Nat.card ↥Yt.LY

The cover-child marked kernel has the base cardinality — the second half of the eq:phasecoverdescent bookkeeping (stratum bound consumers rewrite through this).