def Q2Presentation.Lifting.anyImage {Yt : BoundaryFramedTarget} (q' : Marking Yt.Y) : Subgroup Yt.Y

The image subgroup of a marking.

Equations

• Q2Presentation.Lifting.anyImage q' = Subgroup.closure (Set.range q')

def Q2Presentation.Lifting.anyMarking {Yt : BoundaryFramedTarget} (q' : Marking Yt.Y) : Marking ↥(anyImage q')

The corestricted marking of the image.

Equations

• Q2Presentation.Lifting.anyMarking q' a = ⟨q' a, ⋯⟩

theorem Q2Presentation.Lifting.anyMarking_generates {Yt : BoundaryFramedTarget} (q' : Marking Yt.Y) : Subgroup.closure (Set.range (anyMarking q')) = ⊤

theorem Q2Presentation.Lifting.anyMarking_relator {Yt : BoundaryFramedTarget} (q' : Marking Yt.Y) (w : GExpr) (hw : w.eval q' = 1) : w.eval (anyMarking q') = 1

theorem Q2Presentation.Lifting.anyMarking_mem_twoCore {Yt : BoundaryFramedTarget} (q' : Marking Yt.Y) (a : Gen) (hLY : q' a ∈ Yt.LY) : anyMarking q' a ∈ twoCore ↥(anyImage q')

theorem Q2Presentation.Lifting.anyMarking_admissible {Yt : BoundaryFramedTarget} (q' : Marking Yt.Y) (htame : Q2Word.tameRelator.eval q' = 1) (hwild : Q2Word.wildRelator.eval q' = 1) (hx0 : q' Gen.x0 ∈ Yt.LY) (hx1 : q' Gen.x1 ∈ Yt.LY) : Admissible (anyMarking q')

def Q2Presentation.Lifting.anyHom {Yt : BoundaryFramedTarget} (q' : Marking Yt.Y) (hadm : Admissible (anyMarking q')) : GammaA ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of Yt.Y)

The hom from an admissible marking: epi onto the image, included.

Equations

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

theorem Q2Presentation.Lifting.anyHom_gammaGen {Yt : BoundaryFramedTarget} (q' : Marking Yt.Y) (hadm : Admissible (anyMarking q')) (a : Gen) : (ProfiniteGrp.Hom.hom (anyHom q' hadm)) (gammaGen a) = q' a

def Q2Presentation.Lifting.liftHom_of_marking {Yt : BoundaryFramedTarget} (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) (htame : Q2Word.tameRelator.eval q' = 1) (hwild : Q2Word.wildRelator.eval q' = 1) (hlift : ∀ (a : Gen), (QuotientGroup.mk' E.N) (q' a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a)) (hframe : ∀ (a : Gen), Yt.qYMap (q' a) = (ProfiniteGrp.Hom.hom F.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))) (hx0 : q' Gen.x0 ∈ Yt.LY) (hx1 : q' Gen.x1 ∈ Yt.LY) : TorsorProgram.liftHom Yt E.N ⋯ ⋯ boundaryPackage_GammaA F g

Lifts from markings: any marking with the four lift properties is the generator marking of a framed lift.

Equations

• Q2Presentation.Lifting.liftHom_of_marking E F g q' htame hwild hlift hframe hx0 hx1 = ⟨Q2Presentation.Lifting.anyHom q' ⋯, ⋯⟩

Existence of a base lift

theorem Q2Presentation.Lifting.liftHom_nonempty_of_rowMap_surjective {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) (F : BoundaryFrame Yt) (g : boundaryFramedSurj boundaryPackage_GammaA (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (hsurj : ∀ (qh : Marking Yt.Y), (∀ (a : Gen), (QuotientGroup.mk' E.N) (qh a) = (ProfiniteGrp.Hom.hom (↑g).hom) (gammaGen a)) → (∀ (a : Gen), Yt.qYMap (qh a) = (ProfiniteGrp.Hom.hom F.beta) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.toBoundary) (gammaGen a))) → Function.Surjective ⇑(rowMap E qh)) : Nonempty (TorsorProgram.liftHom Yt E.N ⋯ ⋯ boundaryPackage_GammaA F g)

Existence (the obstruction argument): if the row map is surjective at every marking over g, then g admits a framed lift. Preimages of the child's generator values frame exactly (through the quotient mk-lemmas); the two relator defects lie in N and are killed by a row-map preimage.