FreeGroupBasis.ext_hom
theorem FreeGroupBasis.ext_hom :
∀ {ι : Type u_1} {G : Type u_3} {H : Type u_4} [inst : Group G] [inst_1 : Group H] (b : FreeGroupBasis ι G)
(f g : G →* H), (∀ (i : ι), f (b i) = g (b i)) → f = g
This theorem states that for any two group homomorphisms `f` and `g` from a group `G` to a group `H`, if these two morphisms coincide on the elements of a basis `b` of the free group over `G`, then the two morphisms are identical. In other words, any group homomorphism is completely determined by its action on the basis elements of the free group.
More concisely: Given two group homomorphisms from a group to a group that agree on the basis elements of the free group over that group, they are equal as morphisms.
|
IsFreeGroup.ofUniqueLift
theorem IsFreeGroup.ofUniqueLift :
∀ {G : Type u} [inst : Group G] (X : Type u) (of : X → G),
(∀ {H : Type u} [inst_1 : Group H] (f : X → H), ∃! F, ∀ (a : X), F (of a) = f a) → IsFreeGroup G
This theorem states that, given a group `G` and a type `X` (with a mapping `of` from `X` to `G`), if `G` satisfies the universal property of a free group with respect to `X` (expressed as `IsFreeGroup.unique_lift`), then `G` is indeed a free group. The universal property here refers to the existence of a unique homomorphism `F` from `G` to any other group `H` that preserves the mapping from `X` to `G` and `X` to `H`.
More concisely: If a group `G` together with a mapping `of` from a type `X` to `G` satisfies the universal property of a free group (expressed as `IsFreeGroup.unique_lift`), then `G` is a free group.
|
IsFreeGroup.ofLift
theorem IsFreeGroup.ofLift :
∀ {G : Type u} [inst : Group G] (X : Type u) (of : X → G)
(lift : {H : Type u} → [inst_1 : Group H] → (X → H) ≃ (G →* H)),
(∀ {H : Type u} [inst_1 : Group H] (f : X → H) (a : X), (lift f) (of a) = f a) → IsFreeGroup G
This theorem states that if a group `G` satisfies the universal property of a free group with respect to a given type `X`, then `G` is itself a free group. The universal property in this context is expressed as it is in `IsFreeGroup.lift` and its related properties. In other words, given a group `G`, a type `X`, a function `of : X → G`, and a function `lift`, if for every group `H` and function `f : X → H`, the equation `(lift f) (of a) = f a` holds for all `a` in `X`, then `G` is a free group.
More concisely: If a group `G` satisfies the universal property of being a free group with respect to a type `X` as expressed in `IsFreeGroup.lift`, then `G` is a free group.
|
IsFreeGroup.unique_lift
theorem IsFreeGroup.unique_lift :
∀ {G : Type u_1} [inst : Group G] [inst_1 : IsFreeGroup G] {H : Type u_2} [inst_2 : Group H]
(f : IsFreeGroup.Generators G → H), ∃! F, ∀ (a : IsFreeGroup.Generators G), F (IsFreeGroup.of a) = f a
The theorem `IsFreeGroup.unique_lift` represents the universal property of a free group. For any group `G` which is a free group, and any other group `H`, if there exists a function `f` mapping the generators of `G` to `H`, there exists a unique homomorphism `F` from `G` to `H` such that for every generator `a` of `G`, the application of homomorphism `F` to the image of `a` under the canonical injection of `G`'s generators into `G` equals to the application of function `f` to `a`. It implies that the function `f` from the generators uniquely extends to this group homomorphism `F`.
More concisely: Given any group `G` that is free, any group `H`, and a function `f` mapping `G`'s generators to `H`, there exists a unique homomorphism `F` from `G` to `H` such that `F(g) = f(g)` for all generators `g` in `G`.
|
FreeGroupBasis.isFreeGroup
theorem FreeGroupBasis.isFreeGroup :
∀ {ι : Type u_1} {G : Type u_3} [inst : Group G], FreeGroupBasis ι G → IsFreeGroup G
This theorem states that for any types `ι` and `G`, given that `G` is a group, if `G` admits a free group basis indexed by `ι`, then `G` is itself a free group. In terms of abstract algebra, this means that if we can find a subset of a group that forms a free basis (i.e., each element of the group can be represented uniquely as a finite product of elements in the basis and their inverses), then the group is a free group.
More concisely: If `G` is a group with a basis indexed by `ι`, then `G` is a free group.
|