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] [Category.{v', u'} D] {FC : C → C → Type u_2} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {FD : D → D → Type u_3} {CD : D → Type w} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] [HasForget₂ C D] [(forget C).PreservesMonomorphisms] : (forget₂ C D).PreservesMonomorphisms

instance CategoryTheory.ConcreteCategory.forget₂_preservesEpimorphisms (C : Type u) (D : Type u') [Category.{v, u} C] [Category.{v', u'} D] {FC : C → C → Type u_2} {CC : C → Type w} [(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC] {FD : D → D → Type u_3} {CD : D → Type w} [(X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [ConcreteCategory D FD] [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] : MorphismProperty.surjective C ≤ MorphismProperty.epimorphisms C

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] : MorphismProperty.injective C ≤ MorphismProperty.monomorphisms C

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] : MorphismProperty.surjective C = MorphismProperty.epimorphisms C ↔ (forget C).PreservesEpimorphisms

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] : MorphismProperty.injective C = MorphismProperty.monomorphisms C ↔ (forget C).PreservesMonomorphisms

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] : MorphismProperty.injective C = MorphismProperty.monomorphisms C

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] : MorphismProperty.surjective C = MorphismProperty.epimorphisms C

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] : FunctorialSurjectiveInjectiveFactorizationData C

A concrete category with strong epi mono factorizations and such that the forget functor preserves mono and epi admits functorial surjective/injective factorizations.

@[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] : HasFunctorialSurjectiveInjectiveFactorization C

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)] : Mono f ↔ Function.Injective ⇑(hom f)

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)] : Epi f ↔ Function.Surjective ⇑(hom f)

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) : IsIso f ↔ Function.Bijective ⇑(hom f)

If the forgetful functor of a concrete category reflects isomorphisms, being an isomorphism is equivalent to being bijective.