Finite subdirect closure of admissible markings (Stage A) — manuscript Lemma 2.1

Given a finite family of admissible markings q i : Marking (G i), the diagonal marking a ↦ (i ↦ q i a) into the product ∀ i, G i, corestricted to the subgroup it generates (subdirectSubgroup q), is again admissible. This is the formal content of manuscript Lemma 2.1 (and the engine behind the cofinality argument of Lemma 2.2).

The proof decomposes uniformly, exactly as in the plan (§5):

• relations — via GExpr.eval_map (corestrict along the subgroup inclusion) and GExpr.eval_pi (work coordinatewise); the wild word is never unfolded;
• generation — by construction, the corestricted generators generate the closure;
• wild pro-2 condition — the diagonal images of x₀, x₁ lie in the normal 2-subgroup ∏ᵢ O₂(Gᵢ), whose pullback to the subdirect subgroup is a normal 2-subgroup, hence inside O₂ of the subdirect subgroup by maximality (normal_pSubgroup_le_pCore).

def Q2Presentation.diagonalMarking {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → Group (G i)] (q : (i : ι) → Marking (G i)) : Marking ((i : ι) → G i)

The diagonal marking a ↦ (i ↦ q i a) into the product ∀ i, G i.

Equations

• Q2Presentation.diagonalMarking q a i = q i a

def Q2Presentation.subdirectSubgroup {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → Group (G i)] (q : (i : ι) → Marking (G i)) : Subgroup ((i : ι) → G i)

The subdirect subgroup: the subgroup of ∀ i, G i generated by the diagonal generating tuple.

Equations

• Q2Presentation.subdirectSubgroup q = Subgroup.closure (Set.range (Q2Presentation.diagonalMarking q))

def Q2Presentation.diagonalSubdirectMarking {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → Group (G i)] (q : (i : ι) → Marking (G i)) : Marking ↥(subdirectSubgroup q)

The diagonal marking, corestricted to the subdirect subgroup it generates.

Equations

• Q2Presentation.diagonalSubdirectMarking q a = ⟨Q2Presentation.diagonalMarking q a, ⋯⟩

@[simp]

theorem Q2Presentation.coe_diagonalSubdirectMarking {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → Group (G i)] (q : (i : ι) → Marking (G i)) (a : Gen) : ↑(diagonalSubdirectMarking q a) = diagonalMarking q a

theorem Q2Presentation.isPGroup_subgroupPi {ι : Type u_1} [Finite ι] {G : ι → Type u_2} [(i : ι) → Group (G i)] {p : ℕ} {N : (i : ι) → Subgroup (G i)} (h : ∀ (i : ι), IsPGroup p ↥(N i)) : IsPGroup p ↥(Subgroup.pi Set.univ N)

A finite product (as a Subgroup.pi) of p-groups is a p-group.

theorem Q2Presentation.eval_diagonalSubdirectMarking_eq_one {ι : Type u_1} [Finite ι] {G : ι → Type u_2} [(i : ι) → Group (G i)] [∀ (i : ι), Finite (G i)] (q : (i : ι) → Marking (G i)) (w : GExpr) (hw : ∀ (i : ι), w.eval (q i) = 1) : w.eval (diagonalSubdirectMarking q) = 1

Relator preservation under the subdirect construction: if a word evaluates to 1 in every factor, it evaluates to 1 at the subdirect marking. Uniform via GExpr.eval_map (subgroup inclusion) and GExpr.eval_pi (coordinatewise).

theorem Q2Presentation.diagonalSubdirectMarking_mem_twoCore {ι : Type u_1} [Finite ι] {G : ι → Type u_2} [(i : ι) → Group (G i)] [∀ (i : ι), Finite (G i)] (q : (i : ι) → Marking (G i)) (a : Gen) (ha : ∀ (i : ι), q i a ∈ twoCore (G i)) : diagonalSubdirectMarking q a ∈ twoCore ↥(subdirectSubgroup q)

The diagonal image of a generator that lies in every factor's 2-core lands in the 2-core of the subdirect subgroup.

theorem Q2Presentation.admissible_subdirect {ι : Type u_1} [Finite ι] {G : ι → Type u_2} [(i : ι) → Group (G i)] [∀ (i : ι), Finite (G i)] (q : (i : ι) → Marking (G i)) (h : ∀ (i : ι), Admissible (q i)) : Admissible (diagonalSubdirectMarking q)

Finite subdirect closure of admissibility (manuscript Lemma 2.1). If each q i is admissible, then the corestricted diagonal marking into the subdirect subgroup is admissible.