Mathlib.CategoryTheory.Functor.EpiMono

CategoryTheory.Functor.PreservesMonomorphisms structure

(F : C ⥤ D)

Full source

/-- A functor preserves monomorphisms if it maps monomorphisms to monomorphisms. -/
class PreservesMonomorphisms (F : C ⥤ D) : Prop where
  /-- A functor preserves monomorphisms if it maps monomorphisms to monomorphisms. -/
  preserves : ∀ {X Y : C} (f : X ⟶ Y) [Mono f], Mono (F.map f)

Functor preserving monomorphisms

Informal description

A functor $ F \colon C \to D $ between categories is said to *preserve monomorphisms* if for every monomorphism $ f \colon X \to Y $ in $ C $, the morphism $ F(f) \colon F(X) \to F(Y) $ is a monomorphism in $ D $.

CategoryTheory.Functor.map_mono instance

(F : C ⥤ D) [PreservesMonomorphisms F] {X Y : C} (f : X ⟶ Y) [Mono f] : Mono (F.map f)

Full source

instance map_mono (F : C ⥤ D) [PreservesMonomorphisms F] {X Y : C} (f : X ⟶ Y) [Mono f] :
    Mono (F.map f) :=
  PreservesMonomorphisms.preserves f

Image of a Monomorphism under a Functor Preserving Monomorphisms

Informal description

For any functor $F \colon C \to D$ that preserves monomorphisms and any monomorphism $f \colon X \to Y$ in $C$, the morphism $F(f) \colon F(X) \to F(Y)$ is a monomorphism in $D$.

CategoryTheory.Functor.PreservesEpimorphisms structure

(F : C ⥤ D)

Full source

/-- A functor preserves epimorphisms if it maps epimorphisms to epimorphisms. -/
class PreservesEpimorphisms (F : C ⥤ D) : Prop where
  /-- A functor preserves epimorphisms if it maps epimorphisms to epimorphisms. -/
  preserves : ∀ {X Y : C} (f : X ⟶ Y) [Epi f], Epi (F.map f)

Functor preserving epimorphisms

Informal description

A functor $ F \colon C \to D $ between categories is said to *preserve epimorphisms* if for every epimorphism $ f \colon X \to Y $ in $ C $, the morphism $ F(f) \colon F(X) \to F(Y) $ is an epimorphism in $ D $.

CategoryTheory.Functor.map_epi instance

(F : C ⥤ D) [PreservesEpimorphisms F] {X Y : C} (f : X ⟶ Y) [Epi f] : Epi (F.map f)

Full source

instance map_epi (F : C ⥤ D) [PreservesEpimorphisms F] {X Y : C} (f : X ⟶ Y) [Epi f] :
    Epi (F.map f) :=
  PreservesEpimorphisms.preserves f

Image of an Epimorphism under a Functor Preserving Epimorphisms

Informal description

For any functor $F \colon C \to D$ that preserves epimorphisms and any epimorphism $f \colon X \to Y$ in $C$, the morphism $F(f) \colon F(X) \to F(Y)$ is an epimorphism in $D$.

CategoryTheory.Functor.ReflectsMonomorphisms structure

(F : C ⥤ D)

Full source

/-- A functor reflects monomorphisms if morphisms that are mapped to monomorphisms are themselves
    monomorphisms. -/
class ReflectsMonomorphisms (F : C ⥤ D) : Prop where
   /-- A functor reflects monomorphisms if morphisms that are mapped to monomorphisms are themselves
    monomorphisms. -/
  reflects : ∀ {X Y : C} (f : X ⟶ Y), Mono (F.map f) → Mono f

Functor that reflects monomorphisms

Informal description

A functor $ F : C \to D $ between categories reflects monomorphisms if for any morphism $ f $ in $ C $, whenever $ F(f) $ is a monomorphism in $ D $, then $ f $ is a monomorphism in $ C $.

CategoryTheory.Functor.mono_of_mono_map theorem

(F : C ⥤ D) [ReflectsMonomorphisms F] {X Y : C} {f : X ⟶ Y} (h : Mono (F.map f)) : Mono f

Full source

theorem mono_of_mono_map (F : C ⥤ D) [ReflectsMonomorphisms F] {X Y : C} {f : X ⟶ Y}
    (h : Mono (F.map f)) : Mono f :=
  ReflectsMonomorphisms.reflects f h

Reflection of Monomorphisms by a Functor

Informal description

Let $F \colon C \to D$ be a functor between categories that reflects monomorphisms. For any morphism $f \colon X \to Y$ in $C$, if $F(f)$ is a monomorphism in $D$, then $f$ is a monomorphism in $C$.

CategoryTheory.Functor.ReflectsEpimorphisms structure

(F : C ⥤ D)

Full source

/-- A functor reflects epimorphisms if morphisms that are mapped to epimorphisms are themselves
    epimorphisms. -/
class ReflectsEpimorphisms (F : C ⥤ D) : Prop where
  /-- A functor reflects epimorphisms if morphisms that are mapped to epimorphisms are themselves
      epimorphisms. -/
  reflects : ∀ {X Y : C} (f : X ⟶ Y), Epi (F.map f) → Epi f

Functor that reflects epimorphisms

Informal description

A functor $ F : C \to D $ between categories reflects epimorphisms if for any morphism $ f $ in $ C $, whenever $ F(f) $ is an epimorphism in $ D $, then $ f $ is an epimorphism in $ C $.

CategoryTheory.Functor.epi_of_epi_map theorem

(F : C ⥤ D) [ReflectsEpimorphisms F] {X Y : C} {f : X ⟶ Y} (h : Epi (F.map f)) : Epi f

Full source

theorem epi_of_epi_map (F : C ⥤ D) [ReflectsEpimorphisms F] {X Y : C} {f : X ⟶ Y}
    (h : Epi (F.map f)) : Epi f :=
  ReflectsEpimorphisms.reflects f h

Reflection of Epimorphisms by a Functor

Informal description

Let $ F \colon C \to D $ be a functor between categories that reflects epimorphisms. For any morphism $ f \colon X \to Y $ in $ C $, if $ F(f) $ is an epimorphism in $ D $, then $ f $ is an epimorphism in $ C $.

CategoryTheory.Functor.preservesMonomorphisms_comp instance

(F : C ⥤ D) (G : D ⥤ E) [PreservesMonomorphisms F] [PreservesMonomorphisms G] : PreservesMonomorphisms (F ⋙ G)

Full source

instance preservesMonomorphisms_comp (F : C ⥤ D) (G : D ⥤ E) [PreservesMonomorphisms F]
    [PreservesMonomorphisms G] : PreservesMonomorphisms (F ⋙ G) where
  preserves f h := by
    rw [comp_map]
    exact inferInstance

Composition of Monomorphism-Preserving Functors Preserves Monomorphisms

Informal description

For any functors $F \colon C \to D$ and $G \colon D \to E$ between categories, if both $F$ and $G$ preserve monomorphisms, then their composition $F \circ G$ also preserves monomorphisms.

CategoryTheory.Functor.preservesEpimorphisms_comp instance

(F : C ⥤ D) (G : D ⥤ E) [PreservesEpimorphisms F] [PreservesEpimorphisms G] : PreservesEpimorphisms (F ⋙ G)

Full source

instance preservesEpimorphisms_comp (F : C ⥤ D) (G : D ⥤ E) [PreservesEpimorphisms F]
    [PreservesEpimorphisms G] : PreservesEpimorphisms (F ⋙ G) where
  preserves f h := by
    rw [comp_map]
    exact inferInstance

Composition of Epimorphism-Preserving Functors Preserves Epimorphisms

Informal description

For any functors $F \colon C \to D$ and $G \colon D \to E$ between categories, if both $F$ and $G$ preserve epimorphisms, then their composition $F \circ G$ also preserves epimorphisms.

CategoryTheory.Functor.reflectsMonomorphisms_comp instance

(F : C ⥤ D) (G : D ⥤ E) [ReflectsMonomorphisms F] [ReflectsMonomorphisms G] : ReflectsMonomorphisms (F ⋙ G)

Full source

instance reflectsMonomorphisms_comp (F : C ⥤ D) (G : D ⥤ E) [ReflectsMonomorphisms F]
    [ReflectsMonomorphisms G] : ReflectsMonomorphisms (F ⋙ G) where
  reflects _ h := F.mono_of_mono_map (G.mono_of_mono_map h)

Composition of Monomorphism-Reflecting Functors Reflects Monomorphisms

Informal description

For any functors $F \colon C \to D$ and $G \colon D \to E$ between categories, if both $F$ and $G$ reflect monomorphisms, then their composition $F \circ G$ also reflects monomorphisms.

CategoryTheory.Functor.reflectsEpimorphisms_comp instance

(F : C ⥤ D) (G : D ⥤ E) [ReflectsEpimorphisms F] [ReflectsEpimorphisms G] : ReflectsEpimorphisms (F ⋙ G)

Full source

instance reflectsEpimorphisms_comp (F : C ⥤ D) (G : D ⥤ E) [ReflectsEpimorphisms F]
    [ReflectsEpimorphisms G] : ReflectsEpimorphisms (F ⋙ G) where
  reflects _ h := F.epi_of_epi_map (G.epi_of_epi_map h)

Composition of Epimorphism-Reflecting Functors Reflects Epimorphisms

Informal description

For any functors $F \colon C \to D$ and $G \colon D \to E$ between categories, if both $F$ and $G$ reflect epimorphisms, then their composition $F \circ G$ also reflects epimorphisms.

CategoryTheory.Functor.preservesEpimorphisms_of_preserves_of_reflects theorem

(F : C ⥤ D) (G : D ⥤ E) [PreservesEpimorphisms (F ⋙ G)] [ReflectsEpimorphisms G] : PreservesEpimorphisms F

Full source

theorem preservesEpimorphisms_of_preserves_of_reflects (F : C ⥤ D) (G : D ⥤ E)
    [PreservesEpimorphisms (F ⋙ G)] [ReflectsEpimorphisms G] : PreservesEpimorphisms F :=
  ⟨fun f _ => G.epi_of_epi_map <| show Epi ((F ⋙ G).map f) from inferInstance⟩

Preservation of Epimorphisms via Composition and Reflection

Informal description

Let $F \colon C \to D$ and $G \colon D \to E$ be functors between categories. If the composition $F \circ G$ preserves epimorphisms and $G$ reflects epimorphisms, then $F$ preserves epimorphisms.

CategoryTheory.Functor.preservesMonomorphisms_of_preserves_of_reflects theorem

(F : C ⥤ D) (G : D ⥤ E) [PreservesMonomorphisms (F ⋙ G)] [ReflectsMonomorphisms G] : PreservesMonomorphisms F

Full source

theorem preservesMonomorphisms_of_preserves_of_reflects (F : C ⥤ D) (G : D ⥤ E)
    [PreservesMonomorphisms (F ⋙ G)] [ReflectsMonomorphisms G] : PreservesMonomorphisms F :=
  ⟨fun f _ => G.mono_of_mono_map <| show Mono ((F ⋙ G).map f) from inferInstance⟩

Preservation of Monomorphisms via Composition and Reflection

Informal description

Let $F \colon C \to D$ and $G \colon D \to E$ be functors between categories. If the composition $F \circ G$ preserves monomorphisms and $G$ reflects monomorphisms, then $F$ preserves monomorphisms.

CategoryTheory.Functor.reflectsEpimorphisms_of_preserves_of_reflects theorem

(F : C ⥤ D) (G : D ⥤ E) [PreservesEpimorphisms G] [ReflectsEpimorphisms (F ⋙ G)] : ReflectsEpimorphisms F

Full source

theorem reflectsEpimorphisms_of_preserves_of_reflects (F : C ⥤ D) (G : D ⥤ E)
    [PreservesEpimorphisms G] [ReflectsEpimorphisms (F ⋙ G)] : ReflectsEpimorphisms F :=
  ⟨fun f _ => (F ⋙ G).epi_of_epi_map <| show Epi (G.map (F.map f)) from inferInstance⟩

Reflection of Epimorphisms via Preservation and Composition

Informal description

Let $F \colon C \to D$ and $G \colon D \to E$ be functors between categories. If $G$ preserves epimorphisms and the composition $F \circ G$ reflects epimorphisms, then $F$ reflects epimorphisms.

CategoryTheory.Functor.reflectsMonomorphisms_of_preserves_of_reflects theorem

(F : C ⥤ D) (G : D ⥤ E) [PreservesMonomorphisms G] [ReflectsMonomorphisms (F ⋙ G)] : ReflectsMonomorphisms F

Full source

theorem reflectsMonomorphisms_of_preserves_of_reflects (F : C ⥤ D) (G : D ⥤ E)
    [PreservesMonomorphisms G] [ReflectsMonomorphisms (F ⋙ G)] : ReflectsMonomorphisms F :=
  ⟨fun f _ => (F ⋙ G).mono_of_mono_map <| show Mono (G.map (F.map f)) from inferInstance⟩

Reflection of Monomorphisms via Composition of Functors

Informal description

Let $F \colon C \to D$ and $G \colon D \to E$ be functors between categories. If $G$ preserves monomorphisms and the composition $F \circ G$ reflects monomorphisms, then $F$ reflects monomorphisms.

CategoryTheory.Functor.preservesMonomorphisms.of_iso theorem

{F G : C ⥤ D} [PreservesMonomorphisms F] (α : F ≅ G) : PreservesMonomorphisms G

Full source

theorem preservesMonomorphisms.of_iso {F G : C ⥤ D} [PreservesMonomorphisms F] (α : F ≅ G) :
    PreservesMonomorphisms G :=
  { preserves := fun {X} {Y} f h => by
      suffices G.map f = (α.app X).inv ≫ F.map f ≫ (α.app Y).hom from this ▸ mono_comp _ _
      rw [Iso.eq_inv_comp, Iso.app_hom, Iso.app_hom, NatTrans.naturality] }

Preservation of Monomorphisms under Natural Isomorphism

Informal description

Let $F, G \colon C \to D$ be naturally isomorphic functors between categories. If $F$ preserves monomorphisms, then $G$ also preserves monomorphisms.

CategoryTheory.Functor.preservesMonomorphisms.iso_iff theorem

{F G : C ⥤ D} (α : F ≅ G) : PreservesMonomorphisms F ↔ PreservesMonomorphisms G

Full source

theorem preservesMonomorphisms.iso_iff {F G : C ⥤ D} (α : F ≅ G) :
    PreservesMonomorphismsPreservesMonomorphisms F ↔ PreservesMonomorphisms G :=
  ⟨fun _ => preservesMonomorphisms.of_iso α, fun _ => preservesMonomorphisms.of_iso α.symm⟩

Preservation of Monomorphisms is Invariant under Natural Isomorphism

Informal description

Let $F, G \colon C \to D$ be naturally isomorphic functors between categories. Then $F$ preserves monomorphisms if and only if $G$ preserves monomorphisms.

CategoryTheory.Functor.preservesEpimorphisms.of_iso theorem

{F G : C ⥤ D} [PreservesEpimorphisms F] (α : F ≅ G) : PreservesEpimorphisms G

Full source

theorem preservesEpimorphisms.of_iso {F G : C ⥤ D} [PreservesEpimorphisms F] (α : F ≅ G) :
    PreservesEpimorphisms G :=
  { preserves := fun {X} {Y} f h => by
      suffices G.map f = (α.app X).inv ≫ F.map f ≫ (α.app Y).hom from this ▸ epi_comp _ _
      rw [Iso.eq_inv_comp, Iso.app_hom, Iso.app_hom, NatTrans.naturality] }

Preservation of Epimorphisms under Natural Isomorphism

Informal description

Given two functors $F, G \colon C \to D$ and a natural isomorphism $\alpha \colon F \cong G$, if $F$ preserves epimorphisms, then $G$ also preserves epimorphisms.

CategoryTheory.Functor.preservesEpimorphisms.iso_iff theorem

{F G : C ⥤ D} (α : F ≅ G) : PreservesEpimorphisms F ↔ PreservesEpimorphisms G

Full source

theorem preservesEpimorphisms.iso_iff {F G : C ⥤ D} (α : F ≅ G) :
    PreservesEpimorphismsPreservesEpimorphisms F ↔ PreservesEpimorphisms G :=
  ⟨fun _ => preservesEpimorphisms.of_iso α, fun _ => preservesEpimorphisms.of_iso α.symm⟩

Preservation of Epimorphisms is Equivalent under Natural Isomorphism

Informal description

For any two functors $F, G \colon C \to D$ and a natural isomorphism $\alpha \colon F \cong G$, the functor $F$ preserves epimorphisms if and only if $G$ preserves epimorphisms.

CategoryTheory.Functor.reflectsMonomorphisms.of_iso theorem

{F G : C ⥤ D} [ReflectsMonomorphisms F] (α : F ≅ G) : ReflectsMonomorphisms G

Full source

theorem reflectsMonomorphisms.of_iso {F G : C ⥤ D} [ReflectsMonomorphisms F] (α : F ≅ G) :
    ReflectsMonomorphisms G :=
  { reflects := fun {X} {Y} f h => by
      apply F.mono_of_mono_map
      suffices F.map f = (α.app X).hom ≫ G.map f ≫ (α.app Y).inv from this ▸ mono_comp _ _
      rw [← Category.assoc, Iso.eq_comp_inv, Iso.app_hom, Iso.app_hom, NatTrans.naturality] }

Reflection of Monomorphisms is Preserved under Natural Isomorphism

Informal description

Let $F, G \colon C \to D$ be functors between categories, with $F$ reflecting monomorphisms. If there exists a natural isomorphism $\alpha \colon F \cong G$, then $G$ also reflects monomorphisms.

CategoryTheory.Functor.reflectsMonomorphisms.iso_iff theorem

{F G : C ⥤ D} (α : F ≅ G) : ReflectsMonomorphisms F ↔ ReflectsMonomorphisms G

Full source

theorem reflectsMonomorphisms.iso_iff {F G : C ⥤ D} (α : F ≅ G) :
    ReflectsMonomorphismsReflectsMonomorphisms F ↔ ReflectsMonomorphisms G :=
  ⟨fun _ => reflectsMonomorphisms.of_iso α, fun _ => reflectsMonomorphisms.of_iso α.symm⟩

Reflection of Monomorphisms is Invariant under Natural Isomorphism

Informal description

For any two functors $F, G \colon C \to D$ and a natural isomorphism $\alpha \colon F \cong G$, the functor $F$ reflects monomorphisms if and only if $G$ reflects monomorphisms.

CategoryTheory.Functor.reflectsEpimorphisms.of_iso theorem

{F G : C ⥤ D} [ReflectsEpimorphisms F] (α : F ≅ G) : ReflectsEpimorphisms G

Full source

theorem reflectsEpimorphisms.of_iso {F G : C ⥤ D} [ReflectsEpimorphisms F] (α : F ≅ G) :
    ReflectsEpimorphisms G :=
  { reflects := fun {X} {Y} f h => by
      apply F.epi_of_epi_map
      suffices F.map f = (α.app X).hom ≫ G.map f ≫ (α.app Y).inv from this ▸ epi_comp _ _
      rw [← Category.assoc, Iso.eq_comp_inv, Iso.app_hom, Iso.app_hom, NatTrans.naturality] }

Reflection of Epimorphisms is Preserved by Natural Isomorphism

Informal description

Let $F, G \colon C \to D$ be functors between categories, and let $\alpha \colon F \cong G$ be a natural isomorphism. If $F$ reflects epimorphisms, then $G$ also reflects epimorphisms.

CategoryTheory.Functor.reflectsEpimorphisms.iso_iff theorem

{F G : C ⥤ D} (α : F ≅ G) : ReflectsEpimorphisms F ↔ ReflectsEpimorphisms G

Full source

theorem reflectsEpimorphisms.iso_iff {F G : C ⥤ D} (α : F ≅ G) :
    ReflectsEpimorphismsReflectsEpimorphisms F ↔ ReflectsEpimorphisms G :=
  ⟨fun _ => reflectsEpimorphisms.of_iso α, fun _ => reflectsEpimorphisms.of_iso α.symm⟩

Reflection of Epimorphisms is Invariant under Natural Isomorphism

Informal description

For any two functors $F, G \colon C \to D$ and a natural isomorphism $\alpha \colon F \cong G$, the functor $F$ reflects epimorphisms if and only if $G$ reflects epimorphisms.

CategoryTheory.Functor.preservesEpimorphsisms_of_adjunction theorem

{F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) : PreservesEpimorphisms F

Full source

theorem preservesEpimorphsisms_of_adjunction {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) :
    PreservesEpimorphisms F :=
  { preserves := fun {X} {Y} f hf =>
      ⟨by
        intro Z g h H
        replace H := congr_arg (adj.homEquiv X Z) H
        rwa [adj.homEquiv_naturality_left, adj.homEquiv_naturality_left, cancel_epi,
          Equiv.apply_eq_iff_eq] at H⟩ }

Left Adjoints Preserve Epimorphisms

Informal description

Given an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, the left adjoint $F$ preserves epimorphisms. That is, for any epimorphism $f \colon X \to Y$ in $C$, the morphism $F(f) \colon F(X) \to F(Y)$ is an epimorphism in $D$.

CategoryTheory.Functor.preservesEpimorphisms_of_isLeftAdjoint instance

(F : C ⥤ D) [IsLeftAdjoint F] : PreservesEpimorphisms F

Full source

instance (priority := 100) preservesEpimorphisms_of_isLeftAdjoint (F : C ⥤ D) [IsLeftAdjoint F] :
    PreservesEpimorphisms F :=
  preservesEpimorphsisms_of_adjunction (Adjunction.ofIsLeftAdjoint F)

Left Adjoint Functors Preserve Epimorphisms

Informal description

Every left adjoint functor $F \colon C \to D$ preserves epimorphisms. That is, for any epimorphism $f \colon X \to Y$ in $C$, the morphism $F(f) \colon F(X) \to F(Y)$ is an epimorphism in $D$.

CategoryTheory.Functor.preservesMonomorphisms_of_adjunction theorem

{F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) : PreservesMonomorphisms G

Full source

theorem preservesMonomorphisms_of_adjunction {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) :
    PreservesMonomorphisms G :=
  { preserves := fun {X} {Y} f hf =>
      ⟨by
        intro Z g h H
        replace H := congr_arg (adj.homEquiv Z Y).symm H
        rwa [adj.homEquiv_naturality_right_symm, adj.homEquiv_naturality_right_symm, cancel_mono,
          Equiv.apply_eq_iff_eq] at H⟩ }

Right Adjoints Preserve Monomorphisms

Informal description

Given an adjunction $F \dashv G$ between functors $F \colon C \to D$ and $G \colon D \to C$, the right adjoint $G$ preserves monomorphisms. That is, for any monomorphism $f \colon X \to Y$ in $D$, the morphism $G(f) \colon G(X) \to G(Y)$ is a monomorphism in $C$.

CategoryTheory.Functor.preservesMonomorphisms_of_isRightAdjoint instance

(F : C ⥤ D) [IsRightAdjoint F] : PreservesMonomorphisms F

Full source

instance (priority := 100) preservesMonomorphisms_of_isRightAdjoint (F : C ⥤ D) [IsRightAdjoint F] :
    PreservesMonomorphisms F :=
  preservesMonomorphisms_of_adjunction (Adjunction.ofIsRightAdjoint F)

Right Adjoint Functors Preserve Monomorphisms

Informal description

Every right adjoint functor $F \colon C \to D$ preserves monomorphisms. That is, for any monomorphism $f \colon X \to Y$ in $C$, the morphism $F(f) \colon F(X) \to F(Y)$ is a monomorphism in $D$.

CategoryTheory.Functor.reflectsMonomorphisms_of_faithful instance

(F : C ⥤ D) [Faithful F] : ReflectsMonomorphisms F

Full source

instance (priority := 100) reflectsMonomorphisms_of_faithful (F : C ⥤ D) [Faithful F] :
    ReflectsMonomorphisms F where
  reflects {X} {Y} f _ :=
    ⟨fun {Z} g h hgh =>
      F.map_injective ((cancel_mono (F.map f)).1 (by rw [← F.map_comp, hgh, F.map_comp]))⟩

Faithful Functors Reflect Monomorphisms

Informal description

For any faithful functor $F \colon C \to D$ between categories $C$ and $D$, $F$ reflects monomorphisms. That is, if $F(f)$ is a monomorphism in $D$ for some morphism $f$ in $C$, then $f$ is a monomorphism in $C$.

CategoryTheory.Functor.reflectsEpimorphisms_of_faithful instance

(F : C ⥤ D) [Faithful F] : ReflectsEpimorphisms F

Full source

instance (priority := 100) reflectsEpimorphisms_of_faithful (F : C ⥤ D) [Faithful F] :
    ReflectsEpimorphisms F where
  reflects {X} {Y} f _ :=
    ⟨fun {Z} g h hgh =>
      F.map_injective ((cancel_epi (F.map f)).1 (by rw [← F.map_comp, hgh, F.map_comp]))⟩

Faithful Functors Reflect Epimorphisms

Informal description

For any faithful functor $F \colon C \to D$ between categories $C$ and $D$, $F$ reflects epimorphisms. That is, if $F(f)$ is an epimorphism in $D$ for some morphism $f$ in $C$, then $f$ is an epimorphism in $C$.

CategoryTheory.Functor.splitEpiEquiv definition

[Full F] [Faithful F] : SplitEpi f ≃ SplitEpi (F.map f)

Full source

/-- If `F` is a fully faithful functor, split epimorphisms are preserved and reflected by `F`. -/
noncomputable def splitEpiEquiv [Full F] [Faithful F] : SplitEpiSplitEpi f ≃ SplitEpi (F.map f) where
  toFun f := f.map F
  invFun s := ⟨F.preimage s.section_, by
    apply F.map_injective
    simp only [map_comp, map_preimage, map_id]
    apply SplitEpi.id⟩
  left_inv := by aesop_cat
  right_inv x := by aesop_cat

Equivalence of Split Epimorphisms under Fully Faithful Functors

Informal description

Given a fully faithful functor $ F \colon C \to D $ between categories $ C $ and $ D $, there is a natural equivalence between split epimorphisms $ f $ in $ C $ and split epimorphisms $ F(f) $ in $ D $. Specifically, the equivalence is constructed as follows: - The forward direction maps a split epimorphism $ f $ in $ C $ to the split epimorphism $ F(f) $ in $ D $. - The backward direction uses the preimage under $ F $ to recover a split epimorphism in $ C $ from a split epimorphism in $ D $. This equivalence demonstrates that fully faithful functors both preserve and reflect split epimorphisms.

CategoryTheory.Functor.isSplitEpi_iff theorem

[Full F] [Faithful F] : IsSplitEpi (F.map f) ↔ IsSplitEpi f

Full source

@[simp]
theorem isSplitEpi_iff [Full F] [Faithful F] : IsSplitEpiIsSplitEpi (F.map f) ↔ IsSplitEpi f := by
  constructor
  · intro h
    exact IsSplitEpi.mk' ((splitEpiEquiv F f).invFun h.exists_splitEpi.some)
  · intro h
    exact IsSplitEpi.mk' ((splitEpiEquiv F f).toFun h.exists_splitEpi.some)

Characterization of Split Epimorphisms under Fully Faithful Functors

Informal description

Let $F \colon C \to D$ be a fully faithful functor between categories $C$ and $D$. For any morphism $f$ in $C$, the morphism $F(f)$ is a split epimorphism in $D$ if and only if $f$ is a split epimorphism in $C$.

CategoryTheory.Functor.splitMonoEquiv definition

[Full F] [Faithful F] : SplitMono f ≃ SplitMono (F.map f)

Full source

/-- If `F` is a fully faithful functor, split monomorphisms are preserved and reflected by `F`. -/
noncomputable def splitMonoEquiv [Full F] [Faithful F] : SplitMonoSplitMono f ≃ SplitMono (F.map f) where
  toFun f := f.map F
  invFun s := ⟨F.preimage s.retraction, by
    apply F.map_injective
    simp only [map_comp, map_preimage, map_id]
    apply SplitMono.id⟩
  left_inv := by aesop_cat
  right_inv x := by aesop_cat

Equivalence of Split Monomorphisms under a Fully Faithful Functor

Informal description

Given a fully faithful functor $ F \colon C \to D $ between categories $ C $ and $ D $, there is a natural equivalence between the type of split monomorphisms $ f \colon X \to Y $ in $ C $ and the type of split monomorphisms $ F(f) \colon F(X) \to F(Y) $ in $ D $. The equivalence is constructed as follows: - The forward direction maps a split monomorphism $ f $ in $ C $ to its image $ F(f) $ under $ F $, which remains a split monomorphism in $ D $. - The backward direction uses the fullness of $ F $ to lift a split monomorphism $ s $ in $ D $ back to a split monomorphism in $ C $, ensuring that the composition properties are preserved due to the faithfulness of $ F $.

CategoryTheory.Functor.isSplitMono_iff theorem

[Full F] [Faithful F] : IsSplitMono (F.map f) ↔ IsSplitMono f

Full source

@[simp]
theorem isSplitMono_iff [Full F] [Faithful F] : IsSplitMonoIsSplitMono (F.map f) ↔ IsSplitMono f := by
  constructor
  · intro h
    exact IsSplitMono.mk' ((splitMonoEquiv F f).invFun h.exists_splitMono.some)
  · intro h
    exact IsSplitMono.mk' ((splitMonoEquiv F f).toFun h.exists_splitMono.some)

Characterization of Split Monomorphisms under a Fully Faithful Functor: $F(f)$ is split mono $\leftrightarrow$ $f$ is split mono

Informal description

Let $F \colon C \to D$ be a fully faithful functor between categories $C$ and $D$. For any morphism $f \colon X \to Y$ in $C$, the morphism $F(f) \colon F(X) \to F(Y)$ is a split monomorphism in $D$ if and only if $f$ is a split monomorphism in $C$.

CategoryTheory.Functor.epi_map_iff_epi theorem

[hF₁ : PreservesEpimorphisms F] [hF₂ : ReflectsEpimorphisms F] : Epi (F.map f) ↔ Epi f

Full source

@[simp]
theorem epi_map_iff_epi [hF₁ : PreservesEpimorphisms F] [hF₂ : ReflectsEpimorphisms F] :
    EpiEpi (F.map f) ↔ Epi f := by
  constructor
  · exact F.epi_of_epi_map
  · intro h
    exact F.map_epi f

Characterization of Epimorphisms under a Functor Preserving and Reflecting Epimorphisms: $F(f)$ is epi $\leftrightarrow$ $f$ is epi

Informal description

Let $F \colon C \to D$ be a functor between categories that both preserves and reflects epimorphisms. For any morphism $f \colon X \to Y$ in $C$, the morphism $F(f) \colon F(X) \to F(Y)$ is an epimorphism in $D$ if and only if $f$ is an epimorphism in $C$.

CategoryTheory.Functor.mono_map_iff_mono theorem

[hF₁ : PreservesMonomorphisms F] [hF₂ : ReflectsMonomorphisms F] : Mono (F.map f) ↔ Mono f

Full source

@[simp]
theorem mono_map_iff_mono [hF₁ : PreservesMonomorphisms F] [hF₂ : ReflectsMonomorphisms F] :
    MonoMono (F.map f) ↔ Mono f := by
  constructor
  · exact F.mono_of_mono_map
  · intro h
    exact F.map_mono f

Monomorphism Preservation and Reflection by a Functor: $F(f)$ is Mono $\leftrightarrow$ $f$ is Mono

Informal description

Let $F \colon C \to D$ be a functor that both preserves and reflects monomorphisms. For any morphism $f \colon X \to Y$ in $C$, the morphism $F(f) \colon F(X) \to F(Y)$ is a monomorphism in $D$ if and only if $f$ is a monomorphism in $C$.

CategoryTheory.Functor.splitEpiCategoryImpOfIsEquivalence theorem

[IsEquivalence F] [SplitEpiCategory C] : SplitEpiCategory D

Full source

/-- If `F : C ⥤ D` is an equivalence of categories and `C` is a `split_epi_category`,
then `D` also is. -/
theorem splitEpiCategoryImpOfIsEquivalence [IsEquivalence F] [SplitEpiCategory C] :
    SplitEpiCategory D :=
  ⟨fun {X} {Y} f => by
    intro
    rw [← F.inv.isSplitEpi_iff f]
    apply isSplitEpi_of_epi⟩

Equivalence of Categories Preserves Split Epi Category Structure

Informal description

If $F \colon C \to D$ is an equivalence of categories and $C$ is a split epi category, then $D$ is also a split epi category. That is, every epimorphism in $D$ admits a section.

CategoryTheory.Adjunction.strongEpi_map_of_strongEpi theorem

 (adj : F ⊣ F') (f : A ⟶ B) [F'.PreservesMonomorphisms] [F.PreservesEpimorphisms] [StrongEpi f] : StrongEpi (F.map f)

Full source

theorem strongEpi_map_of_strongEpi (adj : F ⊣ F') (f : A ⟶ B) [F'.PreservesMonomorphisms]
    [F.PreservesEpimorphisms] [StrongEpi f] : StrongEpi (F.map f) :=
  ⟨inferInstance, fun X Y Z => by
    intro
    rw [adj.hasLiftingProperty_iff]
    infer_instance⟩

Preservation of Strong Epimorphisms under an Adjunction with Monomorphism-Preserving Right Adjoint

Informal description

Given an adjunction $F \dashv F'$ between functors $F \colon C \to D$ and $F' \colon D \to C$, where $F'$ preserves monomorphisms and $F$ preserves epimorphisms, and given a strong epimorphism $f \colon A \to B$ in $C$, the morphism $F(f) \colon F(A) \to F(B)$ is a strong epimorphism in $D$.

CategoryTheory.Adjunction.strongEpi_map_of_isEquivalence instance

[F.IsEquivalence] (f : A ⟶ B) [_h : StrongEpi f] : StrongEpi (F.map f)

Full source

instance strongEpi_map_of_isEquivalence [F.IsEquivalence] (f : A ⟶ B) [_h : StrongEpi f] :
    StrongEpi (F.map f) :=
  F.asEquivalence.toAdjunction.strongEpi_map_of_strongEpi f

Equivalences Preserve Strong Epimorphisms

Informal description

For any equivalence of categories $F \colon C \simeq D$ and any strong epimorphism $f \colon A \to B$ in $C$, the morphism $F(f) \colon F(A) \to F(B)$ is a strong epimorphism in $D$.

CategoryTheory.Adjunction.instMonoCoeEquivHomObjHomEquivOfReflectsMonomorphisms instance

 (adj : F ⊣ F') {X : C} {Y : D} (f : F.obj X ⟶ Y) [hf : Mono f] [F.ReflectsMonomorphisms] : Mono (adj.homEquiv _ _ f)

Full source

instance (adj : F ⊣ F') {X : C} {Y : D} (f : F.obj X ⟶ Y) [hf : Mono f] [F.ReflectsMonomorphisms] :
    Mono (adj.homEquiv _ _ f) :=
  F.mono_of_mono_map <| by
    rw [← (homEquiv adj X Y).symm_apply_apply f] at hf
    exact mono_of_mono_fac (adj.homEquiv_counit _ _ _).symm

Monomorphism Reflection via Adjunction Hom-Set Equivalence

Informal description

Given an adjunction $F \dashv F'$ between functors $F \colon C \to D$ and $F' \colon D \to C$, where $F$ reflects monomorphisms, and a monomorphism $f \colon F(X) \to Y$ in $D$, the corresponding morphism under the adjunction hom-set equivalence is a monomorphism in $C$.

CategoryTheory.Functor.strongEpi_map_iff_strongEpi_of_isEquivalence theorem

[IsEquivalence F] : StrongEpi (F.map f) ↔ StrongEpi f

Full source

@[simp]
theorem strongEpi_map_iff_strongEpi_of_isEquivalence [IsEquivalence F] :
    StrongEpiStrongEpi (F.map f) ↔ StrongEpi f := by
  constructor
  · intro
    have e : Arrow.mkArrow.mk f ≅ Arrow.mk (F.inv.map (F.map f)) :=
      Arrow.isoOfNatIso F.asEquivalence.unitIso (Arrow.mk f)
    rw [StrongEpi.iff_of_arrow_iso e]
    infer_instance
  · intro
    infer_instance

Equivalence of Categories Preserves and Reflects Strong Epimorphisms

Informal description

For any equivalence of categories $F \colon C \simeq D$ and any morphism $f$ in $C$, the morphism $F(f)$ is a strong epimorphism in $D$ if and only if $f$ is a strong epimorphism in $C$.