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} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] {X : C} {Y : C} (f : X ⟶ Y) (i : Function.Injective ⇑f) : CategoryTheory.Mono f

In any concrete category, injective morphisms are monomorphisms.

instance CategoryTheory.ConcreteCategory.forget₂_preservesMonomorphisms (C : Type u) (D : Type u') [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Category.{v', u'} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.HasForget₂ C D] [(CategoryTheory.forget C).PreservesMonomorphisms] : (CategoryTheory.forget₂ C D).PreservesMonomorphisms

Equations

• ⋯ = ⋯

instance CategoryTheory.ConcreteCategory.forget₂_preservesEpimorphisms (C : Type u) (D : Type u') [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Category.{v', u'} D] [CategoryTheory.ConcreteCategory D] [CategoryTheory.HasForget₂ C D] [(CategoryTheory.forget C).PreservesEpimorphisms] : (CategoryTheory.forget₂ C D).PreservesEpimorphisms

Equations

• ⋯ = ⋯

theorem CategoryTheory.ConcreteCategory.surjective_le_epimorphisms (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] : CategoryTheory.MorphismProperty.surjective C ≤ CategoryTheory.MorphismProperty.epimorphisms C

theorem CategoryTheory.ConcreteCategory.injective_le_monomorphisms (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] : CategoryTheory.MorphismProperty.injective C ≤ CategoryTheory.MorphismProperty.monomorphisms C

theorem CategoryTheory.ConcreteCategory.surjective_eq_epimorphisms_iff (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] : CategoryTheory.MorphismProperty.surjective C = CategoryTheory.MorphismProperty.epimorphisms C ↔ (CategoryTheory.forget C).PreservesEpimorphisms

theorem CategoryTheory.ConcreteCategory.injective_eq_monomorphisms_iff (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] : CategoryTheory.MorphismProperty.injective C = CategoryTheory.MorphismProperty.monomorphisms C ↔ (CategoryTheory.forget C).PreservesMonomorphisms

theorem CategoryTheory.ConcreteCategory.injective_eq_monomorphisms (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] [(CategoryTheory.forget C).PreservesMonomorphisms] : CategoryTheory.MorphismProperty.injective C = CategoryTheory.MorphismProperty.monomorphisms C

theorem CategoryTheory.ConcreteCategory.surjective_eq_epimorphisms (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] [(CategoryTheory.forget C).PreservesEpimorphisms] : CategoryTheory.MorphismProperty.surjective C = CategoryTheory.MorphismProperty.epimorphisms C

noncomputable def CategoryTheory.ConcreteCategory.functorialSurjectiveInjectiveFactorizationData (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] [(CategoryTheory.forget C).PreservesMonomorphisms] [(CategoryTheory.forget C).PreservesEpimorphisms] : CategoryTheory.ConcreteCategory.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.

Equations

• CategoryTheory.ConcreteCategory.functorialSurjectiveInjectiveFactorizationData C = (CategoryTheory.Limits.functorialEpiMonoFactorizationData C).ofLE ⋯ ⋯

@[instance 100]

instance CategoryTheory.ConcreteCategory.instHasFunctorialSurjectiveInjectiveFactorization (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] [(CategoryTheory.forget C).PreservesMonomorphisms] [(CategoryTheory.forget C).PreservesEpimorphisms] : CategoryTheory.ConcreteCategory.HasFunctorialSurjectiveInjectiveFactorization C

Equations

• ⋯ = ⋯

theorem CategoryTheory.ConcreteCategory.injective_of_mono_of_preservesPullback {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan (CategoryTheory.forget C)] : Function.Injective ⇑f

theorem CategoryTheory.ConcreteCategory.mono_iff_injective_of_preservesPullback {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan (CategoryTheory.forget C)] : CategoryTheory.Mono f ↔ Function.Injective ⇑f

theorem CategoryTheory.ConcreteCategory.epi_of_surjective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] {X : C} {Y : C} (f : X ⟶ Y) (s : Function.Surjective ⇑f) : CategoryTheory.Epi f

In any concrete category, surjective morphisms are epimorphisms.

theorem CategoryTheory.ConcreteCategory.surjective_of_epi_of_preservesPushout {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f] [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan (CategoryTheory.forget C)] : Function.Surjective ⇑f

theorem CategoryTheory.ConcreteCategory.epi_iff_surjective_of_preservesPushout {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan (CategoryTheory.forget C)] : CategoryTheory.Epi f ↔ Function.Surjective ⇑f

theorem CategoryTheory.ConcreteCategory.bijective_of_isIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.IsIso f] : Function.Bijective ((CategoryTheory.forget C).map f)

theorem CategoryTheory.ConcreteCategory.isIso_iff_bijective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ConcreteCategory C] [(CategoryTheory.forget C).ReflectsIsomorphisms] {X : C} {Y : C} (f : X ⟶ Y) : CategoryTheory.IsIso f ↔ Function.Bijective ((CategoryTheory.forget C).map f)

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