Abelianization.hom_ext
theorem Abelianization.hom_ext :
∀ {G : Type u} [inst : Group G] {A : Type v} [inst_1 : Monoid A] (φ ψ : Abelianization G →* A),
φ.comp Abelianization.of = ψ.comp Abelianization.of → φ = ψ
The theorem `Abelianization.hom_ext` states that for any group `G` and any monoid `A`, if two monoid morphisms `φ` and `ψ` from the abelianization of `G` to `A` are such that their compositions with the canonical projection from `G` to its abelianization are equal, then the two morphisms `φ` and `ψ` themselves are equal. In other words, it provides a criterion for the equality of morphisms from the abelianization of a group to a monoid in terms of their compositions with the canonical projection.
More concisely: If two morphisms from the abelianization of a group to a monoid have equal compositions with the canonical projection, then they are equal.
|
commutator_eq_closure
theorem commutator_eq_closure : ∀ (G : Type u) [inst : Group G], commutator G = Subgroup.closure (commutatorSet G) := by
sorry
The theorem `commutator_eq_closure` states that for any group `G`, the commutator subgroup of `G` is equivalent to the subgroup generated by the set of all commutators in `G`. In other words, the subgroup of `G` generated by all expressions of the form `g1 * g2 * g1⁻¹ * g2⁻¹`, where `g1` and `g2` are in `G`, is precisely the same as the normal subgroup generated by the commutators of elements in `G`.
More concisely: The commutator subgroup of a group is equal to the subgroup generated by all commutators in the group.
|