Documentation

Mathlib.GroupTheory.ResiduallyFinite

Residually Finite Groups #

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

Main definitions #

source
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.

Instances
    source
    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.

    Instances
      source
      theorem Group.residuallyFinite_def {G : Type u_1} [Group G] :
      ResiduallyFinite G ↔ ⨅ (H : FiniteIndexNormalSubgroup G), H.toSubgroup = ⊥
      source
      theorem AddGroup.residuallyFinite_def {G : Type u_1} [AddGroup G] :
      ResiduallyFinite G ↔ ⨅ (H : FiniteIndexNormalAddSubgroup G), H.toAddSubgroup = ⊥
      source
      theorem Group.residuallyFinite_iff_forall_finiteIndexNormalSubgroup {G : Type u_1} [Group G] :
      ResiduallyFinite G ↔ ∀ (g : G), (∀ (H : FiniteIndexNormalSubgroup G), g ∈ H) → g = 1
      source
      theorem AddGroup.residuallyFinite_iff_forall_finiteIndexNormalAddSubgroup {G : Type u_1} [AddGroup G] :
      ResiduallyFinite G ↔ ∀ (g : G), (∀ (H : FiniteIndexNormalAddSubgroup G), g ∈ H) → g = 0
      source
      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
      source
      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
      source
      theorem Group.residuallyFinite_iff_exists_finiteIndexNormalSubgroup {G : Type u_1} [Group G] :
      ResiduallyFinite G ↔ ∀ (g : G), g ≠ 1 → ∃ (H : FiniteIndexNormalSubgroup G), g ∉ H
      source
      theorem AddGroup.residuallyFinite_iff_exists_finiteIndexNormalAddSubgroup {G : Type u_1} [AddGroup G] :
      ResiduallyFinite G ↔ ∀ (g : G), g ≠ 0 → ∃ (H : FiniteIndexNormalAddSubgroup G), g ∉ H
      source
      theorem Group.exists_finiteIndexNormalSubgroup_notMem {G : Type u_1} [Group G] [ResiduallyFinite G] (g : G) (hg : g ≠ 1) :
      ∃ (H : FiniteIndexNormalSubgroup G), g ∉ H
      source
      theorem AddGroup.exists_finiteIndexNormalAddSubgroup_notMem {G : Type u_1} [AddGroup G] [ResiduallyFinite G] (g : G) (hg : g ≠ 0) :
      ∃ (H : FiniteIndexNormalAddSubgroup G), g ∉ H
      source
      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
      source
      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
      source
      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
      source
      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
      source
      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.

      source
      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
      source
      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.

      source
      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
      source
      instance Group.instResiduallyFiniteOfFinite {G : Type u_1} [Group G] [Finite G] :
      ResiduallyFinite G
      source
      instance AddGroup.instResiduallyFiniteOfFinite {G : Type u_1} [AddGroup G] [Finite G] :
      ResiduallyFinite G
      source
      instance Group.instResiduallyFiniteSubtypeMemSubgroup {G : Type u_1} [Group G] [ResiduallyFinite G] {H : Subgroup G} :
      ResiduallyFinite ↥H
      source
      instance AddGroup.instResiduallyFiniteSubtypeMemAddSubgroup {G : Type u_1} [AddGroup G] [ResiduallyFinite G] {H : AddSubgroup G} :
      ResiduallyFinite ↥H
      source
      instance Group.instResiduallyFiniteProd {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] [ResiduallyFinite G] [ResiduallyFinite G'] :
      ResiduallyFinite (G × G')
      source
      instance AddGroup.instResiduallyFiniteSum {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] [ResiduallyFinite G] [ResiduallyFinite G'] :
      ResiduallyFinite (G × G')