def Q2Presentation.Lifting.liftMarking {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) (B : BoundaryPackage GammaA) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f : TorsorProgram.liftHom Yt E.N ⋯ ⋯ B F g) : Marking Yt.Y

The generator marking of a framed lift.

Equations

• Q2Presentation.Lifting.liftMarking E B F g f a = (ProfiniteGrp.Hom.hom ↑f) (Q2Presentation.gammaGen a)

theorem Q2Presentation.Lifting.liftDiff_mem {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) (B : BoundaryPackage GammaA) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f₀ f₁ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ B F g) (a : Gen) : ((ProfiniteGrp.Hom.hom ↑f₀) (gammaGen a))⁻¹ * (ProfiniteGrp.Hom.hom ↑f₁) (gammaGen a) ∈ E.N

Two lifts of the same child differ by kernel elements at each generator.

def Q2Presentation.Lifting.liftDiff {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) (B : BoundaryPackage GammaA) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f₀ f₁ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ B F g) : Gen → ↥E.N

The kernel-valued difference tuple of two lifts.

Equations

• Q2Presentation.Lifting.liftDiff E B F g f₀ f₁ a = ⟨((ProfiniteGrp.Hom.hom ↑f₀) (Q2Presentation.gammaGen a))⁻¹ * (ProfiniteGrp.Hom.hom ↑f₁) (Q2Presentation.gammaGen a), ⋯⟩

theorem Q2Presentation.Lifting.liftMarking_perturb {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) (B : BoundaryPackage GammaA) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f₀ f₁ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ B F g) : liftMarking E B F g f₁ = perturb E (liftMarking E B F g f₀) (liftDiff E B F g f₀ f₁)

The second lift's marking is the first's, perturbed by the difference.

theorem Q2Presentation.Lifting.liftMarking_relator_eval {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) (B : BoundaryPackage GammaA) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f : TorsorProgram.liftHom Yt E.N ⋯ ⋯ B F g) (w : GExpr) (hw : ∀ (A : AdmissibleIndex), (w.eval fun (a : Gen) => (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π admissibleDiagram A)) (gammaGen a)) = 1) : w.eval (liftMarking E B F g f) = 1

Relators die at any lift's marking.

theorem Q2Presentation.Lifting.liftDiff_rows {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) (B : BoundaryPackage GammaA) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f₀ f₁ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ B F g) : foxShadow E (liftMarking E B F g f₀) (fun (a : Gen) => Additive.ofMul (liftDiff E B F g f₀ f₁ a)) Q2Word.tameRelator = 0 ∧ foxShadow E (liftMarking E B F g f₀) (fun (a : Gen) => Additive.ofMul (liftDiff E B F g f₀ f₁ a)) Q2Word.wildRelator = 0

The difference rows (N1): the difference tuple of two framed lifts satisfies both relator rows of the word complex.