ResidualFiniteness.lean`

56 declarations, 0 contain sorry, 0 declared as axioms

Finite permutation separation for free groups.

theorem OAI.EilenbergGanea.finite_translation_extension line 21
Source documentation
Left translation, restricted wherever both endpoints lie in a finite set, extends to a permutation of that finite set.
```
theorem finite_translation_extension (s : Finset A) (a : A) :
    ∃ σ : Equiv.Perm s, ∀ (x : s), a * x.val ∈ s → (σ x).val = a * x.val := by
…
```
def OAI.EilenbergGanea.finiteTranslation line 36
theorem OAI.EilenbergGanea.finiteTranslation_apply line 39
theorem OAI.EilenbergGanea.finiteTranslation_inv_apply line 43
def OAI.EilenbergGanea.wordVertices line 57
Source documentation
The finite set of suffix vertices of a free word, including both endpoints.
```
def wordVertices (w : List (X × Bool)) : Finset (FreeGroup X) := by
…
```
theorem OAI.EilenbergGanea.mk_mem_wordVertices line 61
theorem OAI.EilenbergGanea.one_mem_wordVertices line 66
theorem OAI.EilenbergGanea.wordVertices_tail_subset line 71
theorem OAI.EilenbergGanea.mk_cons_sign line 77
def OAI.EilenbergGanea.finiteWordAction line 82
theorem OAI.EilenbergGanea.finiteWordAction_tracks line 88
Source documentation
Whenever a finite set includes all suffix vertices, the finite action follows that word exactly starting at the identity. No reduced-word choice is needed.
```
theorem finiteWordAction_tracks (s : Finset (FreeGroup X)) (w : List (X × Bool))
    (hw : wordVertices w ⊆ s) (h1 : (1 : FreeGroup X) ∈ s) :
    (finiteWordAction s (FreeGroup.mk w) ⟨1, h1⟩).val = FreeGroup.mk w := by
…
```
Mentions: OAI.EilenbergGanea.wordVertices, OAI.EilenbergGanea.finiteWordAction
theorem OAI.EilenbergGanea.freeGroup_residuallyFinite line 116
Source documentation
Free groups on arbitrary types are residually finite; this is proved using finite partial translations, not assumed as a literature result.
```
theorem freeGroup_residuallyFinite (X : Type*) : Group.ResiduallyFinite (FreeGroup X) := by
…
```
def OAI.EilenbergGanea.functionShift line 137
Source documentation
The right translation action on a group-valued function space.
```
def functionShift (D K : Type*) [Group D] [Group K] : D →* MulAut (D → K) where
…
```
def OAI.EilenbergGanea.orbitObservation line 148
Source documentation
All translates of a finite observation of the normal factor, simultaneously.
```
def orbitObservation (φ : D →* MulAut N) (f : N →* K) : N →* (D → K) where
…
```
theorem OAI.EilenbergGanea.orbitObservation_equivariant line 153
theorem OAI.EilenbergGanea.finite_semidirect_residuallyFinite line 161
Source documentation
A finite extension of a residually finite group is residually finite. Only the semidirect form needed by the source is used.
```
theorem finite_semidirect_residuallyFinite [Finite D] [Group.ResiduallyFinite N]
    (φ : D →* MulAut N) : Group.ResiduallyFinite (N ⋊[φ] D) := by
…
```
def OAI.EilenbergGanea.freeAction line 197
theorem OAI.EilenbergGanea.freeAction_of line 212
theorem OAI.EilenbergGanea.freeAction_apply line 215
theorem OAI.EilenbergGanea.freeAction_map_equivariant line 220
theorem OAI.EilenbergGanea.finite_nonidentity_separation line 236
Source documentation
Finitely many nonidentity elements can be excluded by one finite quotient.
```
theorem finite_nonidentity_separation (s : Finset A) :
    ∃ H : FiniteIndexNormalSubgroup A, ∀ a ∈ s, a ≠ 1 → a ∉ H := by
…
```

theorem OAI.EilenbergGanea.finite_set_quotient_injective line 258

Source documentation

The exact finite-set injectivity consequence of residual finiteness.

theorem finite_set_quotient_injective (s : Finset A) :
    ∃ H : FiniteIndexNormalSubgroup A,
      Set.InjOn (QuotientGroup.mk' H.toSubgroup) (s : Set A) := by
…

def OAI.EilenbergGanea.cosetMap line 279
Source documentation
A homomorphism induces a map on left cosets of a subgroup, without a normality hypothesis on that subgroup.
```
def cosetMap (q : A →* D) (C : Subgroup A) : A ⧸ C → D ⧸ C.map q :=
…
```
theorem OAI.EilenbergGanea.cosetMap_mk line 286
theorem OAI.EilenbergGanea.cosetMap_equivariant line 289
theorem OAI.EilenbergGanea.cosetMap_out line 294

theorem OAI.EilenbergGanea.retract_coset_finite_separation line 300

Source documentation

A retract is separable on any finite set of cosets. The two observations (p, p ∘ r) implement the source's diagonal separation argument exactly.

theorem retract_coset_finite_separation [Group.ResiduallyFinite A]
    (C : Subgroup A) (r : A →* A) (hr : ∀ a, r a ∈ C)
    (hfix : ∀ c ∈ C, r c = c) (s : Finset (A ⧸ C)) :
    ∃ (D : Type u) (_ : Group D) (_ : Finite D) (q : A →* D),
      Set.InjOn (cosetMap q C) (s : Set (A ⧸ C)) := by
…

Mentions: OAI.EilenbergGanea.cosetMap

theorem OAI.EilenbergGanea.freeGroup_map_ne_one_of_injOn line 337

Source documentation

Only the finitely many letters of a word must survive a map of alphabets.

theorem freeGroup_map_ne_one_of_injOn {X Y : Type*} [Nonempty X] [DecidableEq X]
    (f : X → Y) (w : FreeGroup X) (hw : w ≠ 1)
    (hf : Set.InjOn f {x | x ∈ w.toWord.map Prod.fst}) :
    FreeGroup.map f w ≠ 1 := by
…

theorem OAI.EilenbergGanea.retract_semidirect_residuallyFinite line 361

Source documentation

The special permutational semidirect product used to add a graph-group vertex is residually finite when the stabilizer is a retract.

theorem retract_semidirect_residuallyFinite {A : Type u} [Group A]
    [Group.ResiduallyFinite A] (C : Subgroup A) (r : A →* A)
    (hr : ∀ a, r a ∈ C) (hfix : ∀ c ∈ C, r c = c) :
    Group.ResiduallyFinite (FreeGroup (A ⧸ C) ⋊[freeAction A (A ⧸ C)] A) := by
…

Mentions: OAI.EilenbergGanea.freeAction

def OAI.EilenbergGanea.artinLift line 405

Source documentation

Universal property in commuting-generator form.

def artinLift (f : V → K) (hf : ∀ v w, L.Adj v w → Commute (f v) (f w)) :
    ArtinGroup L →* K :=
…

theorem OAI.EilenbergGanea.artinLift_generator line 413

def OAI.EilenbergGanea.artinMap line 419

Source documentation

Renaming vertices along a graph isomorphism gives the expected group map.

def artinMap (M : SimpleGraph W) (f : V → W)
    (hf : ∀ v w, L.Adj v w → M.Adj (f v) (f w)) : ArtinGroup L →* ArtinGroup M :=
…

theorem OAI.EilenbergGanea.artinMap_generator line 424

theorem OAI.EilenbergGanea.residuallyFinite_of_injective line 430

Source documentation

Residual finiteness pulls back along an injective homomorphism.

theorem residuallyFinite_of_injective {G H : Type*} [Group G] [Group H]
    [Group.ResiduallyFinite H] (f : G →* H) (hf : Function.Injective f) :
    Group.ResiduallyFinite G := by
…

def OAI.EilenbergGanea.cosetConjugate line 448
Source documentation
The formal inverse to the graph-group splitting, on its free generators.
```
def cosetConjugate (C : Subgroup A) (i : A →* P) (t : P)
    (ht : ∀ c ∈ C, Commute (i c) t) : A ⧸ C → P :=
…
```
theorem OAI.EilenbergGanea.cosetConjugate_mk line 460
theorem OAI.EilenbergGanea.cosetConjugate_equivariant line 464
def OAI.EilenbergGanea.cosetSemidirectLift line 472
theorem OAI.EilenbergGanea.cosetSemidirectLift_inr line 481
theorem OAI.EilenbergGanea.cosetSemidirectLift_base line 486
abbrev OAI.EilenbergGanea.deletedGraph line 498
abbrev OAI.EilenbergGanea.deletedGroup line 499
def OAI.EilenbergGanea.deletedInclusion line 501
def OAI.EilenbergGanea.linkSubgroup line 504
def OAI.EilenbergGanea.linkRetraction line 509
theorem OAI.EilenbergGanea.linkRetraction_generator line 519
theorem OAI.EilenbergGanea.linkRetraction_mem line 524
theorem OAI.EilenbergGanea.linkRetraction_fix line 535
theorem OAI.EilenbergGanea.link_commutes_new line 545
abbrev OAI.EilenbergGanea.optionSemidirect line 555
def OAI.EilenbergGanea.optionGenerator line 558
theorem OAI.EilenbergGanea.optionGenerator_commute line 562
def OAI.EilenbergGanea.optionForward line 585
def OAI.EilenbergGanea.optionBackward line 588
theorem OAI.EilenbergGanea.optionForward_injective line 592
theorem OAI.EilenbergGanea.artin_residuallyFinite line 604
Source documentation
Graph groups on finite graphs are residually finite, by deletion of a vertex and the retract-coset semidirect splitting.
```
theorem artin_residuallyFinite (V : Type u) [Finite V] (L : SimpleGraph V) :
    Group.ResiduallyFinite (ArtinGroup L) := by
…
```