ReidemeisterSchreier.Discrete.OpenSubgroups.Words.NielsenSchreierCompat
This module develops the rewriting and basis constructions behind the subgroup calculations. It tracks words and relations through the chosen transversal to obtain the required presentation or basis statements.
noncomputable def FreeGroupBasis.actionGroupoidIsFree
{ι G A : Type u} [Group G] [MulAction G A] (b : FreeGroupBasis ι G) :
IsFreeGroupoid (ActionCategory G A) where
quiverGenerators :=
⟨fun a b' => { i : ι // b i • a.back = b'.back }⟩
of := fun (e : Subtype _) => ⟨b e, e.property⟩
unique_lift := by
intro X _ f
let f' : ι → (A → X) ⋊[mulAutArrow] G := fun i =>
⟨fun a =>
@f ⟨(), (b i)⁻¹ • a⟩ ⟨(), a⟩
⟨i, smul_inv_smul (b i) a⟩,
b i⟩
let F' : G →* (A → X) ⋊[mulAutArrow] G := b.lift f'
have hF' : ∀ i, F' (b i) = f' i := congrFun (b.lift.left_inv f')
refine ⟨uncurry F' ?_, ?_, ?_⟩
· intro g
suffices SemidirectProduct.rightHom.comp F' = MonoidHom.id G by
exact DFunLike.ext_iff.mp this g
apply b.ext_hom
intro i
rw [MonoidHom.comp_apply, hF' i]
rfl
· rintro ⟨⟨⟩, a : A⟩ ⟨⟨⟩, b'⟩ ⟨i, h : b i • a = b'⟩
change (F' (b i)).left _ = _
rw [hF' i]
cases inv_smul_eq_iff.mpr h.symm
rfl
· intro E hE
have hcurried : curry E = F' := by
apply b.ext_hom
intro i
ext a
· convert hE ⟨(), (b i)⁻¹ • a⟩ ⟨(), a⟩ ⟨i, smul_inv_smul (b i) a⟩
rw [hF' i]
· rw [hF' i]
rfl
apply Functor.hext
· intro
apply Unit.ext
· refine ActionCategory.cases ?_
intro t g
simp only [← hcurried, uncurry_map, curry_apply_left, coe_back, homOfPair.val]
rflAn explicit free-group basis makes the corresponding action groupoid free with controlled generator labels.
lemma actionCategory_eq_of_back_eq {M X : Type u} [Monoid M] [MulAction M X]
{u v : ActionCategory M X} (h : u.back = v.back) : u = vTwo action-category objects are equal when their underlying points are equal.
Show proof
by
cases u
cases v
cases h
rflProof. Fix the chosen Schreier transversal and write each group element as a transversal representative multiplied by an element of the subgroup. The rewriting map is computed letter by letter: after reading a letter, the current coset representative determines the Schreier generator, and the next representative supplies the correction term. The formula is first verified on a single letter and then extended to words by induction on the word list, using concatenation compatibility of the rewriting procedure. The resulting identity in chosen coset representatives is independent of the chosen word presentation after passing through the normal-closure relations, giving the claimed Reidemeister--Schreier formula. At each induction step the current representative and the next representative determine exactly one Schreier generator. The correction terms telescope over a concatenated word, leaving the expected subgroup element at the end of the rewriting. Therefore equality in the subgroup presentation follows from the finite list of rewritten generators and relators, not from any additional relation. The quotient presentation is generated by the Schreier generators, so equality of rewritten generator images determines the induced homomorphism. The normal-closure argument shows that replacing a word by an equivalent word in the original presentation does not change its rewritten image. This supplies the required presentation-level equality. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked.
□