Uniform word evaluation (GExpr) — Stage A

A tiny abstract-syntax tree GExpr for words in the four marked generators (with ℕ-powers and the profinite ω₂-power), together with its evaluation GExpr.eval into a finite group under a Marking G = Gen → G.

The single load-bearing lemma is GExpr.eval_map: evaluation commutes with group homomorphisms between finite groups. The only non-formal ingredient is the powOmega2 case, which is exactly Q2Presentation.map_powOmega2 (proved in Omega2). Its finite-product corollary GExpr.eval_pi says evaluation commutes with the projections of a finite product ∀ i, G i; this is what the subdirect construction in Stage B (admissible_subdirect) uses.

The design point (plan §2): all sophistication lives in eval_map / map_powOmega2; the displayed Q₂ words (in Q2Words.lean) are boring data.

@[reducible, inline]

abbrev Q2Presentation.Marking (G : Type u_1) [Group G] : Type u_1

A marking assigns a group element to each of the four generators.

Equations

• Q2Presentation.Marking G = (Q2Presentation.Gen → G)

def Q2Presentation.instReprGen.repr : Gen → ℕ → Std.Format

Equations

• Q2Presentation.instReprGen.repr Q2Presentation.Gen.sigma prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Q2Presentation.Gen.sigma")).group prec✝
• Q2Presentation.instReprGen.repr Q2Presentation.Gen.tau prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Q2Presentation.Gen.tau")).group prec✝
• Q2Presentation.instReprGen.repr Q2Presentation.Gen.x0 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Q2Presentation.Gen.x0")).group prec✝
• Q2Presentation.instReprGen.repr Q2Presentation.Gen.x1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Q2Presentation.Gen.x1")).group prec✝

instance Q2Presentation.instReprGen : Repr Gen

Equations

• Q2Presentation.instReprGen = { reprPrec := Q2Presentation.instReprGen.repr }

inductive Q2Presentation.GExpr : Type

Abstract syntax for words in the generators: the identity, a generator, products, inverses, ℕ-powers, and the profinite ω₂-power.

• one : GExpr
• gen : Gen → GExpr
• mul : GExpr → GExpr → GExpr
• inv : GExpr → GExpr
• powNat : GExpr → ℕ → GExpr
• powOmega2 : GExpr → GExpr

def Q2Presentation.instReprGExpr.repr : GExpr → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Q2Presentation.instReprGExpr.repr Q2Presentation.GExpr.one prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Q2Presentation.GExpr.one")).group prec✝

instance Q2Presentation.instReprGExpr : Repr GExpr

Equations

• Q2Presentation.instReprGExpr = { reprPrec := Q2Presentation.instReprGExpr.repr }

noncomputable def Q2Presentation.GExpr.eval {G : Type u_1} [Group G] [Finite G] : GExpr → Marking G → G

Evaluate a GExpr in a finite group G under a marking q : Gen → G. The powOmega2 case is the finite ω₂-power Q2Presentation.powOmega2.

Equations

• Q2Presentation.GExpr.one.eval x✝ = 1
• (Q2Presentation.GExpr.gen a).eval x✝ = x✝ a
• (u.mul v).eval x✝ = u.eval x✝ * v.eval x✝
• u.inv.eval x✝ = (u.eval x✝)⁻¹
• (u.powNat n).eval x✝ = u.eval x✝ ^ n
• u.powOmega2.eval x✝ = Q2Presentation.powOmega2 (u.eval x✝)

theorem Q2Presentation.GExpr.eval_map {G : Type u_1} {H : Type u_2} [Group G] [Finite G] [Group H] [Finite H] (φ : G →* H) (w : GExpr) (q : Marking G) : φ (w.eval q) = w.eval fun (a : Gen) => φ (q a)

Evaluation commutes with finite-group homomorphisms. Applying φ to the value of a word equals evaluating the word against the φ-pushed marking. This is the uniform mechanism behind quotient/product relation-preservation; the ω₂-power case is map_powOmega2.

theorem Q2Presentation.GExpr.eval_pi {ι : Type u_1} [Finite ι] {G : ι → Type u_2} [(i : ι) → Group (G i)] [∀ (i : ι), Finite (G i)] (w : GExpr) (q : Marking ((i : ι) → G i)) (i : ι) : w.eval q i = w.eval fun (a : Gen) => q a i

Evaluation commutes with the projections of a finite product. Evaluating a word against a marking into ∀ i, G i and then projecting to the i-th factor equals evaluating the projected marking in G i. This is the special case of eval_map for the evaluation homomorphism Pi.evalMonoidHom, and is the form the subdirect-product construction (admissible_subdirect) consumes.