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 #

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

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

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

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

    Equations
    Instances For
      abbrev AddSubmonoid.fg_iff.match_1 {M : Type u_1} [AddMonoid M] (P : AddSubmonoid M) (motive : AddSubmonoid.FG PProp) :
      (x : AddSubmonoid.FG P) → ((S : Finset M) → (hS : AddSubmonoid.closure S = P) → motive (_ : S, AddSubmonoid.closure S = P)) → motive x
      Equations
      Instances For

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

        abbrev AddSubmonoid.fg_iff.match_2 {M : Type u_1} [AddMonoid M] (P : AddSubmonoid M) (motive : (S, AddSubmonoid.closure S = P Set.Finite S) → Prop) :
        (x : S, AddSubmonoid.closure S = P Set.Finite S) → ((S : Set M) → (hS : AddSubmonoid.closure S = P) → (hf : Set.Finite S) → motive (_ : S, AddSubmonoid.closure S = P Set.Finite S)) → motive x
        Equations
        Instances For
          theorem Submonoid.fg_iff {M : Type u_1} [Monoid M] (P : Submonoid M) :

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

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

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

          Instances
            class AddMonoid.FG (N : Type u_2) [AddMonoid N] :

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

            Instances

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

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

              theorem AddSubmonoid.FG.map {M : Type u_1} [AddMonoid M] {M' : Type u_3} [AddMonoid M'] {P : AddSubmonoid M} (h : AddSubmonoid.FG P) (e : M →+ M') :
              theorem Submonoid.FG.map {M : Type u_1} [Monoid M] {M' : Type u_3} [Monoid M'] {P : Submonoid M} (h : Submonoid.FG P) (e : M →* M') :
              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.FG (AddSubmonoid.map e P)) :
              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.FG (Submonoid.map e P)) :
              @[simp]
              theorem Monoid.fg_iff_submonoid_fg {M : Type u_1} [Monoid M] (N : Submonoid M) :
              Monoid.FG { x // x N } Submonoid.FG N
              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) :
              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) :
              theorem AddMonoid.fg_range.proof_1 {M : Type u_1} [AddMonoid M] {M' : Type u_2} [AddMonoid M'] [AddMonoid.FG M] (f : M →+ M') :
              instance Monoid.fg_range {M : Type u_1} [Monoid M] {M' : Type u_3} [Monoid M'] [Monoid.FG M] (f : M →* M') :
              Equations

              Groups and subgroups #

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

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

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

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

                Equations
                Instances For
                  abbrev AddSubgroup.fg_iff.match_1 {G : Type u_1} [AddGroup G] (P : AddSubgroup G) (motive : AddSubgroup.FG PProp) :
                  (x : AddSubgroup.FG P) → ((S : Finset G) → (hS : AddSubgroup.closure S = P) → motive (_ : S, AddSubgroup.closure S = P)) → motive x
                  Equations
                  Instances For

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

                    abbrev AddSubgroup.fg_iff.match_2 {G : Type u_1} [AddGroup G] (P : AddSubgroup G) (motive : (S, AddSubgroup.closure S = P Set.Finite S) → Prop) :
                    (x : S, AddSubgroup.closure S = P Set.Finite S) → ((S : Set G) → (hS : AddSubgroup.closure S = P) → (hf : Set.Finite S) → motive (_ : S, AddSubgroup.closure S = P Set.Finite S)) → motive x
                    Equations
                    Instances For
                      theorem Subgroup.fg_iff {G : Type u_3} [Group G] (P : Subgroup G) :

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

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

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

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

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

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

                      Instances
                        class AddGroup.FG (H : Type u_4) [AddGroup H] :

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

                        Instances

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

                          theorem Group.fg_iff {G : Type u_3} [Group G] :

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

                          abbrev AddGroup.fg_iff'.match_1 {G : Type u_1} [AddGroup G] (motive : AddSubgroup.FG Prop) :
                          (x : AddSubgroup.FG ) → ((S : Finset G) → (hS : AddSubgroup.closure S = ) → motive (_ : S, AddSubgroup.closure S = )) → motive x
                          Equations
                          Instances For
                            abbrev AddGroup.fg_iff'.match_2 {G : Type u_1} [AddGroup G] (motive : (n S, Finset.card S = n AddSubgroup.closure S = ) → Prop) :
                            (x : n S, Finset.card S = n AddSubgroup.closure S = ) → ((_n : ) → (S : Finset G) → (_hn : Finset.card S = _n) → (hS : AddSubgroup.closure S = ) → motive (_ : n S, Finset.card S = n AddSubgroup.closure S = )) → motive x
                            Equations
                            Instances For
                              theorem Group.fg_iff' {G : Type u_3} [Group G] :

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

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

                              @[simp]
                              @[simp]
                              theorem Group.fg_iff_subgroup_fg {G : Type u_3} [Group G] (H : Subgroup G) :
                              Group.FG { x // x H } Subgroup.FG H
                              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) :
                              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) :
                              theorem AddGroup.fg_range.proof_1 {G : Type u_1} [AddGroup G] {G' : Type u_2} [AddGroup G'] [AddGroup.FG G] (f : G →+ G') :
                              instance Group.fg_range {G : Type u_3} [Group G] {G' : Type u_5} [Group G'] [Group.FG G] (f : G →* G') :
                              Equations
                              noncomputable def AddGroup.rank (G : Type u_3) [AddGroup G] [h : AddGroup.FG G] :

                              The minimum number of generators of an additive group

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

                                The minimum number of generators of a group.

                                Equations
                                Instances For
                                  theorem Group.rank_spec (G : Type u_3) [Group G] [h : Group.FG G] :
                                  theorem Group.rank_le (G : Type u_3) [Group G] [h : Group.FG G] {S : Finset G} (hS : Subgroup.closure S = ) :
                                  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) :
                                  theorem AddGroup.rank_range_le {G : Type u_3} [AddGroup G] {G' : Type u_5} [AddGroup G'] [AddGroup.FG G] {f : G →+ G'} :
                                  theorem Group.rank_range_le {G : Type u_3} [Group G] {G' : Type u_5} [Group G'] [Group.FG G] {f : G →* G'} :
                                  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') :
                                  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') :
                                  theorem AddSubgroup.rank_congr {G : Type u_3} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} [AddGroup.FG { x // x H }] [AddGroup.FG { x // x K }] (h : H = K) :
                                  AddGroup.rank { x // x H } = AddGroup.rank { x // x K }
                                  theorem Subgroup.rank_congr {G : Type u_3} [Group G] {H : Subgroup G} {K : Subgroup G} [Group.FG { x // x H }] [Group.FG { x // x K }] (h : H = K) :
                                  Group.rank { x // x H } = Group.rank { x // x K }