Epi and mono in concrete categories #
In this file, we relate epimorphisms and monomorphisms in a concrete category C
to surjective and injective morphisms, and we show that if C has
strong epi mono factorizations and is such that forget C preserves
both epi and mono, then any morphism in C can be factored in a
functorial manner as a composition of a surjective morphism followed
by an injective morphism.
theorem
CategoryTheory.ConcreteCategory.mono_of_injective
{C : Type u}
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type w}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
{X Y : C}
(f : X ⟶ Y)
(i : Function.Injective ⇑(hom f))
:
Mono f
In any concrete category, injective morphisms are monomorphisms.
instance
CategoryTheory.ConcreteCategory.forget₂_preservesMonomorphisms
(C : Type u)
(D : Type u')
[Category.{v, u} C]
[HasForget C]
[Category.{v', u'} D]
[HasForget D]
[HasForget₂ C D]
[(forget C).PreservesMonomorphisms]
:
instance
CategoryTheory.ConcreteCategory.forget₂_preservesEpimorphisms
(C : Type u)
(D : Type u')
[Category.{v, u} C]
[HasForget C]
[Category.{v', u'} D]
[HasForget D]
[HasForget₂ C D]
[(forget C).PreservesEpimorphisms]
:
(forget₂ C D).PreservesEpimorphisms
theorem
CategoryTheory.ConcreteCategory.surjective_le_epimorphisms
(C : Type u)
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type w}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
:
theorem
CategoryTheory.ConcreteCategory.injective_le_monomorphisms
(C : Type u)
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type w}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
:
theorem
CategoryTheory.ConcreteCategory.surjective_eq_epimorphisms_iff
(C : Type u)
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type w}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
:
theorem
CategoryTheory.ConcreteCategory.injective_eq_monomorphisms_iff
(C : Type u)
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type w}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
:
theorem
CategoryTheory.ConcreteCategory.injective_eq_monomorphisms
(C : Type u)
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type w}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
[(forget C).PreservesMonomorphisms]
:
theorem
CategoryTheory.ConcreteCategory.surjective_eq_epimorphisms
(C : Type u)
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type w}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
[(forget C).PreservesEpimorphisms]
:
noncomputable def
CategoryTheory.ConcreteCategory.functorialSurjectiveInjectiveFactorizationData
(C : Type u)
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type w}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
[Limits.HasStrongEpiMonoFactorisations C]
[(forget C).PreservesMonomorphisms]
[(forget C).PreservesEpimorphisms]
:
A concrete category with strong epi mono factorizations and such that the forget functor preserves mono and epi admits functorial surjective/injective factorizations.
Equations
Instances For
@[instance 100]
instance
CategoryTheory.ConcreteCategory.instHasFunctorialSurjectiveInjectiveFactorization
(C : Type u)
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type w}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
[Limits.HasStrongEpiMonoFactorisations C]
[(forget C).PreservesMonomorphisms]
[(forget C).PreservesEpimorphisms]
:
theorem
CategoryTheory.ConcreteCategory.injective_of_mono_of_preservesPullback
{C : Type u}
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type w}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
{X Y : C}
(f : X ⟶ Y)
[Mono f]
[Limits.PreservesLimitsOfShape Limits.WalkingCospan (forget C)]
:
Function.Injective ⇑(hom f)
theorem
CategoryTheory.ConcreteCategory.mono_iff_injective_of_preservesPullback
{C : Type u}
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type w}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
{X Y : C}
(f : X ⟶ Y)
[Limits.PreservesLimitsOfShape Limits.WalkingCospan (forget C)]
:
theorem
CategoryTheory.ConcreteCategory.epi_of_surjective
{C : Type u}
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type w}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
{X Y : C}
(f : X ⟶ Y)
(s : Function.Surjective ⇑(hom f))
:
Epi f
In any concrete category, surjective morphisms are epimorphisms.
theorem
CategoryTheory.ConcreteCategory.surjective_of_epi_of_preservesPushout
{C : Type u}
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type w}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
{X Y : C}
(f : X ⟶ Y)
[Epi f]
[Limits.PreservesColimitsOfShape Limits.WalkingSpan (forget C)]
:
Function.Surjective ⇑(hom f)
theorem
CategoryTheory.ConcreteCategory.epi_iff_surjective_of_preservesPushout
{C : Type u}
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type w}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
{X Y : C}
(f : X ⟶ Y)
[Limits.PreservesColimitsOfShape Limits.WalkingSpan (forget C)]
:
theorem
CategoryTheory.ConcreteCategory.bijective_of_isIso
{C : Type u}
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type w}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
{X Y : C}
(f : X ⟶ Y)
[IsIso f]
:
Function.Bijective ⇑(hom f)
theorem
CategoryTheory.ConcreteCategory.isIso_iff_bijective
{C : Type u}
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type w}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
[(forget C).ReflectsIsomorphisms]
{X Y : C}
(f : X ⟶ Y)
:
If the forgetful functor of a concrete category reflects isomorphisms, being an isomorphism is equivalent to being bijective.