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 isomorphim 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) [inst : Group G] :
Type (u+1)
  • The generators of a free group.

    Generators : Type u
  • The multiplicative equivalence between "the" free group on the generators, and the given group G. Note: IsFreeGroup.MulEquiv' should not be used directly. IsFreeGroup.MulEquiv should be used instead because it makes G an explicit variable.

    MulEquiv' : FreeGroup Generators ≃* G

IsFreeGroup G means that G isomorphic to a free group.

Instances

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

    Equations
    @[simp]
    theorem IsFreeGroup.toFreeGroup_apply (G : Type u_1) [inst : Group G] [inst : IsFreeGroup G] :

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

    Equations
    def IsFreeGroup.of {G : Type u_1} [inst : Group G] [inst : IsFreeGroup G] :

    The canonical injection of G's generators into G

    Equations
    @[simp]
    theorem IsFreeGroup.of_eq_freeGroup_of {A : Type u} :
    IsFreeGroup.of = FreeGroup.of
    def IsFreeGroup.lift {G : Type u_1} [inst : Group G] [inst : IsFreeGroup G] {H : Type u_2} [inst : Group H] :

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

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem IsFreeGroup.lift'_eq_freeGroup_lift {H : Type u_1} [inst : Group H] {A : Type u} :
    IsFreeGroup.lift = FreeGroup.lift
    @[simp]
    theorem IsFreeGroup.lift_of {G : Type u_1} [inst : Group G] [inst : IsFreeGroup G] {H : Type u_2} [inst : 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} [inst : Group G] [inst : IsFreeGroup G] {H : Type u_2} [inst : Group H] (f : G →* H) (a : IsFreeGroup.Generators G) :
    ↑(Equiv.symm IsFreeGroup.lift) f a = f (IsFreeGroup.of a)
    theorem IsFreeGroup.ext_hom {G : Type u_1} [inst : Group G] [inst : IsFreeGroup G] {H : Type u_2} [inst : 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} [inst : Group G] [inst : IsFreeGroup G] {H : Type u_2} [inst : 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 functions 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} [inst : 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.

    Equations
    • One or more equations did not get rendered due to their size.
    noncomputable def IsFreeGroup.ofUniqueLift {G : Type u} [inst : 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.

    Equations
    • One or more equations did not get rendered due to their size.
    def IsFreeGroup.ofMulEquiv {G : Type u_1} [inst : Group G] [inst : IsFreeGroup G] {H : Type u_1} [inst : Group H] (h : G ≃* H) :

    Being a free group transports across group isomorphisms.

    Equations