ReidemeisterSchreier/Discrete/OpenSubgroups/Words/NielsenSchreierCompat.lean
1import ReidemeisterSchreier.Groupoid
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ReidemeisterSchreier/Discrete/OpenSubgroups/Words/NielsenSchreierCompat.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Free-word compatibility for Schreier theory
14Free-group word lemmas, prefix-parent compatibility, Nielsen-Schreier calculations, and cancellation rules for Schreier generators.
15-/
17namespace ReidemeisterSchreier.Discrete.OpenSubgroups
19section NielsenSchreierCompat
21open scoped Pointwise
22open CategoryTheory CategoryTheory.ActionCategory CategoryTheory.SingleObj Quiver FreeGroup
24/-- A basis-level version of `IsFreeGroupoid.actionGroupoidIsFree`. Using an explicit
26`IsFreeGroup.Generators`. -/
27noncomputable def FreeGroupBasis.actionGroupoidIsFree
28 {ι G A : Type u} [Group G] [MulAction G A] (b : FreeGroupBasis ι G) :
29 IsFreeGroupoid (ActionCategory G A) where
30 quiverGenerators :=
31 ⟨fun a b' => { i : ι // b i • a.back = b'.back }⟩
32 of := fun (e : Subtype _) => ⟨b e, e.property⟩
33 unique_lift := by
34 intro X _ f
35 let f' : ι → (A → X) ⋊[mulAutArrow] G := fun i =>
36 ⟨fun a =>
37 @f ⟨(), (b i)⁻¹ • a⟩ ⟨(), a⟩
38 ⟨i, smul_inv_smul (b i) a⟩,
39 b i⟩
40 let F' : G →* (A → X) ⋊[mulAutArrow] G := b.lift f'
41 have hF' : ∀ i, F' (b i) = f' i := congrFun (b.lift.left_inv f')
42 refine ⟨uncurry F' ?_, ?_, ?_⟩
43 · intro g
44 suffices SemidirectProduct.rightHom.comp F' = MonoidHom.id G by
45 exact DFunLike.ext_iff.mp this g
46 apply b.ext_hom
47 intro i
48 rw [MonoidHom.comp_apply, hF' i]
49 rfl
50 · rintro ⟨⟨⟩, a : A⟩ ⟨⟨⟩, b'⟩ ⟨i, h : b i • a = b'⟩
51 change (F' (b i)).left _ = _
52 rw [hF' i]
53 cases inv_smul_eq_iff.mpr h.symm
54 rfl
55 · intro E hE
56 have hcurried : curry E = F' := by
57 apply b.ext_hom
58 intro i
59 ext a
60 · convert hE ⟨(), (b i)⁻¹ • a⟩ ⟨(), a⟩ ⟨i, smul_inv_smul (b i) a⟩
61 rw [hF' i]
62 · rw [hF' i]
63 rfl
64 apply Functor.hext
65 · intro
66 apply Unit.ext
67 · refine ActionCategory.cases ?_
68 intro t g
69 simp only [← hcurried, uncurry_map, curry_apply_left, coe_back, homOfPair.val]
70 rfl
72lemma actionCategory_eq_of_back_eq {M X : Type u} [Monoid M] [MulAction M X]
73 {u v : ActionCategory M X} (h : u.back = v.back) : u = v := by
74 cases u
75 cases v
76 cases h
77 rfl
79end NielsenSchreierCompat
81end ReidemeisterSchreier.Discrete.OpenSubgroups