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] : Prop

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 = ⊥

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

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 = ⊥

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.exists_finiteIndexNormalSubgroup_notMem {G : Type u_1} [Group G] [ResiduallyFinite G] (g : G) (hg : g ≠ 1) : ∃ (H : FiniteIndexNormalSubgroup G), g ∉ H

theorem AddGroup.exists_finiteIndexNormalAddSubgroup_notMem {G : Type u_1} [AddGroup G] [ResiduallyFinite G] (g : G) (hg : 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

theorem Group.exists_finiteIndexNormalSubgroup_of_residuallyFinite {G : Type u_1} [Group G] [ResiduallyFinite G] (g h : G) (hgh : g ≠ h) : ∃ (H : FiniteIndexNormalSubgroup G), ↑g ≠ ↑h

If G is residually finite, for every pair of distinct elements g, h there exists a finite index normal subgroup H such that g and h differ in the quotient G ⧸ H.

theorem AddGroup.exists_finiteIndexNormalAddSubgroup_of_residuallyFinite {G : Type u_1} [AddGroup G] [ResiduallyFinite G] (g h : G) (hgh : g ≠ h) : ∃ (H : FiniteIndexNormalAddSubgroup G), ↑g ≠ ↑h

If G is residually finite, for every pair of distinct elements g, h there exists a finite index normal additive subgroup H such that g and h differ in the quotient G ⧸ H.

theorem Group.residuallyFinite_of_forall_exists_finite_monoidHom {G : Type u_1} [Group G] (h : ∀ (g : G), g ≠ 1 → ∃ (H : Type u) (x : Group H) (_ : Finite H) (f : G →* H), f g ≠ 1) : ResiduallyFinite G

G is residually finite if for every element g not equal to 1 there exists a group homomorphism f to a finite group H such that f g ≠ 1.

theorem AddGroup.residuallyFinite_of_forall_exists_finite_addMonoidHom {G : Type u_1} [AddGroup G] (h : ∀ (g : G), g ≠ 0 → ∃ (H : Type u) (x : AddGroup H) (_ : Finite H) (f : G →+ H), f g ≠ 0) : ResiduallyFinite G

G is residually finite if for every element g not equal to 0 there exists an additive group homomorphism f to a finite additive group H such that f g ≠ 0.

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

instance Group.instResiduallyFiniteSubtypeMemSubgroup {G : Type u_1} [Group G] [ResiduallyFinite G] {H : Subgroup G} : ResiduallyFinite ↥H

instance AddGroup.instResiduallyFiniteSubtypeMemAddSubgroup {G : Type u_1} [AddGroup G] [ResiduallyFinite G] {H : AddSubgroup G} : ResiduallyFinite ↥H

instance Group.instResiduallyFiniteProd {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] [ResiduallyFinite G] [ResiduallyFinite G'] : ResiduallyFinite (G × G')

instance AddGroup.instResiduallyFiniteSum {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] [ResiduallyFinite G] [ResiduallyFinite G'] : ResiduallyFinite (G × G')