Admissibility is preserved by quotient maps (paper §2, Lemmas 2.1–2.2)

The paper builds the candidate Γ_A as an inverse limit of admissible finite quotients, which requires that admissibility is stable under the maps of the system. The technical heart is that the auxiliary words (which involve ω₂-powers) commute with group homomorphisms — this is exactly GQ2.powOmega2_map. Here we push it through the whole word ledger to obtain:

• GQ2.Marking.map_admissible: an admissible marking of G pushes forward, along any surjective group homomorphism f : G → H (of finite groups), to an admissible marking of H.

def GQ2.Marking.map {G : Type u_1} {H : Type u_2} [Group G] [Group H] (f : G →* H) (t : Marking G) : Marking H

Push a marking forward along a group homomorphism.

Equations

• GQ2.Marking.map f t = { σ := f t.σ, τ := f t.τ, x₀ := f t.x₀, x₁ := f t.x₁ }

@[simp]

theorem GQ2.Marking.map_σ {G : Type u_1} {H : Type u_2} [Group G] [Group H] (f : G →* H) (t : Marking G) : (map f t).σ = f t.σ

@[simp]

theorem GQ2.Marking.map_τ {G : Type u_1} {H : Type u_2} [Group G] [Group H] (f : G →* H) (t : Marking G) : (map f t).τ = f t.τ

@[simp]

theorem GQ2.Marking.map_x₀ {G : Type u_1} {H : Type u_2} [Group G] [Group H] (f : G →* H) (t : Marking G) : (map f t).x₀ = f t.x₀

@[simp]

theorem GQ2.Marking.map_x₁ {G : Type u_1} {H : Type u_2} [Group G] [Group H] (f : G →* H) (t : Marking G) : (map f t).x₁ = f t.x₁

theorem GQ2.Marking.map_conjP {G : Type u_1} {H : Type u_2} [Group G] [Group H] (f : G →* H) (x g : G) : f (conjP x g) = conjP (f x) (f g)

f intertwines the conjugation convention.

theorem GQ2.Marking.map_commP {G : Type u_1} {H : Type u_2} [Group G] [Group H] (f : G →* H) (x y : G) : f (commP x y) = commP (f x) (f y)

f intertwines the commutator convention.

@[simp]

theorem GQ2.Marking.map_sigma2 {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Finite G] (f : G →* H) (t : Marking G) : (map f t).sigma2 = f t.sigma2

@[simp]

theorem GQ2.Marking.map_u0 {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Finite G] (f : G →* H) (t : Marking G) : (map f t).u0 = f t.u0

@[simp]

theorem GQ2.Marking.map_u1 {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Finite G] (f : G →* H) (t : Marking G) : (map f t).u1 = f t.u1

@[simp]

theorem GQ2.Marking.map_d0 {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Finite G] (f : G →* H) (t : Marking G) : (map f t).d0 = f t.d0

@[simp]

theorem GQ2.Marking.map_z0 {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Finite G] (f : G →* H) (t : Marking G) : (map f t).z0 = f t.z0

@[simp]

theorem GQ2.Marking.map_c0 {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Finite G] (f : G →* H) (t : Marking G) : (map f t).c0 = f t.c0

@[simp]

theorem GQ2.Marking.map_g0 {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Finite G] (f : G →* H) (t : Marking G) : (map f t).g0 = f t.g0

@[simp]

theorem GQ2.Marking.map_dg {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Finite G] (f : G →* H) (t : Marking G) : (map f t).dg = f t.dg

@[simp]

theorem GQ2.Marking.map_hc {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Finite G] (f : G →* H) (t : Marking G) : (map f t).hc = f t.hc

@[simp]

theorem GQ2.Marking.map_h0 {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Finite G] (f : G →* H) (t : Marking G) : (map f t).h0 = f t.h0

theorem GQ2.Marking.map_tameRel {G : Type u_1} {H : Type u_2} [Group G] [Group H] (f : G →* H) (t : Marking G) (h : t.TameRel) : (map f t).TameRel

The tame relation transfers along any group hom.

theorem GQ2.Marking.map_wildLHS {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Finite G] (f : G →* H) (t : Marking G) : (map f t).h0 * (map f t).u1⁻¹ * conjP (map f t).x₁ (map f t).σ * (map f t).c0 = f (t.h0 * t.u1⁻¹ * conjP t.x₁ t.σ * t.c0)

The wild relator word commutes with any group hom f.

theorem GQ2.Marking.map_wildRel {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Finite G] (f : G →* H) (t : Marking G) (h : t.WildRel) : (map f t).WildRel

The wild relation transfers along any group hom.

theorem GQ2.Marking.map_admissible {G : Type u_3} {H : Type u_4} [Group G] [Group H] [Finite G] [Finite H] (f : G →* H) (hf : Function.Surjective ⇑f) (t : Marking G) (ht : t.Admissible) : (map f t).Admissible

Admissibility pushes forward along surjective quotient maps (paper §2, cofinality / Lemma 2.1–2.2). If t is an admissible marking of a finite group G and f : G ↠ H is a surjective homomorphism of finite groups, then t.map f is an admissible marking of H.

Paper-tag ledger (auto-generated by paperforge; do not edit)

• Lemma 2.1 = ⟦lem-subdirect⟧