theorem Q2Presentation.Lifting.conjEndN_mul_mem {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (y s : Yt.Y) (hs : s ∈ E.N) : conjEndN E (y * s) = conjEndN E y

Kernel conjugations are invisible to the shadow operators.

theorem Q2Presentation.Lifting.foxShadow_perturb_eq {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (q : Marking Yt.Y) (n : Gen → ↥E.N) (m : Gen → NAdd E) (w : GExpr) : foxShadow E (perturb E q n) m w = foxShadow E q m w

Row invariance under kernel perturbation: shadows at a perturbed marking agree with shadows at the base.

theorem Q2Presentation.Lifting.rowMap_perturb_eq {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (q : Marking Yt.Y) (n : Gen → ↥E.N) : rowMap E (perturb E q n) = rowMap E q

The row map only depends on the marking through its kernel cosets.

theorem Q2Presentation.Lifting.compat_eq_perturb {Yt : BoundaryFramedTarget} [Finite Yt.Y] (E : ElementaryKernel Yt) (q q' : Marking Yt.Y) (h : ∀ (a : Gen), (QuotientGroup.mk' E.N) (q a) = (QuotientGroup.mk' E.N) (q' a)) : ∃ (n : Gen → ↥E.N), q' = perturb E q n

Two kernel-compatible markings differ by a kernel perturbation.

noncomputable def Q2Presentation.Lifting.baseMarking {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) (F : BoundaryFrame Yt) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) : Marking Yt.Y

A chosen base marking under g.

Equations

• Q2Presentation.Lifting.baseMarking E F g a = Classical.choose ⋯

theorem Q2Presentation.Lifting.baseMarking_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)) (a : Gen) : (QuotientGroup.mk' E.N) (baseMarking E F g a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a)

theorem Q2Presentation.Lifting.frame_of_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)) (q : Marking Yt.Y) (hq : ∀ (a : Gen), (QuotientGroup.mk' E.N) (q a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a)) (a : Gen) : Yt.qYMap (q a) = (ProfiniteGrp.Hom.hom F.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))

Kernel-compatible markings frame exactly.

theorem Q2Presentation.Lifting.defect_mem_of_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)) (q : Marking Yt.Y) (hq : ∀ (a : Gen), (QuotientGroup.mk' E.N) (q a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a)) (w : GExpr) (hw1 : (w.eval fun (a : Gen) => (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a)) = 1) : w.eval q ∈ E.N

Relator defects of kernel-compatible markings lie in the kernel.

theorem Q2Presentation.Lifting.defect_tame_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)) : Q2Word.tameRelator.eval q ∈ E.N

theorem Q2Presentation.Lifting.defect_wild_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)) : Q2Word.wildRelator.eval q ∈ E.N

noncomputable def Q2Presentation.Lifting.defectPair {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)) : NAdd E × NAdd E

The relator-defect pair of a compatible marking.

Equations

• Q2Presentation.Lifting.defectPair E F g q hq = (Additive.ofMul ⟨Q2Presentation.Q2Word.tameRelator.eval q, ⋯⟩, Additive.ofMul ⟨Q2Presentation.Q2Word.wildRelator.eval q, ⋯⟩)

theorem Q2Presentation.Lifting.defectPair_perturb {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)) (n : Gen → ↥E.N) (hq' : ∀ (a : Gen), (QuotientGroup.mk' E.N) (perturb E q n a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a)) : defectPair E F g (perturb E q n) hq' = defectPair E F g q hq + (rowMap E q) fun (a : Gen) => Additive.ofMul (n a)

Perturbation shifts the defect pair by a row value.

def Q2Presentation.Lifting.obstructionSpace {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)) : Type

The obstruction space of g: the row-map cokernel at the base marking.

Equations

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

instance Q2Presentation.Lifting.instAddCommGroupObstructionSpace {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)) : AddCommGroup (obstructionSpace E F g)

Equations

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

instance Q2Presentation.Lifting.instModuleZModOfNatNatObstructionSpace {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)) : Module (ZMod 2) (obstructionSpace E F g)

Equations

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

noncomputable def Q2Presentation.Lifting.obstructionClass {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)) : obstructionSpace E F g

The obstruction class of g.

Equations

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

theorem Q2Presentation.Lifting.obstructionClass_eq_zero_iff {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)) : obstructionClass E F g = 0 ↔ Nonempty (TorsorProgram.liftHom Yt E.N ⋯ ⋯ boundaryPackage_GammaA F g)

The obstruction detects lift existence.