Q2Presentation.Lifting.ExtensionStep

source

theorem Q2Presentation.Lifting.perturb_eval_one {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) (n : Gen → ↥E.N) (w : GExpr) (h1 : w.eval (liftMarking E B F g f₀) = 1) (hsh : foxShadow E (liftMarking E B F g f₀) (fun (a : Gen) => Additive.ofMul (n a)) w = 0) :

w.eval (perturb E (liftMarking E B F g f₀) n) = 1

Perturbed-marking relator death: base death + zero shadow.

source

def Q2Presentation.Lifting.extImage {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) (n : Gen → ↥E.N) :

Subgroup Yt.Y

The image subgroup of the perturbed marking.

Equations

Q2Presentation.Lifting.extImage E B F g f₀ n = Subgroup.closure (Set.range (Q2Presentation.Lifting.perturb E (Q2Presentation.Lifting.liftMarking E B F g f₀) n))

Instances For

source

def Q2Presentation.Lifting.extMarking {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) (n : Gen → ↥E.N) :

Marking ↥(extImage E B F g f₀ n)

The corestricted marking of the image.

Equations

Q2Presentation.Lifting.extMarking E B F g f₀ n a = ⟨Q2Presentation.Lifting.perturb E (Q2Presentation.Lifting.liftMarking E B F g f₀) n a, ⋯⟩

Instances For

source

theorem Q2Presentation.Lifting.extMarking_generates {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) (n : Gen → ↥E.N) :

Subgroup.closure (Set.range (extMarking E B F g f₀ n)) = ⊤

source

theorem Q2Presentation.Lifting.extMarking_relator {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) (n : Gen → ↥E.N) (w : GExpr) (hw : w.eval (perturb E (liftMarking E B F g f₀) n) = 1) :

w.eval (extMarking E B F g f₀ n) = 1

Relators transport into the corestricted marking.

source

theorem Q2Presentation.Lifting.extMarking_mem_twoCore {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) (n : Gen → ↥E.N) (a : Gen) (hLY : perturb E (liftMarking E B F g f₀) n a ∈ Yt.LY) :

extMarking E B F g f₀ n a ∈ twoCore ↥(extImage E B F g f₀ n)

Wild values in L_Y land in the image's 2-core.

source

theorem Q2Presentation.Lifting.extMarking_admissible {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) (n : Gen → ↥E.N) (hrowT : foxShadow E (liftMarking E B F g f₀) (fun (a : Gen) => Additive.ofMul (n a)) Q2Word.tameRelator = 0) (hrowW : foxShadow E (liftMarking E B F g f₀) (fun (a : Gen) => Additive.ofMul (n a)) Q2Word.wildRelator = 0) (hx0 : perturb E (liftMarking E B F g f₀) n Gen.x0 ∈ Yt.LY) (hx1 : perturb E (liftMarking E B F g f₀) n Gen.x1 ∈ Yt.LY) :

Admissible (extMarking E B F g f₀ n)

Admissibility of the perturbed image marking.

source

theorem Q2Presentation.Lifting.homs_ext_on_gen {R : ProfiniteGrp.{0}} [T2Space ↑R.toProfinite.toTop] {f g' : GammaA ⟶ R} (h : ∀ (a : Gen), (ProfiniteGrp.Hom.hom f) (gammaGen a) = (ProfiniteGrp.Hom.hom g') (gammaGen a)) :

f = g'

Generic density extensionality for homs out of Γ_A into a Hausdorff profinite target.

source

def Q2Presentation.Lifting.qYHom {Yt : BoundaryFramedTarget} :

ProfiniteGrp.ofFiniteGrp (FiniteGrp.of Yt.Y) ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Yt.H × Multiplicative Yt.E))

The framing pair q_Y = (π_Y, θ_Y) as a bundled hom.

Equations

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

Instances For

source

def Q2Presentation.Lifting.extHom {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) (n : Gen → ↥E.N) (hadm : Admissible (extMarking E B F g f₀ n)) :

GammaA ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of Yt.Y)

The extended hom: epi onto the image, included into Y.

Equations

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

Instances For

source

theorem Q2Presentation.Lifting.extHom_gammaGen {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) (n : Gen → ↥E.N) (hadm : Admissible (extMarking E B F g f₀ n)) (a : Gen) :

(ProfiniteGrp.Hom.hom (extHom E B F g f₀ n hadm)) (gammaGen a) = perturb E (liftMarking E B F g f₀) n a

The extended hom takes the perturbed values on the generators.

source

def Q2Presentation.Lifting.extLift {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) (n : Gen → ↥E.N) (hadm : Admissible (extMarking E B F g f₀ n)) :

TorsorProgram.liftHom Yt E.N ⋯ ⋯ B F g

The extension step (N2): a row-satisfying kernel perturbation of a framed lift is again a framed lift, with the perturbed generator values.

Equations

Q2Presentation.Lifting.extLift E B F g f₀ n hadm = ⟨Q2Presentation.Lifting.extHom E B F g f₀ n hadm, ⋯⟩

Instances For

source

theorem Q2Presentation.Lifting.extLift_marking {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) (n : Gen → ↥E.N) (hadm : Admissible (extMarking E B F g f₀ n)) :

liftMarking E B F g (extLift E B F g f₀ n hadm) = perturb E (liftMarking E B F g f₀) n

The extended lift's generator values.

source

theorem Q2Presentation.Lifting.liftMarking_mem_LY_of_tame_one {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) (a : Gen) (htame : (ProfiniteGrp.Hom.hom B.tameMap) (gammaGen a) = 1) :

liftMarking E B F g f a ∈ Yt.LY

A generator with trivial tame image lifts into the wild part L_Y.

source

theorem Q2Presentation.Lifting.liftHom_ext {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) (h : liftMarking E B F g f₁ = liftMarking E B F g f₂) :

f₁ = f₂

Lifts are determined by their generator markings (density).