Documentation

Mathlib.GroupTheory.IsFreeGroup

Free groups structures on arbitrary types #

This file defines a type class for type that are free groups, together with the usual operations. The type class can be instantiated by providing an isomorphism to the canonical free group, or by proving that the universal property holds.

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

Main definitions #

Main results #

class IsFreeGroup (G : Type u) [Group G] :
Type (u + 1)

IsFreeGroup G means that G isomorphic to a free group.

Instances

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

    Instances For
      @[simp]

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

      Instances For

        The canonical injection of G's generators into G

        Instances For
          @[simp]
          theorem IsFreeGroup.of_eq_freeGroup_of {A : Type u} :
          IsFreeGroup.of = FreeGroup.of
          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.

          Instances For
            @[simp]
            theorem IsFreeGroup.lift'_eq_freeGroup_lift {H : Type u_2} [Group H] {A : Type u} :
            IsFreeGroup.lift = FreeGroup.lift
            @[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, ∀ (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.

            def 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 H inst) f) (of a) = f a) :

            If a group satisfies the universal property of a free group, then it is a free group, where the universal property is expressed as in IsFreeGroup.lift and its properties.

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

              If a group satisfies the universal property of a free group, then it is a free group, where the universal property is expressed as in IsFreeGroup.unique_lift.

              Instances For
                def IsFreeGroup.ofMulEquiv {G : Type u_1} [Group G] [IsFreeGroup G] {H : Type u_1} [Group H] (h : G ≃* H) :

                Being a free group transports across group isomorphisms.

                Instances For