ReidemeisterSchreier/Discrete/OpenSubgroups/ClassicalGeneratorBasis.lean
1import ReidemeisterSchreier.Discrete.OpenSubgroups.FreeBasis
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ReidemeisterSchreier/Discrete/OpenSubgroups/ClassicalGeneratorBasis.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
14This focused module keeps the classical value-set Schreier generator basis out of the public root.
15The preferred public basis remains `nontrivialSchreierPairBasis`.
16-/
18namespace ReidemeisterSchreier.Discrete.OpenSubgroups
20section ClassicalGeneratorBasis
22namespace Internal
24/-- A strengthened Schreier-basis existence statement exposing the value of the chosen basis map
25on free generators. This inverse-valued statement records the internal basis orientation used by
27in the subgroup. Use `exists_schreierBasisEquiv` for the positive-valued compatibility theorem. -/
28private theorem IsRightSchreierTransversal.exists_inverseSchreierBasisEquiv
29 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
30 (hT : IsRightSchreierTransversal (X := X) L T) :
31 ∃ e : FreeGroup ↥(schreierGeneratorSet (X := X) hT) ≃* L,
32 ∀ z : ↥(schreierGeneratorSet (X := X) hT),
33 e (FreeGroup.of z) = (z : L)⁻¹ := by
34 classical
35 letI := schreierTransversalRightCosetAction (X := X) hT
36 letI : IsFreeGroupoid (CategoryTheory.ActionCategory (FreeGroup X) T) :=
37 FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
38 let C :
39 Set (Quiver.Total
40 (IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T))) :=
41 ((Quiver.wideSubquiverEquivSetTotal <|
42 Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT))ᶜ : Set _)
43 let b : FreeGroupBasis ↑C L :=
44 (IsFreeGroupoid.SpanningTree.endBasis (schreierPrefixTree (X := X) hT)).map
45 (schreierRootEndMulEquiv (X := X) hT)
46 let toSch : ↑C → ↥(schreierGeneratorSet (X := X) hT) := fun i =>
47 ⟨schreierGenerator (X := X) hT (((i.1.left.back : T) : FreeGroup X)) i.1.hom.1,
48 by
49 refine ⟨
51 i.1.hom.1, rfl, ?_⟩
52 intro hgen
53 exact i.2 (show i.1 ∈ Quiver.wideSubquiverEquivSetTotal
54 (Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT)) from
55 schreierGenerator_eq_one_implies_mem_prefixTree (X := X) hT i.1.hom hgen)⟩
56 have hval : ∀ i : ↑C, (b i : L) =
57 (((toSch i : ↥(schreierGeneratorSet (X := X) hT)) : L)⁻¹) := by
58 intro i
59 rw [FreeGroupBasis.map_apply, IsFreeGroupoid.SpanningTree.endBasis_apply]
60 have htree : ∀ {a b : IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T)}
61 (e : a ⟶ b),
62 e ∈ Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT) a b →
63 (schreierLabelFunctor (X := X) hT).map (IsFreeGroupoid.of e) = (1 : L) := by
64 intro a b e he
65 exact schreierLabelFunctor_map_of_eq_one_of_mem_tree (X := X) hT e he
66 have hloop := IsFreeGroupoid.SpanningTree.map_loopOfHom_eq_map
67 (T := schreierPrefixTree (X := X) hT)
68 (F := schreierLabelFunctor (X := X) hT)
69 (hTree := by
70 intro a b e he
71 exact htree e he)
72 (q := IsFreeGroupoid.of i.1.hom)
73 let loop := IsFreeGroupoid.SpanningTree.loopOfHom (schreierPrefixTree (X := X) hT)
74 (IsFreeGroupoid.of i.1.hom)
75 have hrootEq : (schreierRootEndMulEquiv (X := X) hT loop : L) =
76 (schreierLabelFunctor (X := X) hT).map loop := by
77 apply Subtype.ext
78 change loop.1 = (1 : FreeGroup X) * loop.1 * (1 : FreeGroup X)⁻¹
79 simp only [CategoryTheory.actionAsFunctor_obj, CategoryTheory.actionAsFunctor_map, one_mul, inv_one, mul_one]
80 exact hrootEq.trans <| hloop.trans <| schreierLabelFunctor_map_of (X := X) hT i.1.hom
81 have hto_inj : Function.Injective toSch := by
82 intro i j hij
83 apply b.injective
84 have hz : ((toSch i : ↥(schreierGeneratorSet (X := X) hT)) : L) =
85 ((toSch j : ↥(schreierGeneratorSet (X := X) hT)) : L) := congrArg Subtype.val hij
86 have hz_inv : (((toSch i : ↥(schreierGeneratorSet (X := X) hT)) : L)⁻¹) =
87 (((toSch j : ↥(schreierGeneratorSet (X := X) hT)) : L)⁻¹) := congrArg Inv.inv hz
88 exact (hval i).trans (hz_inv.trans (hval j).symm)
89 have hto_surj : Function.Surjective toSch := by
90 intro z
91 rcases z.2 with ⟨t, ht, x, hz, hne⟩
92 let a : CategoryTheory.ActionCategory (FreeGroup X) T :=
93 ((⟨t, ht⟩ : T) : CategoryTheory.ActionCategory (FreeGroup X) T)
94 let b0 : CategoryTheory.ActionCategory (FreeGroup X) T :=
95 (schreierRepresentative (X := X) hT (t * FreeGroup.of x) : T)
96 let e :
97 (show IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T) from
98 a) ⟶ b0 :=
99 ⟨x, by
100 rw [FreeGroup.inverseBasis_apply]
101 change (FreeGroup.of x)⁻¹ • (show T from CategoryTheory.ActionCategory.back a) =
102 (show T from CategoryTheory.ActionCategory.back b0)
103 simpa [a, b0] using
104 (schreierTransversalRightCosetAction_smul (X := X) hT (FreeGroup.of x)⁻¹ (⟨t, ht⟩ : T))⟩
105 have he_not : ⟨a, b0, e⟩ ∈ C := by
106 change ¬ e ∈ Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT) a b0
107 intro he
108 have hgen1_inv :
109 (schreierGenerator (X := X) hT
110 ((show T from CategoryTheory.ActionCategory.back a) : FreeGroup X) e.1)⁻¹ = 1 := by
111 have htreeLabel :=
112 schreierLabelFunctor_map_of_eq_one_of_mem_tree (X := X) hT e he
113 rw [schreierLabelFunctor_map_of (X := X) hT e] at htreeLabel
114 exact htreeLabel
115 have hgen1 :
116 schreierGenerator (X := X) hT
117 ((show T from CategoryTheory.ActionCategory.back a) : FreeGroup X) e.1 = 1 :=
118 inv_eq_one.mp hgen1_inv
119 exact hne (by simpa [a, e, hz] using hgen1)
120 refine ⟨⟨⟨a, b0, e⟩, he_not⟩, ?_⟩
121 apply Subtype.ext
122 simpa [toSch, a, e] using hz.symm
123 let eC : ↑C ≃ ↥(schreierGeneratorSet (X := X) hT) := Equiv.ofBijective toSch ⟨hto_inj, hto_surj⟩
124 refine ⟨(b.reindex eC).repr.symm, ?_⟩
125 intro z
126 have hbasis :
127 (b.reindex eC).repr.symm (FreeGroup.of z) = (b.reindex eC) z := by
128 apply (b.reindex eC).repr.injective
129 calc
130 (b.reindex eC).repr ((b.reindex eC).repr.symm (FreeGroup.of z))
131 = FreeGroup.of z := by simp only [MulEquiv.apply_symm_apply]
132 _ = (b.reindex eC).repr ((b.reindex eC) z) :=
133 (FreeGroupBasis.repr_apply_coe (b.reindex eC) z).symm
134 calc
135 (b.reindex eC).repr.symm (FreeGroup.of z)
136 = (b.reindex eC) z := hbasis
137 _ = b (eC.symm z) := by
138 rw [FreeGroupBasis.reindex_apply]
139 _ = (((toSch (eC.symm z) : ↥(schreierGeneratorSet (X := X) hT)) : L)⁻¹) :=
140 hval (eC.symm z)
141 _ = (z : L)⁻¹ := by
142 exact congrArg (fun w : ↥(schreierGeneratorSet (X := X) hT) => ((w : L)⁻¹))
143 (eC.apply_symm_apply z)
145end Internal
147/-- Positive-valued Schreier-basis existence statement on the classical Schreier generator set.
148Prefer `nontrivialSchreierPairBasisEquiv` in new public code. -/
149theorem IsRightSchreierTransversal.exists_schreierBasisEquiv
150 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
151 (hT : IsRightSchreierTransversal (X := X) L T) :
152 ∃ e : FreeGroup ↥(schreierGeneratorSet (X := X) hT) ≃* L,
153 ∀ z : ↥(schreierGeneratorSet (X := X) hT),
154 e (FreeGroup.of z) = (z : L) := by
155 classical
156 rcases Internal.IsRightSchreierTransversal.exists_inverseSchreierBasisEquiv hT with
157 ⟨eInverse, hInverse⟩
158 let e : FreeGroup ↥(schreierGeneratorSet (X := X) hT) ≃* L :=
159 (FreeGroup.generatorInversionEquiv ↥(schreierGeneratorSet (X := X) hT)).trans eInverse
160 refine ⟨e, ?_⟩
161 intro z
162 dsimp [e]
163 calc
164 eInverse ((FreeGroup.of z)⁻¹) = (eInverse (FreeGroup.of z))⁻¹ := by simp only [map_inv]
165 _ = ((z : L)⁻¹)⁻¹ := by rw [hInverse z]
168/-- Auxiliary inverse-valued free group equivalence on the classical Schreier generator value set.
169This compatibility route is kept outside the public root; new code should use
171noncomputable def schreierGeneratorInverseBasisEquiv
172 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
173 (hT : IsRightSchreierTransversal (X := X) L T) :
174 FreeGroup ↥(schreierGeneratorSet (X := X) hT) ≃* L :=
175 Classical.choose (Internal.IsRightSchreierTransversal.exists_inverseSchreierBasisEquiv hT)
177/-- The inverse-valued classical generator-set equivalence sends a free generator to the inverse
178of the represented Schreier generator. -/
180 {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
181 (hT : IsRightSchreierTransversal (X := X) L T)
182 (z : ↥(schreierGeneratorSet (X := X) hT)) :
183 schreierGeneratorInverseBasisEquiv (X := X) hT (FreeGroup.of z) = (z : L)⁻¹ :=
184 Classical.choose_spec (Internal.IsRightSchreierTransversal.exists_inverseSchreierBasisEquiv hT) z
186end ClassicalGeneratorBasis
188end ReidemeisterSchreier.Discrete.OpenSubgroups