AddCommGroupCat.mono_iff_injective
theorem AddCommGroupCat.mono_iff_injective :
∀ {A B : AddCommGroupCat} (f : A ⟶ B), CategoryTheory.Mono f ↔ Function.Injective ⇑f
This theorem states that for any two objects `A` and `B` in the category of additive commutative groups (denoted `AddCommGroupCat`), a morphism `f` from `A` to `B` is a monomorphism (in categorical sense, meaning roughly that it "preserves distinctness") if and only if the function represented by `f` is injective (in the set-theoretic sense, meaning that distinct inputs lead to distinct outputs). In other words, in the category of additive commutative groups, the categorical notion of a monomorphism aligns with the set-theoretic notion of an injective function.
More concisely: In the category of additive commutative groups, a morphism is a monomorphism if and only if the represented function is injective.
|
GroupCat.SurjectiveOfEpiAuxs.tau.proof_1
theorem GroupCat.SurjectiveOfEpiAuxs.tau.proof_1 :
∀ {A B : GroupCat} (f : A ⟶ B), ∃ y, (fun x => x • ↑(MonoidHom.range f)) y = ↑(MonoidHom.range f)
The theorem `GroupCat.SurjectiveOfEpiAuxs.tau.proof_1` states that for any two groups `A` and `B`, represented as objects in the category of groups `GroupCat`, and any morphism `f` from `A` to `B` (which is a group homomorphism), there exists an element `y` such that the action of `y` on the image of `f` (which is a subgroup of `B` as stated by `MonoidHom.range f`) equals the image of `f`. In other words, there is some `y` that leaves the image of the group homomorphism invariant under the group action.
More concisely: Given any group homomorphism `f` from group `A` to group `B`, there exists an element `y` in `B` such that `y * x = f(x)` for all `x` in the image of `f`.
|
AddCommGroupCat.epi_iff_surjective
theorem AddCommGroupCat.epi_iff_surjective :
∀ {A B : AddCommGroupCat} (f : A ⟶ B), CategoryTheory.Epi f ↔ Function.Surjective ⇑f
The theorem `AddCommGroupCat.epi_iff_surjective` asserts that for all additive commutative groups `A` and `B` in the category of additive commutative groups (denoted as `AddCommGroupCat`), a morphism `f` from `A` to `B` (denoted as `A ⟶ B`) is an epimorphism if and only if it is surjective. In category theory, an epimorphism (or epi) is a morphism that is right-cancellable, meaning that if two morphisms following it are equal, then they were equal before composition with it. In set theory, a function is surjective (or onto) if for every element in the codomain there is at least one element in the domain that maps to it. Thus, in the context of additive commutative groups, this theorem is establishing an equivalence between these two seemingly different concepts.
More concisely: In the category of additive commutative groups, a morphism is an epimorphism if and only if it is surjective.
|
GroupCat.epi_iff_surjective
theorem GroupCat.epi_iff_surjective : ∀ {A B : GroupCat} (f : A ⟶ B), CategoryTheory.Epi f ↔ Function.Surjective ⇑f
This theorem states that for any two objects `A` and `B` in the category of groups, a morphism `f` from `A` to `B` is an epimorphism if and only if the underlying function of `f` is surjective. In other words, `f` is an epimorphism in the category of groups (i.e., for any two morphisms `g, h : B ⟶ C`, if `g ∘ f = h ∘ f` then `g = h`) if and only if for every element `b` in `B` there exists an element `a` in `A` such that `f(a) = b`.
More concisely: In the category of groups, a morphism is an epimorphism if and only if its underlying function is surjective.
|