Documentation

Mathlib.GroupTheory.ResiduallyFinite

Residually Finite Groups #

In this file we define residually finite groups and prove some basic properties.

Main definitions #

Group.ResiduallyFinite G: A group G is residually finite if the intersection of all finite index normal subgroups is trivial.

class AddGroup.ResiduallyFinite (G : Type u_1) [AddGroup G] :

An additive group G is residually finite if the intersection of all finite index normal additive subgroups is trivial.

iInf_eq_bot : ⨅ (H : FiniteIndexNormalAddSubgroup G), H.toAddSubgroup = ⊥

Instances

class Group.ResiduallyFinite (G : Type u_1) [Group G] :

A group G is residually finite if the intersection of all finite index normal subgroups is trivial.

iInf_eq_bot : ⨅ (H : FiniteIndexNormalSubgroup G), H.toSubgroup = ⊥

Instances

theorem Group.residuallyFinite_def {G : Type u_1} [Group G] :

ResiduallyFinite G ↔ ⨅ (H : FiniteIndexNormalSubgroup G), H.toSubgroup = ⊥

theorem AddGroup.residuallyFinite_def {G : Type u_1} [AddGroup G] :

ResiduallyFinite G ↔ ⨅ (H : FiniteIndexNormalAddSubgroup G), H.toAddSubgroup = ⊥

theorem Group.residuallyFinite_iff_forall_finiteIndexNormalSubgroup {G : Type u_1} [Group G] :

ResiduallyFinite G ↔ ∀ (g : G), (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1

theorem AddGroup.residuallyFinite_iff_forall_finiteIndexNormalAddSubgroup {G : Type u_1} [AddGroup G] :

ResiduallyFinite G ↔ ∀ (g : G), (∀ (H : FiniteIndexNormalAddSubgroup G), g ∈ H) → g = 0

theorem Group.eq_one_iff_forall_finiteIndexNormalSubroup {G : Type u_1} [Group G] [ResiduallyFinite G] (g : G) (hg : ∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) :

g = 1

theorem AddGroup.eq_zero_iff_forall_finiteIndexNormalSubroup {G : Type u_1} [AddGroup G] [ResiduallyFinite G] (g : G) (hg : ∀ (H : FiniteIndexNormalAddSubgroup G), g ∈ H) :

g = 0

theorem Group.residuallyFinite_iff_exists_finiteIndexNormalSubgroup {G : Type u_1} [Group G] :

ResiduallyFinite G ↔ ∀ (g : G), g ≠ 1 → ∃ (H : FiniteIndexNormalSubgroup G), g ∉ H

theorem AddGroup.residuallyFinite_iff_exists_finiteIndexNormalAddSubgroup {G : Type u_1} [AddGroup G] :

ResiduallyFinite G ↔ ∀ (g : G), g ≠ 0 → ∃ (H : FiniteIndexNormalAddSubgroup G), g ∉ H

theorem Group.residuallyFinite_iff_forall_finiteIndex {G : Type u_1} [Group G] :

ResiduallyFinite G ↔ ∀ (g : G), (∀ (H : Subgroup G) [H.FiniteIndex], g ∈ H) → g = 1

theorem AddGroup.residuallyFinite_iff_forall_finiteIndex {G : Type u_1} [AddGroup G] :

ResiduallyFinite G ↔ ∀ (g : G), (∀ (H : AddSubgroup G) [H.FiniteIndex], g ∈ H) → g = 0

theorem Group.residuallyFinite_iff_exists_finiteIndex {G : Type u_1} [Group G] :

ResiduallyFinite G ↔ ∀ (g : G), g ≠ 1 → ∃ (H : Subgroup G), H.FiniteIndex ∧ g ∉ H

theorem AddGroup.residuallyFinite_iff_exists_finiteIndex {G : Type u_1} [AddGroup G] :

ResiduallyFinite G ↔ ∀ (g : G), g ≠ 0 → ∃ (H : AddSubgroup G), H.FiniteIndex ∧ g ∉ H

instance Group.instResiduallyFiniteOfFinite {G : Type u_1} [Group G] [Finite G] :

ResiduallyFinite G

instance AddGroup.instResiduallyFiniteOfFinite {G : Type u_1} [AddGroup G] [Finite G] :

ResiduallyFinite G