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 : Finset M), AddSubmonoid.closure S = P))motive x
      Equations
      • (_ : motive x) = (_ : motive x)
      Instances For
        abbrev AddSubmonoid.fg_iff.match_2 {M : Type u_1} [AddMonoid M] (P : AddSubmonoid M) (motive : (∃ (S : Set M), AddSubmonoid.closure S = P Set.Finite S)Prop) :
        ∀ (x : ∃ (S : Set M), AddSubmonoid.closure S = P Set.Finite S), (∀ (S : Set M) (hS : AddSubmonoid.closure S = P) (hf : Set.Finite S), motive (_ : ∃ (S : Set M), AddSubmonoid.closure S = P Set.Finite S))motive x
        Equations
        • (_ : motive x) = (_ : motive x)
        Instances For

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

          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.

              theorem Monoid.fg_iff {M : Type u_1} [Monoid M] :

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

              Equations
              instance Monoid.fg_of_finite {M : Type u_1} [Monoid M] [Finite M] :
              Equations
              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 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) :
              instance AddMonoid.fg_range {M : Type u_1} [AddMonoid M] {M' : Type u_3} [AddMonoid M'] [AddMonoid.FG M] (f : M →+ M') :
              Equations
              instance Monoid.fg_range {M : Type u_1} [Monoid M] {M' : Type u_3} [Monoid M'] [Monoid.FG M] (f : M →* M') :
              Equations
              instance Monoid.powers_fg {M : Type u_1} [Monoid M] (r : M) :
              Equations
              instance Monoid.closure_finset_fg {M : Type u_1} [Monoid M] (s : Finset M) :
              Equations
              instance Monoid.closure_finite_fg {M : Type u_1} [Monoid M] (s : Set M) [Finite s] :
              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 : Finset G), AddSubgroup.closure S = P))motive x
                  Equations
                  • (_ : motive x) = (_ : motive x)
                  Instances For
                    abbrev AddSubgroup.fg_iff.match_2 {G : Type u_1} [AddGroup G] (P : AddSubgroup G) (motive : (∃ (S : Set G), AddSubgroup.closure S = P Set.Finite S)Prop) :
                    ∀ (x : ∃ (S : Set G), AddSubgroup.closure S = P Set.Finite S), (∀ (S : Set G) (hS : AddSubgroup.closure S = P) (hf : Set.Finite S), motive (_ : ∃ (S : Set G), AddSubgroup.closure S = P Set.Finite S))motive x
                    Equations
                    • (_ : motive x) = (_ : motive x)
                    Instances For

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

                      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.

                          theorem AddGroup.fg_iff' {G : Type u_3} [AddGroup G] :
                          AddGroup.FG G ∃ (n : ) (S : Finset G), S.card = n AddSubgroup.closure S =
                          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 : Finset G), AddSubgroup.closure S = ))motive x
                          Equations
                          • (_ : motive x) = (_ : motive x)
                          Instances For
                            abbrev AddGroup.fg_iff'.match_2 {G : Type u_1} [AddGroup G] (motive : (∃ (n : ) (S : Finset G), S.card = n AddSubgroup.closure S = )Prop) :
                            ∀ (x : ∃ (n : ) (S : Finset G), S.card = n AddSubgroup.closure S = ), (∀ (_n : ) (S : Finset G) (_hn : S.card = _n) (hS : AddSubgroup.closure S = ), motive (_ : ∃ (n : ) (S : Finset G), S.card = n AddSubgroup.closure S = ))motive x
                            Equations
                            • (_ : motive x) = (_ : motive x)
                            Instances For
                              theorem Group.fg_iff' {G : Type u_3} [Group G] :
                              Group.FG G ∃ (n : ) (S : Finset G), S.card = n Subgroup.closure S =

                              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]
                              theorem Group.fg_iff_subgroup_fg {G : Type u_3} [Group G] (H : Subgroup G) :
                              Equations
                              instance AddGroup.fg_of_finite {G : Type u_3} [AddGroup G] [Finite G] :
                              Equations
                              instance Group.fg_of_finite {G : Type u_3} [Group G] [Finite G] :
                              Equations
                              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) :
                              instance AddGroup.fg_range {G : Type u_3} [AddGroup G] {G' : Type u_5} [AddGroup G'] [AddGroup.FG G] (f : G →+ G') :
                              Equations
                              instance Group.fg_range {G : Type u_3} [Group G] {G' : Type u_5} [Group G'] [Group.FG G] (f : G →* G') :
                              Equations
                              instance Group.closure_finset_fg {G : Type u_3} [Group G] (s : Finset G) :
                              Equations
                              instance Group.closure_finite_fg {G : Type u_3} [Group G] (s : Set G) [Finite s] :
                              Equations
                              theorem AddGroup.rank.proof_1 (G : Type u_1) [AddGroup G] [h : AddGroup.FG G] :
                              ∃ (n : ) (S : Finset G), S.card = n AddSubgroup.closure S =
                              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 AddGroup.rank_spec (G : Type u_3) [AddGroup G] [h : AddGroup.FG G] :
                                  ∃ (S : Finset G), S.card = AddGroup.rank G AddSubgroup.closure S =
                                  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 =
                                  theorem AddGroup.rank_le (G : Type u_3) [AddGroup G] [h : AddGroup.FG G] {S : Finset G} (hS : AddSubgroup.closure S = ) :
                                  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
                                  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 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 H] [AddGroup.FG K] (h : H = K) :
                                  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) :
                                  Equations
                                  instance QuotientGroup.fg {G : Type u_3} [Group G] [Group.FG G] (N : Subgroup G) [Subgroup.Normal N] :
                                  Equations