Marking freedom for the obstruction class

theorem Q2Presentation.Lifting.obstructionClass_eq_zero_iff_defect_mem {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (F : BoundaryFrame Yt) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (q : Marking Yt.Y) (hq : ∀ (a : Gen), (QuotientGroup.mk' E.N) (q a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a)) : obstructionClass E F g = 0 ↔ defectPair E F g q hq ∈ (rowMap E (baseMarking E F g)).range

Generic engine addendum: the obstruction class vanishes iff the defect of ANY compatible marking lies in the base row image (the row map only sees kernel cosets, so the defect shifts by a row value under perturbation).

Diagonal rows at the relative kernel

theorem Q2Presentation.Lifting.rowMap_scalarRelKernel_apply {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (hne : lam ≠ 0) (q' : Marking (scalarCoverTarget E lam hinv).Y) (n : Gen → NAdd (scalarRelKernel E lam hinv)) : (rowMap (scalarRelKernel E lam hinv) q') n = (n Gen.tau, n Gen.tau)

Diagonal rows at the relative kernel (trivial Jacobian (b,b), prop:defduality l.1935–1939, relative form), at EVERY marking: the card-2 kernel makes every functional conjugation-invariant, so both relator rows collapse to the τ-slot.

theorem Q2Presentation.Lifting.mem_range_rowMap_scalarRelKernel_iff {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (hne : lam ≠ 0) (q' : Marking (scalarCoverTarget E lam hinv).Y) (x : NAdd (scalarRelKernel E lam hinv) × NAdd (scalarRelKernel E lam hinv)) : x ∈ (rowMap (scalarRelKernel E lam hinv) q').range ↔ x.1 = x.2

The relative row image is the diagonal.

The projected base marking and its defect

def Q2Presentation.Lifting.scalarCoverMarking {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (F : BoundaryFrame Yt) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) : Marking (scalarCoverTarget E lam hinv).Y

The projected parent base marking (spelled as an application, not a composition, to match GExpr.eval_map).

Equations

• Q2Presentation.Lifting.scalarCoverMarking E F g lam hinv a = (Q2Presentation.Lifting.scalarProj E lam hinv) (Q2Presentation.Lifting.baseMarking E F g a)

theorem Q2Presentation.Lifting.scalarCoverMarking_lift {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (F : BoundaryFrame Yt) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (a : Gen) : (QuotientGroup.mk' (scalarRelKernel E lam hinv).N) (scalarCoverMarking E F g lam hinv a) = (ProfiniteGrp.Hom.hom (↑(scalarCoverChild E lam hinv boundaryPackage_GammaA F g)).hom) (gammaGen a)

The projected base marking is compatible with the transported child.

theorem Q2Presentation.Lifting.defectPair_scalarCover {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (F : BoundaryFrame Yt) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) : defectPair (scalarRelKernel E lam hinv) (scalarCoverFrame E lam hinv F) (scalarCoverChild E lam hinv boundaryPackage_GammaA F g) (scalarCoverMarking E F g lam hinv) ⋯ = ((scalarRelProj E lam hinv) (defectPair E F g (baseMarking E F g) ⋯).1, (scalarRelProj E lam hinv) (defectPair E F g (baseMarking E F g) ⋯).2)

The relative defect is the mkN-image of the parent defect (GExpr.eval_map at the scalar projection; the ω₂-power case is map_powOmega2, unconditional).

P1-A, generic core

theorem Q2Presentation.Lifting.scalar_defect_eq_zero_iff_coverLift {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (F : BoundaryFrame Yt) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (hne : lam ≠ 0) : lam ((defectPair E F g (baseMarking E F g) ⋯).1 + (defectPair E F g (baseMarking E F g) ⋯).2) = 0 ↔ Nonempty (scalarCoverLiftHom E lam hinv boundaryPackage_GammaA F g)

P1-A, generic core (lem:obstructionseparation l.4219–4223, candidate half): the λ-pairing of the defect sum vanishes iff g lifts through B_λ. hR-free, diamond-free: the engine at the cover parent with the relative kernel, plus the diagonal row image and ker mkN = ker λ.

Optional P2 prep: the candidate cover-lift torsor size

def Q2Presentation.Lifting.tauVanishEquiv (V : Type) [Zero V] : { n : Gen → V // n Gen.tau = 0 } ≃ V × V × V

Splitting a τ-vanishing generator tuple into its three off-τ coordinates.

Equations

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

theorem Q2Presentation.Lifting.scalarCover_Z1_card {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (F : BoundaryFrame Yt) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (lam : Module.Dual (ZMod 2) (NAdd E)) (hinv : lam ∈ conjInvDuals E) (hne : lam ≠ 0) (f₀ : scalarCoverLiftHom E lam hinv boundaryPackage_GammaA F g) : Nat.card (TorsorProgram.Z1 (scalarCoverTarget E lam hinv) (scalarRelKernel E lam hinv).N ⋯ ⋯ boundaryPackage_GammaA (scalarCoverFrame E lam hinv F) (scalarCoverChild E lam hinv boundaryPackage_GammaA F g) f₀) = 8

Optional P2 prep (lem:commonscalars l.3791–3815, candidate half): the cover-lift torsor has size |Hom(Γ_A, 𝔽₂)| = 8 — the row-map kernel at the diagonal rows is the τ-vanishing tuple space (R/ker λ)³.