Documentation

Mathlib.GroupTheory.FreeGroup.IsFreeGroup

Free groups structures on arbitrary types #

This file defines the notion of free basis of a group, which induces an isomorphism between the group and the free group generated by the basis.

It also introduced a type class for groups which are free groups, i.e., for which some free basis exists.

For the explicit construction of free groups, see GroupTheory/FreeGroup.

Main definitions #

Main results #

structure FreeGroupBasis (ι : Type u_1) (G : Type u_2) [Group G] :
Type (max u_1 u_2)

A free group basis FreeGroupBasis ι G is a structure recording the isomorphism between a group G and the free group over ι. One may think of such a basis as a function from ι to G (which is registered through a FunLike instance) together with the fact that the morphism induced by this function from FreeGroup ι to G is an isomorphism.

  • ofRepr :: (
    • repr : G ≃* FreeGroup ι

      repr is the isomorphism between the group G and the free group generated by ι.

  • )
Instances For
    class IsFreeGroup (G : Type u) [Group G] :

    A group is free if it admits a free group basis. In the definition, we require the basis to be in the same universe as G, although this property follows from the existence of a basis in any universe, see FreeGroupBasis.isFreeGroup.

    Instances
      theorem IsFreeGroup.nonempty_basis {G : Type u} [Group G] [self : IsFreeGroup G] :
      ∃ (ι : Type u), Nonempty (FreeGroupBasis ι G)
      instance FreeGroupBasis.instFunLike {ι : Type u_1} {G : Type u_3} [Group G] :

      A free group basis for G over ι is associated to a map ι → G recording the images of the generators.

      Equations
      @[simp]
      theorem FreeGroupBasis.repr_apply_coe {ι : Type u_1} {G : Type u_3} [Group G] (b : FreeGroupBasis ι G) (i : ι) :
      b.repr (b i) = FreeGroup.of i

      The canonical basis of the free group over X.

      Equations
      Instances For
        def FreeGroupBasis.reindex {ι : Type u_1} {ι' : Type u_2} {G : Type u_3} [Group G] (b : FreeGroupBasis ι G) (e : ι ι') :

        Reindex a free group basis through a bijection of the indexing sets.

        Equations
        Instances For
          @[simp]
          theorem FreeGroupBasis.reindex_apply {ι : Type u_1} {ι' : Type u_2} {G : Type u_3} [Group G] (b : FreeGroupBasis ι G) (e : ι ι') (x : ι') :
          (b.reindex e) x = b (e.symm x)
          def FreeGroupBasis.map {ι : Type u_1} {G : Type u_3} {H : Type u_4} [Group G] [Group H] (b : FreeGroupBasis ι G) (e : G ≃* H) :

          Pushing a free group basis through a group isomorphism.

          Equations
          • b.map e = { repr := e.symm.trans b.repr }
          Instances For
            @[simp]
            theorem FreeGroupBasis.map_apply {ι : Type u_1} {G : Type u_3} {H : Type u_4} [Group G] [Group H] (b : FreeGroupBasis ι G) (e : G ≃* H) (x : ι) :
            (b.map e) x = e (b x)
            theorem FreeGroupBasis.injective {ι : Type u_1} {G : Type u_3} [Group G] (b : FreeGroupBasis ι G) :
            theorem FreeGroupBasis.isFreeGroup {ι : Type u_1} {G : Type u_3} [Group G] (b : FreeGroupBasis ι G) :

            A group admitting a free group basis is a free group.

            @[simp]
            theorem FreeGroupBasis.lift_symm_apply {ι : Type u_1} {G : Type u_3} {H : Type u_4} [Group G] [Group H] (b : FreeGroupBasis ι G) :
            ∀ (a : G →* H) (a_1 : ι), b.lift.symm a a_1 = a (b.repr.symm (FreeGroup.of a_1))
            @[simp]
            theorem FreeGroupBasis.lift_apply_apply {ι : Type u_1} {G : Type u_3} {H : Type u_4} [Group G] [Group H] (b : FreeGroupBasis ι G) :
            ∀ (a : ιH) (a_1 : G), (b.lift a) a_1 = (FreeGroup.lift a) (b.repr a_1)
            def FreeGroupBasis.lift {ι : Type u_1} {G : Type u_3} {H : Type u_4} [Group G] [Group H] (b : FreeGroupBasis ι G) :
            (ιH) (G →* H)

            Given a free group basis of G over ι, there is a canonical bijection between maps from ι to a group H and morphisms from G to H.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              theorem FreeGroupBasis.ext_hom {ι : Type u_1} {G : Type u_3} {H : Type u_4} [Group G] [Group H] (b : FreeGroupBasis ι G) (f : G →* H) (g : G →* H) (h : ∀ (i : ι), f (b i) = g (b i)) :
              f = g

              If two morphisms on G coincide on the elements of a basis, then they coincide.

              def FreeGroupBasis.ofLift {G : Type u} [Group G] (X : Type u) (of : XG) (lift : {H : Type u} → [inst : Group H] → (XH) (G →* H)) (lift_of : ∀ {H : Type u} [inst : Group H] (f : XH) (a : X), (lift f) (of a) = f a) :

              If a group satisfies the universal property of a free group with respect to a given type, then it admits a free group basis based on this type. Here, the universal property is expressed as in IsFreeGroup.lift and its properties.

              Equations
              • FreeGroupBasis.ofLift X of lift lift_of = { repr := ((FreeGroup.lift of).toMulEquiv (lift FreeGroup.of) ).symm }
              Instances For
                def FreeGroupBasis.ofUniqueLift {G : Type u} [Group G] (X : Type u) (of : XG) (h : ∀ {H : Type u} [inst : Group H] (f : XH), ∃! F : G →* H, ∀ (a : X), F (of a) = f a) :

                If a group satisfies the universal property of a free group with respect to a given type, then it admits a free group basis based on this type. Here the universal property is expressed as in IsFreeGroup.unique_lift.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def IsFreeGroup.Generators (G : Type u_1) [Group G] [IsFreeGroup G] :
                  Type u_1

                  A set of generators of a free group, chosen arbitrarily

                  Equations
                  Instances For
                    theorem IsFreeGroup.mulEquiv_def (G : Type u_2) [Group G] [IsFreeGroup G] :
                    IsFreeGroup.mulEquiv G = .some.repr.symm
                    @[irreducible]

                    Any free group is isomorphic to "the" free group.

                    Equations
                    Instances For

                      A free group basis of a free group G, over the set Generators G.

                      Equations
                      Instances For
                        @[simp]
                        theorem IsFreeGroup.toFreeGroup_apply (G : Type u_1) [Group G] [IsFreeGroup G] :
                        ∀ (a : G), (IsFreeGroup.toFreeGroup G) a = (IsFreeGroup.mulEquiv G).symm a

                        Any free group is isomorphic to "the" free group.

                        Equations
                        Instances For

                          The canonical injection of G's generators into G

                          Equations
                          Instances For
                            def IsFreeGroup.lift {G : Type u_1} [Group G] [IsFreeGroup G] {H : Type u_2} [Group H] :

                            The equivalence between functions on the generators and group homomorphisms from a free group given by those generators.

                            Equations
                            Instances For
                              @[simp]
                              theorem IsFreeGroup.lift_of {G : Type u_1} [Group G] [IsFreeGroup G] {H : Type u_2} [Group H] (f : IsFreeGroup.Generators GH) (a : IsFreeGroup.Generators G) :
                              (IsFreeGroup.lift f) (IsFreeGroup.of a) = f a
                              @[simp]
                              theorem IsFreeGroup.lift_symm_apply {G : Type u_1} [Group G] [IsFreeGroup G] {H : Type u_2} [Group H] (f : G →* H) (a : IsFreeGroup.Generators G) :
                              IsFreeGroup.lift.symm f a = f (IsFreeGroup.of a)
                              theorem IsFreeGroup.ext_hom {G : Type u_1} [Group G] [IsFreeGroup G] {H : Type u_2} [Group H] ⦃f : G →* H ⦃g : G →* H (h : ∀ (a : IsFreeGroup.Generators G), f (IsFreeGroup.of a) = g (IsFreeGroup.of a)) :
                              f = g
                              theorem IsFreeGroup.unique_lift {G : Type u_1} [Group G] [IsFreeGroup G] {H : Type u_2} [Group H] (f : IsFreeGroup.Generators GH) :
                              ∃! F : G →* H, ∀ (a : IsFreeGroup.Generators G), F (IsFreeGroup.of a) = f a

                              The universal property of a free group: A function from the generators of G to another group extends in a unique way to a homomorphism from G.

                              Note that since IsFreeGroup.lift is expressed as a bijection, it already expresses the universal property.

                              theorem IsFreeGroup.ofLift {G : Type u} [Group G] (X : Type u) (of : XG) (lift : {H : Type u} → [inst : Group H] → (XH) (G →* H)) (lift_of : ∀ {H : Type u} [inst : Group H] (f : XH) (a : X), (lift f) (of a) = f a) :

                              If a group satisfies the universal property of a free group with respect to a given type, then it is free. Here, the universal property is expressed as in IsFreeGroup.lift and its properties.

                              theorem IsFreeGroup.ofUniqueLift {G : Type u} [Group G] (X : Type u) (of : XG) (h : ∀ {H : Type u} [inst : Group H] (f : XH), ∃! F : G →* H, ∀ (a : X), F (of a) = f a) :

                              If a group satisfies the universal property of a free group with respect to a given type, then it is free. Here the universal property is expressed as in IsFreeGroup.unique_lift.

                              theorem IsFreeGroup.ofMulEquiv {G : Type u_1} [Group G] [IsFreeGroup G] {H : Type u_2} [Group H] (e : G ≃* H) :