Documentation

Mathlib.GroupTheory.Finiteness

Finitely generated monoids and groups #

We define finitely generated monoids and groups. See also Submodule.FG and Module.Finite for finitely-generated modules.

Main definition #

Monoids and submonoids #

source
def AddSubmonoid.FG {M : Type u_1} [AddMonoid M] (P : AddSubmonoid M) :
Prop

An additive submonoid of N is finitely generated if it is the closure of a finite subset of M.

Equations
source
def Submonoid.FG {M : Type u_1} [Monoid M] (P : Submonoid M) :
Prop

A submonoid of M is finitely generated if it is the closure of a finite subset of M.

Equations
source
theorem AddSubmonoid.fg_iff {M : Type u_1} [AddMonoid M] (P : AddSubmonoid M) :
P.FG ↔ ∃ (S : Set M), AddSubmonoid.closure S = P ∧ S.Finite

An equivalent expression of AddSubmonoid.FG in terms of Set.Finite instead of Finset.

source
theorem Submonoid.fg_iff {M : Type u_1} [Monoid M] (P : Submonoid M) :
P.FG ↔ ∃ (S : Set M), Submonoid.closure S = P ∧ S.Finite

An equivalent expression of Submonoid.FG in terms of Set.Finite instead of Finset.

source
theorem Submonoid.fg_iff_add_fg {M : Type u_1} [Monoid M] (P : Submonoid M) :
P.FG ↔ (Submonoid.toAddSubmonoid P).FG
source
theorem AddSubmonoid.fg_iff_mul_fg {N : Type u_2} [AddMonoid N] (P : AddSubmonoid N) :
P.FG ↔ (AddSubmonoid.toSubmonoid P).FG
source
class Monoid.FG (M : Type u_1) [Monoid M] :
Prop

A monoid is finitely generated if it is finitely generated as a submonoid of itself.

Instances
    source
    theorem Monoid.FG.out {M : Type u_1} :
    ∀ {inst : Monoid M} [self : Monoid.FG M], ⊤.FG
    source
    class AddMonoid.FG (N : Type u_2) [AddMonoid N] :
    Prop

    An additive monoid is finitely generated if it is finitely generated as an additive submonoid of itself.

    Instances
      source
      theorem AddMonoid.FG.out {N : Type u_2} :
      ∀ {inst : AddMonoid N} [self : AddMonoid.FG N], ⊤.FG
      source
      theorem Monoid.fg_def {M : Type u_1} [Monoid M] :
      Monoid.FG M ↔ ⊤.FG
      source
      theorem AddMonoid.fg_def {N : Type u_2} [AddMonoid N] :
      AddMonoid.FG N ↔ ⊤.FG
      source
      theorem AddMonoid.fg_iff {M : Type u_1} [AddMonoid M] :
      AddMonoid.FG M ↔ ∃ (S : Set M), AddSubmonoid.closure S = ⊤ ∧ S.Finite

      An equivalent expression of AddMonoid.FG in terms of Set.Finite instead of Finset.

      source
      theorem Monoid.fg_iff {M : Type u_1} [Monoid M] :
      Monoid.FG M ↔ ∃ (S : Set M), Submonoid.closure S = ⊤ ∧ S.Finite

      An equivalent expression of Monoid.FG in terms of Set.Finite instead of Finset.

      source
      theorem Monoid.fg_iff_add_fg {M : Type u_1} [Monoid M] :
      Monoid.FG M ↔ AddMonoid.FG (Additive M)
      source
      theorem AddMonoid.fg_iff_mul_fg {N : Type u_2} [AddMonoid N] :
      AddMonoid.FG N ↔ Monoid.FG (Multiplicative N)
      source
      instance AddMonoid.fg_of_monoid_fg {M : Type u_1} [Monoid M] [Monoid.FG M] :
      AddMonoid.FG (Additive M)
      Equations
      • ⋯ = ⋯
      source
      instance Monoid.fg_of_addMonoid_fg {N : Type u_2} [AddMonoid N] [AddMonoid.FG N] :
      Monoid.FG (Multiplicative N)
      Equations
      • ⋯ = ⋯
      source
      @[instance 100]
      instance AddMonoid.fg_of_finite {M : Type u_1} [AddMonoid M] [Finite M] :
      AddMonoid.FG M
      Equations
      • ⋯ = ⋯
      source
      @[instance 100]
      instance Monoid.fg_of_finite {M : Type u_1} [Monoid M] [Finite M] :
      Monoid.FG M
      Equations
      • ⋯ = ⋯
      source
      theorem AddSubmonoid.FG.map {M : Type u_1} [AddMonoid M] {M' : Type u_3} [AddMonoid M'] {P : AddSubmonoid M} (h : P.FG) (e : M →+ M') :
      (AddSubmonoid.map e P).FG
      source
      theorem Submonoid.FG.map {M : Type u_1} [Monoid M] {M' : Type u_3} [Monoid M'] {P : Submonoid M} (h : P.FG) (e : M →* M') :
      (Submonoid.map e P).FG
      source
      theorem AddSubmonoid.FG.map_injective {M : Type u_1} [AddMonoid M] {M' : Type u_3} [AddMonoid M'] {P : AddSubmonoid M} (e : M →+ M') (he : Function.Injective ⇑e) (h : (AddSubmonoid.map e P).FG) :
      P.FG
      source
      theorem Submonoid.FG.map_injective {M : Type u_1} [Monoid M] {M' : Type u_3} [Monoid M'] {P : Submonoid M} (e : M →* M') (he : Function.Injective ⇑e) (h : (Submonoid.map e P).FG) :
      P.FG
      source
      @[simp]
      theorem AddMonoid.fg_iff_addSubmonoid_fg {M : Type u_1} [AddMonoid M] (N : AddSubmonoid M) :
      AddMonoid.FG ↥N ↔ N.FG
      source
      @[simp]
      theorem Monoid.fg_iff_submonoid_fg {M : Type u_1} [Monoid M] (N : Submonoid M) :
      Monoid.FG ↥N ↔ N.FG
      source
      theorem AddMonoid.fg_of_surjective {M : Type u_1} [AddMonoid M] {M' : Type u_3} [AddMonoid M'] [AddMonoid.FG M] (f : M →+ M') (hf : Function.Surjective ⇑f) :
      AddMonoid.FG M'
      source
      theorem Monoid.fg_of_surjective {M : Type u_1} [Monoid M] {M' : Type u_3} [Monoid M'] [Monoid.FG M] (f : M →* M') (hf : Function.Surjective ⇑f) :
      Monoid.FG M'
      source
      instance AddMonoid.fg_range {M : Type u_1} [AddMonoid M] {M' : Type u_3} [AddMonoid M'] [AddMonoid.FG M] (f : M →+ M') :
      AddMonoid.FG ↥(AddMonoidHom.mrange f)
      Equations
      • ⋯ = ⋯
      source
      instance Monoid.fg_range {M : Type u_1} [Monoid M] {M' : Type u_3} [Monoid M'] [Monoid.FG M] (f : M →* M') :
      Monoid.FG ↥(MonoidHom.mrange f)
      Equations
      • ⋯ = ⋯
      source
      theorem AddSubmonoid.multiples_fg {M : Type u_1} [AddMonoid M] (r : M) :
      (AddSubmonoid.multiples r).FG
      source
      theorem Submonoid.powers_fg {M : Type u_1} [Monoid M] (r : M) :
      (Submonoid.powers r).FG
      source
      instance AddMonoid.multiples_fg {M : Type u_1} [AddMonoid M] (r : M) :
      AddMonoid.FG ↥(AddSubmonoid.multiples r)
      Equations
      • ⋯ = ⋯
      source
      instance Monoid.powers_fg {M : Type u_1} [Monoid M] (r : M) :
      Monoid.FG ↥(Submonoid.powers r)
      Equations
      • ⋯ = ⋯
      source
      instance AddMonoid.closure_finset_fg {M : Type u_1} [AddMonoid M] (s : Finset M) :
      AddMonoid.FG ↥(AddSubmonoid.closure ↑s)
      Equations
      • ⋯ = ⋯
      source
      instance Monoid.closure_finset_fg {M : Type u_1} [Monoid M] (s : Finset M) :
      Monoid.FG ↥(Submonoid.closure ↑s)
      Equations
      • ⋯ = ⋯
      source
      instance AddMonoid.closure_finite_fg {M : Type u_1} [AddMonoid M] (s : Set M) [Finite ↑s] :
      AddMonoid.FG ↥(AddSubmonoid.closure s)
      Equations
      • ⋯ = ⋯
      source
      instance Monoid.closure_finite_fg {M : Type u_1} [Monoid M] (s : Set M) [Finite ↑s] :
      Monoid.FG ↥(Submonoid.closure s)
      Equations
      • ⋯ = ⋯

      Groups and subgroups #

      source
      def AddSubgroup.FG {G : Type u_3} [AddGroup G] (P : AddSubgroup G) :
      Prop

      An additive subgroup of H is finitely generated if it is the closure of a finite subset of H.

      Equations
      source
      def Subgroup.FG {G : Type u_3} [Group G] (P : Subgroup G) :
      Prop

      A subgroup of G is finitely generated if it is the closure of a finite subset of G.

      Equations
      source
      theorem AddSubgroup.fg_iff {G : Type u_3} [AddGroup G] (P : AddSubgroup G) :
      P.FG ↔ ∃ (S : Set G), AddSubgroup.closure S = P ∧ S.Finite

      An equivalent expression of AddSubgroup.fg in terms of Set.Finite instead of Finset.

      source
      theorem Subgroup.fg_iff {G : Type u_3} [Group G] (P : Subgroup G) :
      P.FG ↔ ∃ (S : Set G), Subgroup.closure S = P ∧ S.Finite

      An equivalent expression of Subgroup.FG in terms of Set.Finite instead of Finset.

      source
      theorem AddSubgroup.fg_iff_addSubmonoid_fg {G : Type u_3} [AddGroup G] (P : AddSubgroup G) :
      P.FG ↔ P.FG

      An additive subgroup is finitely generated if and only if it is finitely generated as an additive submonoid.

      source
      theorem Subgroup.fg_iff_submonoid_fg {G : Type u_3} [Group G] (P : Subgroup G) :
      P.FG ↔ P.FG

      A subgroup is finitely generated if and only if it is finitely generated as a submonoid.

      source
      theorem Subgroup.fg_iff_add_fg {G : Type u_3} [Group G] (P : Subgroup G) :
      P.FG ↔ (Subgroup.toAddSubgroup P).FG
      source
      theorem AddSubgroup.fg_iff_mul_fg {H : Type u_4} [AddGroup H] (P : AddSubgroup H) :
      P.FG ↔ (AddSubgroup.toSubgroup P).FG
      source
      class Group.FG (G : Type u_3) [Group G] :
      Prop

      A group is finitely generated if it is finitely generated as a submonoid of itself.

      Instances
        source
        theorem Group.FG.out {G : Type u_3} :
        ∀ {inst : Group G} [self : Group.FG G], ⊤.FG
        source
        class AddGroup.FG (H : Type u_4) [AddGroup H] :
        Prop

        An additive group is finitely generated if it is finitely generated as an additive submonoid of itself.

        Instances
          source
          theorem AddGroup.FG.out {H : Type u_4} :
          ∀ {inst : AddGroup H} [self : AddGroup.FG H], ⊤.FG
          source
          theorem Group.fg_def {G : Type u_3} [Group G] :
          Group.FG G ↔ ⊤.FG
          source
          theorem AddGroup.fg_def {H : Type u_4} [AddGroup H] :
          AddGroup.FG H ↔ ⊤.FG
          source
          theorem AddGroup.fg_iff {G : Type u_3} [AddGroup G] :
          AddGroup.FG G ↔ ∃ (S : Set G), AddSubgroup.closure S = ⊤ ∧ S.Finite

          An equivalent expression of AddGroup.fg in terms of Set.Finite instead of Finset.

          source
          theorem Group.fg_iff {G : Type u_3} [Group G] :
          Group.FG G ↔ ∃ (S : Set G), Subgroup.closure S = ⊤ ∧ S.Finite

          An equivalent expression of Group.FG in terms of Set.Finite instead of Finset.

          source
          theorem AddGroup.fg_iff' {G : Type u_3} [AddGroup G] :
          AddGroup.FG G ↔ ∃ (n : ℕ) (S : Finset G), S.card = n ∧ AddSubgroup.closure ↑S = ⊤
          source
          theorem Group.fg_iff' {G : Type u_3} [Group G] :
          Group.FG G ↔ ∃ (n : ℕ) (S : Finset G), S.card = n ∧ Subgroup.closure ↑S = ⊤
          source
          theorem AddGroup.fg_iff_addMonoid_fg {G : Type u_3} [AddGroup G] :
          AddGroup.FG G ↔ AddMonoid.FG G

          An additive group is finitely generated if and only if it is finitely generated as an additive monoid.

          source
          theorem Group.fg_iff_monoid_fg {G : Type u_3} [Group G] :
          Group.FG G ↔ Monoid.FG G

          A group is finitely generated if and only if it is finitely generated as a monoid.

          source
          @[simp]
          theorem AddGroup.fg_iff_addSubgroup_fg {G : Type u_3} [AddGroup G] (H : AddSubgroup G) :
          AddGroup.FG ↥H ↔ H.FG
          source
          @[simp]
          theorem Group.fg_iff_subgroup_fg {G : Type u_3} [Group G] (H : Subgroup G) :
          Group.FG ↥H ↔ H.FG
          source
          theorem GroupFG.iff_add_fg {G : Type u_3} [Group G] :
          Group.FG G ↔ AddGroup.FG (Additive G)
          source
          theorem AddGroup.fg_iff_mul_fg {H : Type u_4} [AddGroup H] :
          AddGroup.FG H ↔ Group.FG (Multiplicative H)
          source
          instance AddGroup.fg_of_group_fg {G : Type u_3} [Group G] [Group.FG G] :
          AddGroup.FG (Additive G)
          Equations
          • ⋯ = ⋯
          source
          instance Group.fg_of_mul_group_fg {H : Type u_4} [AddGroup H] [AddGroup.FG H] :
          Group.FG (Multiplicative H)
          Equations
          • ⋯ = ⋯
          source
          @[instance 100]
          instance AddGroup.fg_of_finite {G : Type u_3} [AddGroup G] [Finite G] :
          AddGroup.FG G
          Equations
          • ⋯ = ⋯
          source
          @[instance 100]
          instance Group.fg_of_finite {G : Type u_3} [Group G] [Finite G] :
          Group.FG G
          Equations
          • ⋯ = ⋯
          source
          theorem AddGroup.fg_of_surjective {G : Type u_3} [AddGroup G] {G' : Type u_5} [AddGroup G'] [hG : AddGroup.FG G] {f : G →+ G'} (hf : Function.Surjective ⇑f) :
          AddGroup.FG G'
          source
          theorem Group.fg_of_surjective {G : Type u_3} [Group G] {G' : Type u_5} [Group G'] [hG : Group.FG G] {f : G →* G'} (hf : Function.Surjective ⇑f) :
          Group.FG G'
          source
          instance AddGroup.fg_range {G : Type u_3} [AddGroup G] {G' : Type u_5} [AddGroup G'] [AddGroup.FG G] (f : G →+ G') :
          AddGroup.FG ↥f.range
          Equations
          • ⋯ = ⋯
          source
          instance Group.fg_range {G : Type u_3} [Group G] {G' : Type u_5} [Group G'] [Group.FG G] (f : G →* G') :
          Group.FG ↥f.range
          Equations
          • ⋯ = ⋯
          source
          instance AddGroup.closure_finset_fg {G : Type u_3} [AddGroup G] (s : Finset G) :
          AddGroup.FG ↥(AddSubgroup.closure ↑s)
          Equations
          • ⋯ = ⋯
          source
          instance Group.closure_finset_fg {G : Type u_3} [Group G] (s : Finset G) :
          Group.FG ↥(Subgroup.closure ↑s)
          Equations
          • ⋯ = ⋯
          source
          instance AddGroup.closure_finite_fg {G : Type u_3} [AddGroup G] (s : Set G) [Finite ↑s] :
          AddGroup.FG ↥(AddSubgroup.closure s)
          Equations
          • ⋯ = ⋯
          source
          instance Group.closure_finite_fg {G : Type u_3} [Group G] (s : Set G) [Finite ↑s] :
          Group.FG ↥(Subgroup.closure s)
          Equations
          • ⋯ = ⋯
          source
          noncomputable def AddGroup.rank (G : Type u_3) [AddGroup G] [h : AddGroup.FG G] :
          ℕ

          The minimum number of generators of an additive group

          Equations
          source
          noncomputable def Group.rank (G : Type u_3) [Group G] [h : Group.FG G] :
          ℕ

          The minimum number of generators of a group.

          Equations
          source
          theorem AddGroup.rank_spec (G : Type u_3) [AddGroup G] [h : AddGroup.FG G] :
          ∃ (S : Finset G), S.card = AddGroup.rank G ∧ AddSubgroup.closure ↑S = ⊤
          source
          theorem Group.rank_spec (G : Type u_3) [Group G] [h : Group.FG G] :
          ∃ (S : Finset G), S.card = Group.rank G ∧ Subgroup.closure ↑S = ⊤
          source
          theorem AddGroup.rank_le (G : Type u_3) [AddGroup G] [h : AddGroup.FG G] {S : Finset G} (hS : AddSubgroup.closure ↑S = ⊤) :
          AddGroup.rank G ≤ S.card
          source
          theorem Group.rank_le (G : Type u_3) [Group G] [h : Group.FG G] {S : Finset G} (hS : Subgroup.closure ↑S = ⊤) :
          Group.rank G ≤ S.card
          source
          theorem AddGroup.rank_le_of_surjective {G : Type u_3} [AddGroup G] {G' : Type u_5} [AddGroup G'] [AddGroup.FG G] [AddGroup.FG G'] (f : G →+ G') (hf : Function.Surjective ⇑f) :
          AddGroup.rank G' ≤ AddGroup.rank G
          source
          theorem Group.rank_le_of_surjective {G : Type u_3} [Group G] {G' : Type u_5} [Group G'] [Group.FG G] [Group.FG G'] (f : G →* G') (hf : Function.Surjective ⇑f) :
          Group.rank G' ≤ Group.rank G
          source
          theorem AddGroup.rank_range_le {G : Type u_3} [AddGroup G] {G' : Type u_5} [AddGroup G'] [AddGroup.FG G] {f : G →+ G'} :
          AddGroup.rank ↥f.range ≤ AddGroup.rank G
          source
          theorem Group.rank_range_le {G : Type u_3} [Group G] {G' : Type u_5} [Group G'] [Group.FG G] {f : G →* G'} :
          Group.rank ↥f.range ≤ Group.rank G
          source
          theorem AddGroup.rank_congr {G : Type u_3} [AddGroup G] {G' : Type u_5} [AddGroup G'] [AddGroup.FG G] [AddGroup.FG G'] (f : G ≃+ G') :
          AddGroup.rank G = AddGroup.rank G'
          source
          theorem Group.rank_congr {G : Type u_3} [Group G] {G' : Type u_5} [Group G'] [Group.FG G] [Group.FG G'] (f : G ≃* G') :
          Group.rank G = Group.rank G'
          source
          theorem AddSubgroup.rank_congr {G : Type u_3} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} [AddGroup.FG ↥H] [AddGroup.FG ↥K] (h : H = K) :
          AddGroup.rank ↥H = AddGroup.rank ↥K
          source
          theorem Subgroup.rank_congr {G : Type u_3} [Group G] {H : Subgroup G} {K : Subgroup G} [Group.FG ↥H] [Group.FG ↥K] (h : H = K) :
          Group.rank ↥H = Group.rank ↥K
          source
          theorem AddSubgroup.rank_closure_finset_le_card {G : Type u_3} [AddGroup G] (s : Finset G) :
          AddGroup.rank ↥(AddSubgroup.closure ↑s) ≤ s.card
          source
          theorem Subgroup.rank_closure_finset_le_card {G : Type u_3} [Group G] (s : Finset G) :
          Group.rank ↥(Subgroup.closure ↑s) ≤ s.card
          source
          theorem AddSubgroup.rank_closure_finite_le_nat_card {G : Type u_3} [AddGroup G] (s : Set G) [Finite ↑s] :
          AddGroup.rank ↥(AddSubgroup.closure s) ≤ Nat.card ↑s
          source
          theorem Subgroup.rank_closure_finite_le_nat_card {G : Type u_3} [Group G] (s : Set G) [Finite ↑s] :
          Group.rank ↥(Subgroup.closure s) ≤ Nat.card ↑s
          source
          instance QuotientAddGroup.fg {G : Type u_3} [AddGroup G] [AddGroup.FG G] (N : AddSubgroup G) [N.Normal] :
          AddGroup.FG (G ⧸ N)
          Equations
          • ⋯ = ⋯
          source
          instance QuotientGroup.fg {G : Type u_3} [Group G] [Group.FG G] (N : Subgroup G) [N.Normal] :
          Group.FG (G ⧸ N)
          Equations
          • ⋯ = ⋯