Char-2 helpers on the head V = M/T

theorem Q2Presentation.Induction.edgeV_add_self {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (v : towerM K ⧸ towerT K) : v + v = 0

Every head vector is 2-torsion (V is a ZMod 2-module).

theorem Q2Presentation.Induction.edgeV_eq_of_add_eq_zero {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {v w : towerM K ⧸ towerT K} (h : v + w = 0) : v = w

Char-2 cancellation on the head: a vanishing sum means equality.

The fibre inclusion vInG is injective and onto vLayer

theorem Q2Presentation.Induction.vInG_eq_one {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (u : towerM K ⧸ towerT K) (hu : vInG chief K u = 1) : u = 0

Kernel triviality of the fibre inclusion: vInG u = 1 → u = 0 (the T-membership chase through mChildEquiv_mem_tChild_iff).

theorem Q2Presentation.Induction.vInG_injective {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Function.Injective (vInG chief K)

The fibre inclusion is injective (char-2 reduction to the kernel case).

theorem Q2Presentation.Induction.vInG_surjOn_vLayer {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (x : (btChild chief K).fst.Y) (hx : x ∈ vLayer chief K) : ∃ (v : towerM K ⧸ towerT K), vInG chief K v = x

The fibre inclusion is onto the V-layer (surjectivity of the M'-bridge, one T'-level up).

def Q2Presentation.Induction.vOut {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (x : (btChild chief K).fst.Y) : towerM K ⧸ towerT K

The choice-packaged partial inverse of vInG (total function; 0 off the V-layer).

Equations

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

theorem Q2Presentation.Induction.vOut_def {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (x : (btChild chief K).fst.Y) : vOut chief K x = if h : ∃ (v : towerM K ⧸ towerT K), vInG chief K v = x then h.choose else 0

The classical-dite def-form of vOut (cite this, never re-haveI a Decidable instance — the sGammaZ_def fix-class).

theorem Q2Presentation.Induction.vInG_vOut {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (x : (btChild chief K).fst.Y) (hx : x ∈ vLayer chief K) : vInG chief K (vOut chief K x) = x

theorem Q2Presentation.Induction.vOut_vInG {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (v : towerM K ⧸ towerT K) : vOut chief K (vInG chief K v) = v

The collapse B/T' → B/M' = C-child and the vLayer frame

bookkeeping (the qYMap/beta transports at the btChild carrier)

def Q2Presentation.Induction.btToC {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : (btChild chief K).fst.Y →* (cChild chief K).fst.Y

The child-tower collapse B/T' →* B/M' (T' ≤ M').

Equations

• Q2Presentation.Induction.btToC chief K = QuotientGroup.lift (Q2Presentation.Induction.tChild chief K) (QuotientGroup.mk' (Q2Presentation.Induction.mChild chief K)) ⋯

@[simp]

theorem Q2Presentation.Induction.btToC_mk {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (y : (XRZero.xrChild chief K).fst.Y) : (btToC chief K) ((QuotientGroup.mk' (tChild chief K)) y) = (QuotientGroup.mk' (mChild chief K)) y

theorem Q2Presentation.Induction.cChildCollapse_btToC {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (x : (btChild chief K).fst.Y) : (cChildCollapse chief K) ((btToC chief K) x) = (btProj chief K) x

The collapse computes btProj through cChildCollapse (the square B/T' → B/M' ≃ C commutes with the base projection).

theorem Q2Presentation.Induction.btToC_qYMap {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (x : (btChild chief K).fst.Y) : (cChild chief K).fst.qYMap ((btToC chief K) x) = (btChild chief K).fst.qYMap x

Frame transport across the collapse: the q_Y-data of a B/T'-point agrees with the q_Y-data of its C-child image.

theorem Q2Presentation.Induction.vLayer_le_btChild_LY {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : vLayer chief K ≤ (btChild chief K).fst.LY

The V-layer sits inside the marked kernel of B/T'.

theorem Q2Presentation.Induction.vLayer_theta {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (n : (btChild chief K).fst.Y) (hn : n ∈ vLayer chief K) : (btChild chief K).fst.thetaY n = 1

The decoration of B/T' kills the V-layer.

theorem Q2Presentation.Induction.btChild_piY_vLayer {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (n : (btChild chief K).fst.Y) (hn : n ∈ vLayer chief K) : (btChild chief K).fst.piY n = 1

The tame projection of B/T' kills the V-layer.

theorem Q2Presentation.Induction.btChild_qYMap_vLayer_mul {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (n : (btChild chief K).fst.Y) (hn : n ∈ vLayer chief K) (x : (btChild chief K).fst.Y) : (btChild chief K).fst.qYMap (n * x) = (btChild chief K).fst.qYMap x

q_Y is insensitive to left V-layer translation (the frame clause of a V⋊C-lift depends only on its C-part).

theorem Q2Presentation.Induction.btSection_one {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (s : towerC K → (btChild chief K).fst.Y) (hmul : ∀ (c d : towerC K), s c * s d = s (c * d)) : s 1 = 1

A multiplicative section of btProj is normalized.

The lower-map composite ρ̄ and the carrier Z¹_ρ(V)

def Q2Presentation.Induction.lowerBar {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (γ : ↑Γ.toProfinite.toTop) : towerC K

ρ̄ — the lower map read in C = towerC K (the headActE ∘ cChildCollapse-composite of the design).

Equations

• Q2Presentation.Induction.lowerBar chief K B ρ γ = (Q2Presentation.Induction.cChildCollapse chief K) ((ProfiniteGrp.Hom.hom (↑ρ).hom) γ)

theorem Q2Presentation.Induction.lowerBar_one {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : lowerBar chief K B ρ 1 = 1

theorem Q2Presentation.Induction.lowerBar_mul {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (γ γ' : ↑Γ.toProfinite.toTop) : lowerBar chief K B ρ (γ * γ') = lowerBar chief K B ρ γ * lowerBar chief K B ρ γ'

theorem Q2Presentation.Induction.lowerBar_isLocallyConstant {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : IsLocallyConstant (lowerBar chief K B ρ)

def Q2Presentation.Induction.edgeZ1Add {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : AddSubgroup (↑Γ.toProfinite.toTop → towerM K ⧸ towerT K)

The additive-subgroup carrier of Z¹_ρ(V).

Equations

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

def Q2Presentation.Induction.edgeZ1 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : Submodule (ZMod 2) (↑Γ.toProfinite.toTop → towerM K ⧸ towerT K)

Z¹_ρ(V) — the ZMod 2-module of continuous (locally constant) V-valued ρ̄-twisted 1-cocycles: z(γγ′) = z(γ) + ρ̄(γ)·z(γ′) (THE orientation pin — aRep_cocycle's house orientation; design §2.1's W_ρ, the engine carrier of the W2 instantiation).

Equations

• Q2Presentation.Induction.edgeZ1 chief K B ρ = (AddSubgroup.toZModSubmodule 2) (Q2Presentation.Induction.edgeZ1Add chief K B ρ)

theorem Q2Presentation.Induction.mem_edgeZ1 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (z : ↑Γ.toProfinite.toTop → towerM K ⧸ towerT K) : z ∈ edgeZ1 chief K B ρ ↔ IsLocallyConstant z ∧ ∀ (γ γ' : ↑Γ.toProfinite.toTop), z (γ * γ') = z γ + (headActE chief K (lowerBar chief K B ρ γ)) (z γ')

theorem Q2Presentation.Induction.edgeZ1_val_one {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) {z : ↑Γ.toProfinite.toTop → towerM K ⧸ towerT K} (hz : z ∈ edgeZ1 chief K B ρ) : z 1 = 0

A twisted cocycle vanishes at 1.

theorem Q2Presentation.Induction.edgeZ1_val_inv {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) {z : ↑Γ.toProfinite.toTop → towerM K ⧸ towerT K} (hz : z ∈ edgeZ1 chief K B ρ) (γ : ↑Γ.toProfinite.toTop) : z γ⁻¹ = (headActE chief K (lowerBar chief K B ρ γ⁻¹)) (z γ)

Values at inverses: z(γ⁻¹) = ρ̄(γ⁻¹)·z(γ) (char 2).

theorem Q2Presentation.Induction.edgeZ1_ext_on {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (S : Set ↑Γ.toProfinite.toTop) (hS : (Subgroup.closure S).topologicalClosure = ⊤) {z w : ↑Γ.toProfinite.toTop → towerM K ⧸ towerT K} (hz : z ∈ edgeZ1 chief K B ρ) (hw : w ∈ edgeZ1 chief K B ρ) (hagree : ∀ γ ∈ S, z γ = w γ) : z = w

Twisted-cocycle extensionality: two cocycles agreeing on a topologically generating set agree (the agreement locus is a CLOPEN subgroup — local constancy gives closedness with no topology on V).

theorem Q2Presentation.Induction.edgeZ1_finite_of_tfg {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (hP : Profinite.TopologicallyFinitelyGenerated Γ) : Finite ↥(edgeZ1 chief K B ρ)

Finiteness of Z¹_ρ(V) at a topologically finitely generated source (the tfg pattern of Profinite.tfg_hom_to_finite_finite, run at the cocycle carrier through edgeZ1_ext_on).

The per-source instances (tfg witnesses: centralCover_tfg_GammaA

for Γ_A; the recorded gq2_topologicallyFinitelyGenerated for G_ℚ₂)

instance Q2Presentation.Induction.instEdgeZ1FiniteGammaA {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (B : BoundaryPackage GammaA) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : Finite ↥(edgeZ1 chief K B ρ)

instance Q2Presentation.Induction.instEdgeZ1FiniteGQ2 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (B : BoundaryPackage GQ2Profinite) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : Finite ↥(edgeZ1 chief K B ρ)

noncomputable instance Q2Presentation.Induction.instEdgeZ1FintypeGammaA {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (B : BoundaryPackage GammaA) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : Fintype ↥(edgeZ1 chief K B ρ)

Equations

• Q2Presentation.Induction.instEdgeZ1FintypeGammaA chief K B ρ = Fintype.ofFinite ↥(Q2Presentation.Induction.edgeZ1 chief K B ρ)

noncomputable instance Q2Presentation.Induction.instEdgeZ1FintypeGQ2 {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (B : BoundaryPackage GQ2Profinite) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : Fintype ↥(edgeZ1 chief K B ρ)

Equations

• Q2Presentation.Induction.instEdgeZ1FintypeGQ2 chief K B ρ = Fintype.ofFinite ↥(Q2Presentation.Induction.edgeZ1 chief K B ρ)

The torsor trivialization of V⋊C-lifts at a multiplicative

section (at a pinned bundle: the basepoint P.s ∘ ρ̄)

def Q2Presentation.Induction.btLiftHom {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) : Type

The V⋊C-lifts of a lower map ρ: framed continuous homs into B/T' over ρ̄ (through btProj; the frame clause is the house q_Y = β-condition — surjectivity NOT imposed, lem:affinelifting's weak coordinates).

Equations

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

def Q2Presentation.Induction.btLiftVal {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (F : btLiftHom chief K B ρ) (γ : ↑Γ.toProfinite.toTop) : (btChild chief K).fst.Y

Carrier readout of a V⋊C-lift, at the child spelling (the banked childMk fix-class: only a DEF with the raw-typed signature keeps HMul homogeneous — ascriptions are impotent for instance search).

Equations

• Q2Presentation.Induction.btLiftVal chief K B ρ F γ = (ProfiniteGrp.Hom.hom ↑F) γ

theorem Q2Presentation.Induction.btLiftVal_proj {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (F : btLiftHom chief K B ρ) (γ : ↑Γ.toProfinite.toTop) : (btProj chief K) (btLiftVal chief K B ρ F γ) = lowerBar chief K B ρ γ

theorem Q2Presentation.Induction.btLiftVal_mul {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (F : btLiftHom chief K B ρ) (γ γ' : ↑Γ.toProfinite.toTop) : btLiftVal chief K B ρ F (γ * γ') = btLiftVal chief K B ρ F γ * btLiftVal chief K B ρ F γ'

theorem Q2Presentation.Induction.btLift_base_qYMap {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (s : towerC K → (btChild chief K).fst.Y) (hsec : ∀ (c : towerC K), (btProj chief K) (s c) = c) (γ : ↑Γ.toProfinite.toTop) : (btChild chief K).fst.qYMap (s (lowerBar chief K B ρ γ)) = (ProfiniteGrp.Hom.hom p.snd.beta) ((ProfiniteGrp.Hom.hom B.toBoundary) γ)

Any section-composite s ∘ ρ̄ satisfies the frame clause (the qYMap/beta-transport across btToC).

def Q2Presentation.Induction.edgeTrivial {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (s : towerC K → (btChild chief K).fst.Y) (hsec : ∀ (c : towerC K), (btProj chief K) (s c) = c) (hmul : ∀ (c d : towerC K), s c * s d = s (c * d)) (z : ↥(edgeZ1 chief K B ρ)) : btLiftHom chief K B ρ

The trivialization map: a twisted cocycle z yields the V⋊C-lift γ ↦ vInG(z γ)·s(ρ̄ γ) (vInG_conj is exactly what makes this multiplicative — the design's stated dependency).

Equations

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

@[simp]

theorem Q2Presentation.Induction.edgeTrivial_apply {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (s : towerC K → (btChild chief K).fst.Y) (hsec : ∀ (c : towerC K), (btProj chief K) (s c) = c) (hmul : ∀ (c d : towerC K), s c * s d = s (c * d)) (z : ↥(edgeZ1 chief K B ρ)) (γ : ↑Γ.toProfinite.toTop) : (ProfiniteGrp.Hom.hom ↑(edgeTrivial chief K B ρ s hsec hmul z)) γ = vInG chief K (↑z γ) * s (lowerBar chief K B ρ γ)

theorem Q2Presentation.Induction.edgeTrivial_injective {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (s : towerC K → (btChild chief K).fst.Y) (hsec : ∀ (c : towerC K), (btProj chief K) (s c) = c) (hmul : ∀ (c d : towerC K), s c * s d = s (c * d)) : Function.Injective (edgeTrivial chief K B ρ s hsec hmul)

theorem Q2Presentation.Induction.edgeTrivial_surjective {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (s : towerC K → (btChild chief K).fst.Y) (hsec : ∀ (c : towerC K), (btProj chief K) (s c) = c) (hmul : ∀ (c d : towerC K), s c * s d = s (c * d)) : Function.Surjective (edgeTrivial chief K B ρ s hsec hmul)

noncomputable def Q2Presentation.Induction.edgeZ1EquivBtLift {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (s : towerC K → (btChild chief K).fst.Y) (hsec : ∀ (c : towerC K), (btProj chief K) (s c) = c) (hmul : ∀ (c d : towerC K), s c * s d = s (c * d)) : ↥(edgeZ1 chief K B ρ) ≃ btLiftHom chief K B ρ

The torsor trivialization at a multiplicative section: Z¹_ρ(V) ≃ {V⋊C-lifts of ρ} (lem:affinelifting's stage-2 carrier identification, both sources at once).

Equations

• Q2Presentation.Induction.edgeZ1EquivBtLift chief K B ρ s hsec hmul = Equiv.ofBijective (Q2Presentation.Induction.edgeTrivial chief K B ρ s hsec hmul) ⋯

noncomputable def Q2Presentation.Induction.edgeZ1EquivBtLift_pinned {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (ρ : boundaryFramedSurj B (cChild chief K).fst (cChild chief K).snd) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (Z : ZeroEdgeDescentData chief K lam hinv) (P : ZeroEdgePinning chief K lam hinv Z) : ↥(edgeZ1 chief K B ρ) ≃ btLiftHom chief K B ρ

The trivialization at the pinned basepoint P.s ∘ ρ̄ — the design's stated instance: a pinned bundle's multiplicative Csec-section trivializes the V⋊C-lift torsor over every lower map.

Equations

• Q2Presentation.Induction.edgeZ1EquivBtLift_pinned chief K B ρ lam hinv Z P = Q2Presentation.Induction.edgeZ1EquivBtLift chief K B ρ P.s ⋯ ⋯

The T′-stage pullback square

B_λ ≃* xrChild ×_{B/T′} descTarget (from W ⊕ relN = T̃)

def Q2Presentation.Induction.descProjHom {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) : ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (descTarget chief K lam hinv D hW).Y)

The descent projection as a hom of finite discrete profinite groups (the scalarCoverProjHom idiom).

Equations

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

@[simp]

theorem Q2Presentation.Induction.descProjHom_apply {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (b : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) : (ProfiniteGrp.Hom.hom (descProjHom chief K lam hinv D hW)) b = (descProj chief K lam hinv D hW) b

theorem Q2Presentation.Induction.descProj_surjective {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) : Function.Surjective ⇑(descProj chief K lam hinv D hW)

theorem Q2Presentation.Induction.descTarget_qYMap_descProj {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (b : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) : (descTarget chief K lam hinv D hW).qYMap ((descProj chief K lam hinv D hW) b) = (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).qYMap b

Frame transport down the left leg: the q_Y-data of the descended target computes on W-classes (both quotient*_mk transports are definitional).

theorem Q2Presentation.Induction.descToBt_descProj {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) (b : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) : (descToBt chief K lam hinv D hW hne) ((descProj chief K lam hinv D hW) b) = (QuotientGroup.mk' (tChild chief K)) ((Lifting.scalarCoverProj (xrKernel chief K) lam hinv) b)

The square commutes: descToBt ∘ descProj = mk_{T′} ∘ p_λ — the deck collapse of a W-class is the T′-class of its cover projection (three Noether-III Aux_mk_mk computations).

theorem Q2Presentation.Induction.scalarCoverProj_eq_one_iff {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (z : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) : (Lifting.scalarCoverProj (xrKernel chief K) lam hinv) z = 1 ↔ z ∈ (Lifting.scalarRelKernel (xrKernel chief K) lam hinv).N

The kernel of the cover projection is the deck kernel (elementwise spelling of ker_scalarCoverProj).

theorem Q2Presentation.Induction.exists_mem_W_scalarCoverProj {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (D : EdgeComplement chief K lam hinv) (hne : lam ≠ 0) (t : (XRZero.xrChild chief K).fst.Y) (ht : t ∈ tChild chief K) : ∃ w ∈ D.W, (Lifting.scalarCoverProj (xrKernel chief K) lam hinv) w = t

W covers T′ (from W ⊕ relN = T̃ and p_λ(relN) = 1): every T′-element is the cover projection of a complement element.

theorem Q2Presentation.Induction.descPair_injective {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) {b b' : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y} (hsc : (Lifting.scalarCoverProj (xrKernel chief K) lam hinv) b = (Lifting.scalarCoverProj (xrKernel chief K) lam hinv) b') (hdp : (descProj chief K lam hinv D hW) b = (descProj chief K lam hinv D hW) b') : b = b'

Monicity of the pair (p_λ, descProj) (from W ⊓ relN = ⊥).

theorem Q2Presentation.Induction.descPair_exists {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) (x : (XRZero.xrChild chief K).fst.Y) (d : (descTarget chief K lam hinv D hW).Y) (h : (QuotientGroup.mk' (tChild chief K)) x = (descToBt chief K lam hinv D hW hne) d) : ∃ (b : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y), (Lifting.scalarCoverProj (xrKernel chief K) lam hinv) b = x ∧ (descProj chief K lam hinv D hW) b = d

Effectivity of the pair: every square-compatible pair of points (x, d) comes from a cover point (existence half of the pullback).

def Q2Presentation.Induction.descPullInv {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (q : (XRZero.xrChild chief K).fst.Y × (descTarget chief K lam hinv D hW).Y) : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y

The choice-packaged inverse of the pair (p_λ, descProj) (total function; 1 off the square locus).

Equations

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

theorem Q2Presentation.Induction.descPullInv_def {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (q : (XRZero.xrChild chief K).fst.Y × (descTarget chief K lam hinv D hW).Y) : descPullInv chief K lam hinv D hW q = if h : ∃ (b : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y), (Lifting.scalarCoverProj (xrKernel chief K) lam hinv) b = q.1 ∧ (descProj chief K lam hinv D hW) b = q.2 then h.choose else 1

The classical-dite def-form of descPullInv (the sGammaZ_def fix-class: cite this form, never re-haveI a Decidable instance).

theorem Q2Presentation.Induction.descPullInv_spec {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (q : (XRZero.xrChild chief K).fst.Y × (descTarget chief K lam hinv D hW).Y) (hq : ∃ (b : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y), (Lifting.scalarCoverProj (xrKernel chief K) lam hinv) b = q.1 ∧ (descProj chief K lam hinv D hW) b = q.2) : (Lifting.scalarCoverProj (xrKernel chief K) lam hinv) (descPullInv chief K lam hinv D hW q) = q.1 ∧ (descProj chief K lam hinv D hW) (descPullInv chief K lam hinv D hW q) = q.2

theorem Q2Presentation.Induction.descPullInv_unique {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) (q : (XRZero.xrChild chief K).fst.Y × (descTarget chief K lam hinv D hW).Y) {b : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y} (hb1 : (Lifting.scalarCoverProj (xrKernel chief K) lam hinv) b = q.1) (hb2 : (descProj chief K lam hinv D hW) b = q.2) : descPullInv chief K lam hinv D hW q = b

def Q2Presentation.Induction.descPullback {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) : Subgroup ((XRZero.xrChild chief K).fst.Y × (descTarget chief K lam hinv D hW).Y)

The pullback locus xrChild ×_{B/T′} descTarget, as a subgroup of the product (the equalizer of mk_{T′} ∘ fst and descToBt ∘ snd).

Equations

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

theorem Q2Presentation.Induction.mem_descPullback {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) (q : (XRZero.xrChild chief K).fst.Y × (descTarget chief K lam hinv D hW).Y) : q ∈ descPullback chief K lam hinv D hW hne ↔ (QuotientGroup.mk' (tChild chief K)) q.1 = (descToBt chief K lam hinv D hW hne) q.2

def Q2Presentation.Induction.descProjPair {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y →* (XRZero.xrChild chief K).fst.Y × (descTarget chief K lam hinv D hW).Y

The pair hom (p_λ, descProj), spelled at the child carrier.

Equations

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

theorem Q2Presentation.Induction.descProjPair_mem {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) (b : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y) : (descProjPair chief K lam hinv D hW) b ∈ descPullback chief K lam hinv D hW hne

noncomputable def Q2Presentation.Induction.descPullbackEquiv {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) : (Lifting.scalarCoverTarget (xrKernel chief K) lam hinv).Y ≃* ↥(descPullback chief K lam hinv D hW hne)

The T′-stage pullback square (design §4-N1): the scalar cover IS the fibre product xrChild ×_{B/T′} descTarget — group isomorphism from the W ⊕ relN = T̃ decomposition.

Equations

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

Stage 1: λ-liftability descends to the double cover

def Q2Presentation.Induction.descLiftableWeak {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (f : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N B (XRZero.xrChild chief K).snd) : Prop

descTarget-liftability of f mod T′: a weak framed lift of the reduced map through the descended central double cover — the T′-stage of the lem:affinelifting fibration (frame clause in the house q_Y = β spelling; surjectivity NOT imposed).

Equations

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

theorem Q2Presentation.Induction.coverLiftableWeak_iff_descLiftableWeak {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (lam : Module.Dual (ZMod 2) (Lifting.NAdd (xrKernel chief K))) (hinv : lam ∈ Lifting.conjInvDuals (xrKernel chief K)) (D : EdgeComplement chief K lam hinv) (hW : D.W.Normal) (hne : lam ≠ 0) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (f : TorsorProgram.coverLiftTotal (XRZero.xrChild chief K).fst (mChildKernel chief K).N B (XRZero.xrChild chief K).snd) : coverLiftableWeak chief K lam hinv B f ↔ descLiftableWeak chief K lam hinv D hW hne B f

The stage-1 equivalence (design §4-N1, both sources at once): a weak M-lift is λ-liftable iff its T′-reduction lifts through descToBt — forward by composing with descProj (square commutation

• frame transport), backward through the pullback inverse.