Preservation and reflection of monomorphisms and epimorphisms

We provide typeclasses that state that a functor preserves or reflects monomorphisms or epimorphisms.

class CategoryTheory.Functor.PreservesMonomorphisms {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : Prop

A functor preserves monomorphisms if it maps monomorphisms to monomorphisms.

• preserves : ∀ {X Y : C} (f : X ⟶ Y) [inst : CategoryTheory.Mono f], CategoryTheory.Mono (F.map f)

  A functor preserves monomorphisms if it maps monomorphisms to monomorphisms.

theorem CategoryTheory.Functor.PreservesMonomorphisms.preserves {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D} {F : CategoryTheory.Functor C D} [self : F.PreservesMonomorphisms] {X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.Mono f], CategoryTheory.Mono (F.map f)

A functor preserves monomorphisms if it maps monomorphisms to monomorphisms.

instance CategoryTheory.Functor.map_mono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.PreservesMonomorphisms] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f] : CategoryTheory.Mono (F.map f)

Equations

• ⋯ = ⋯

class CategoryTheory.Functor.PreservesEpimorphisms {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : Prop

A functor preserves epimorphisms if it maps epimorphisms to epimorphisms.

• preserves : ∀ {X Y : C} (f : X ⟶ Y) [inst : CategoryTheory.Epi f], CategoryTheory.Epi (F.map f)

  A functor preserves epimorphisms if it maps epimorphisms to epimorphisms.

theorem CategoryTheory.Functor.PreservesEpimorphisms.preserves {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D} {F : CategoryTheory.Functor C D} [self : F.PreservesEpimorphisms] {X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.Epi f], CategoryTheory.Epi (F.map f)

A functor preserves epimorphisms if it maps epimorphisms to epimorphisms.

instance CategoryTheory.Functor.map_epi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.PreservesEpimorphisms] {X : C} {Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f] : CategoryTheory.Epi (F.map f)

Equations

• ⋯ = ⋯

class CategoryTheory.Functor.ReflectsMonomorphisms {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : Prop

A functor reflects monomorphisms if morphisms that are mapped to monomorphisms are themselves monomorphisms.

• reflects : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Mono (F.map f) → CategoryTheory.Mono f

  A functor reflects monomorphisms if morphisms that are mapped to monomorphisms are themselves monomorphisms.

theorem CategoryTheory.Functor.ReflectsMonomorphisms.reflects {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D} {F : CategoryTheory.Functor C D} [self : F.ReflectsMonomorphisms] {X Y : C} (f : X ⟶ Y), CategoryTheory.Mono (F.map f) → CategoryTheory.Mono f

A functor reflects monomorphisms if morphisms that are mapped to monomorphisms are themselves monomorphisms.

theorem CategoryTheory.Functor.mono_of_mono_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.ReflectsMonomorphisms] {X : C} {Y : C} {f : X ⟶ Y} (h : CategoryTheory.Mono (F.map f)) : CategoryTheory.Mono f

class CategoryTheory.Functor.ReflectsEpimorphisms {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) : Prop

A functor reflects epimorphisms if morphisms that are mapped to epimorphisms are themselves epimorphisms.

• reflects : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Epi (F.map f) → CategoryTheory.Epi f

  A functor reflects epimorphisms if morphisms that are mapped to epimorphisms are themselves epimorphisms.

theorem CategoryTheory.Functor.ReflectsEpimorphisms.reflects {C : Type u₁} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D} {F : CategoryTheory.Functor C D} [self : F.ReflectsEpimorphisms] {X Y : C} (f : X ⟶ Y), CategoryTheory.Epi (F.map f) → CategoryTheory.Epi f

A functor reflects epimorphisms if morphisms that are mapped to epimorphisms are themselves epimorphisms.

theorem CategoryTheory.Functor.epi_of_epi_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.ReflectsEpimorphisms] {X : C} {Y : C} {f : X ⟶ Y} (h : CategoryTheory.Epi (F.map f)) : CategoryTheory.Epi f

instance CategoryTheory.Functor.preservesMonomorphisms_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.PreservesMonomorphisms] [G.PreservesMonomorphisms] : (F.comp G).PreservesMonomorphisms

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.preservesEpimorphisms_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.PreservesEpimorphisms] [G.PreservesEpimorphisms] : (F.comp G).PreservesEpimorphisms

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.reflectsMonomorphisms_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.ReflectsMonomorphisms] [G.ReflectsMonomorphisms] : (F.comp G).ReflectsMonomorphisms

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.reflectsEpimorphisms_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.ReflectsEpimorphisms] [G.ReflectsEpimorphisms] : (F.comp G).ReflectsEpimorphisms

Equations

• ⋯ = ⋯

theorem CategoryTheory.Functor.preservesEpimorphisms_of_preserves_of_reflects {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [(F.comp G).PreservesEpimorphisms] [G.ReflectsEpimorphisms] : F.PreservesEpimorphisms

theorem CategoryTheory.Functor.preservesMonomorphisms_of_preserves_of_reflects {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [(F.comp G).PreservesMonomorphisms] [G.ReflectsMonomorphisms] : F.PreservesMonomorphisms

theorem CategoryTheory.Functor.reflectsEpimorphisms_of_preserves_of_reflects {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [G.PreservesEpimorphisms] [(F.comp G).ReflectsEpimorphisms] : F.ReflectsEpimorphisms

theorem CategoryTheory.Functor.reflectsMonomorphisms_of_preserves_of_reflects {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [G.PreservesMonomorphisms] [(F.comp G).ReflectsMonomorphisms] : F.ReflectsMonomorphisms

theorem CategoryTheory.Functor.preservesMonomorphisms.of_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} [F.PreservesMonomorphisms] (α : F ≅ G) : G.PreservesMonomorphisms

theorem CategoryTheory.Functor.preservesMonomorphisms.iso_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (α : F ≅ G) : F.PreservesMonomorphisms ↔ G.PreservesMonomorphisms

theorem CategoryTheory.Functor.preservesEpimorphisms.of_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} [F.PreservesEpimorphisms] (α : F ≅ G) : G.PreservesEpimorphisms

theorem CategoryTheory.Functor.preservesEpimorphisms.iso_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (α : F ≅ G) : F.PreservesEpimorphisms ↔ G.PreservesEpimorphisms

theorem CategoryTheory.Functor.reflectsMonomorphisms.of_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} [F.ReflectsMonomorphisms] (α : F ≅ G) : G.ReflectsMonomorphisms

theorem CategoryTheory.Functor.reflectsMonomorphisms.iso_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (α : F ≅ G) : F.ReflectsMonomorphisms ↔ G.ReflectsMonomorphisms

theorem CategoryTheory.Functor.reflectsEpimorphisms.of_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} [F.ReflectsEpimorphisms] (α : F ≅ G) : G.ReflectsEpimorphisms

theorem CategoryTheory.Functor.reflectsEpimorphisms.iso_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (α : F ≅ G) : F.ReflectsEpimorphisms ↔ G.ReflectsEpimorphisms

theorem CategoryTheory.Functor.preservesEpimorphsisms_of_adjunction {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) : F.PreservesEpimorphisms

@[instance 100]

instance CategoryTheory.Functor.preservesEpimorphisms_of_isLeftAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsLeftAdjoint] : F.PreservesEpimorphisms

Equations

• ⋯ = ⋯

theorem CategoryTheory.Functor.preservesMonomorphisms_of_adjunction {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) : G.PreservesMonomorphisms

@[instance 100]

instance CategoryTheory.Functor.preservesMonomorphisms_of_isRightAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsRightAdjoint] : F.PreservesMonomorphisms

Equations

• ⋯ = ⋯

@[instance 100]

instance CategoryTheory.Functor.reflectsMonomorphisms_of_faithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Faithful] : F.ReflectsMonomorphisms

Equations

• ⋯ = ⋯

@[instance 100]

instance CategoryTheory.Functor.reflectsEpimorphisms_of_faithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Faithful] : F.ReflectsEpimorphisms

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.Functor.splitEpiEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) [F.Full] [F.Faithful] : CategoryTheory.SplitEpi f ≃ CategoryTheory.SplitEpi (F.map f)

If F is a fully faithful functor, split epimorphisms are preserved and reflected by F.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.isSplitEpi_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) [F.Full] [F.Faithful] : CategoryTheory.IsSplitEpi (F.map f) ↔ CategoryTheory.IsSplitEpi f

noncomputable def CategoryTheory.Functor.splitMonoEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) [F.Full] [F.Faithful] : CategoryTheory.SplitMono f ≃ CategoryTheory.SplitMono (F.map f)

If F is a fully faithful functor, split monomorphisms are preserved and reflected by F.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Functor.isSplitMono_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) [F.Full] [F.Faithful] : CategoryTheory.IsSplitMono (F.map f) ↔ CategoryTheory.IsSplitMono f

@[simp]

theorem CategoryTheory.Functor.epi_map_iff_epi {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) [hF₁ : F.PreservesEpimorphisms] [hF₂ : F.ReflectsEpimorphisms] : CategoryTheory.Epi (F.map f) ↔ CategoryTheory.Epi f

@[simp]

theorem CategoryTheory.Functor.mono_map_iff_mono {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} (f : X ⟶ Y) [hF₁ : F.PreservesMonomorphisms] [hF₂ : F.ReflectsMonomorphisms] : CategoryTheory.Mono (F.map f) ↔ CategoryTheory.Mono f

theorem CategoryTheory.Functor.splitEpiCategoryImpOfIsEquivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] [CategoryTheory.SplitEpiCategory C] : CategoryTheory.SplitEpiCategory D

If F : C ⥤ D is an equivalence of categories and C is a split_epi_category, then D also is.

theorem CategoryTheory.Adjunction.strongEpi_map_of_strongEpi {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F : CategoryTheory.Functor C D} {F' : CategoryTheory.Functor D C} {A : C} {B : C} (adj : F ⊣ F') (f : A ⟶ B) [F'.PreservesMonomorphisms] [F.PreservesEpimorphisms] [CategoryTheory.StrongEpi f] : CategoryTheory.StrongEpi (F.map f)

instance CategoryTheory.Adjunction.strongEpi_map_of_isEquivalence {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F : CategoryTheory.Functor C D} {A : C} {B : C} [F.IsEquivalence] (f : A ⟶ B) [_h : CategoryTheory.StrongEpi f] : CategoryTheory.StrongEpi (F.map f)

Equations

• ⋯ = ⋯

instance CategoryTheory.Adjunction.instMonoCoeEquivHomObjHomEquivOfReflectsMonomorphisms {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F : CategoryTheory.Functor C D} {F' : CategoryTheory.Functor D C} (adj : F ⊣ F') {X : C} {Y : D} (f : F.obj X ⟶ Y) [hf : CategoryTheory.Mono f] [F.ReflectsMonomorphisms] : CategoryTheory.Mono ((adj.homEquiv X Y) f)

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.Functor.strongEpi_map_iff_strongEpi_of_isEquivalence {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] {F : CategoryTheory.Functor C D} {A : C} {B : C} (f : A ⟶ B) [F.IsEquivalence] : CategoryTheory.StrongEpi (F.map f) ↔ CategoryTheory.StrongEpi f