ModuleCat.epi_iff_surjective
theorem ModuleCat.epi_iff_surjective :
∀ {R : Type u} [inst : Ring R] {X Y : ModuleCat R} (f : X ⟶ Y), CategoryTheory.Epi f ↔ Function.Surjective ⇑f := by
sorry
The theorem `ModuleCat.epi_iff_surjective` states that for any ring `R`, and any two modules `X` and `Y` over `R`, a morphism `f` from `X` to `Y` is an epimorphism in the category of modules over `R` if and only if the function induced by `f` is surjective. In other words, `f` is an epimorphism if and only if every element in `Y` is the image of some element in `X` under `f`.
More concisely: A morphism of R-modules is an epimorphism if and only if its induced function is surjective.
|
ModuleCat.mono_iff_injective
theorem ModuleCat.mono_iff_injective :
∀ {R : Type u} [inst : Ring R] {X Y : ModuleCat R} (f : X ⟶ Y), CategoryTheory.Mono f ↔ Function.Injective ⇑f := by
sorry
The theorem `ModuleCat.mono_iff_injective` states that for any ring `R`, and for any modules `X` and `Y` over `R`, a morphism `f` from `X` to `Y` is a monomorphism in the category theory sense if and only if the function represented by `f` is injective. Here, a function is considered injective if for any two elements `a₁` and `a₂` from the domain, if the function maps `a₁` and `a₂` to the same element in the codomain, then `a₁` and `a₂` must be the same. The morphism `f` is considered a monomorphism if it has the left cancellation property; that is, for any morphisms `g`, `h` from any object to `X`, if `f` composed with `g` equals `f` composed with `h`, then `g` equals `h`.
More concisely: A morphism between modules over a ring is a monomorphism if and only if the underlying function is injective.
|