Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero

CategoryTheory.Functor.PreservesZeroMorphisms structure

(F : C ⥤ D)

Full source

/-- A functor preserves zero morphisms if it sends zero morphisms to zero morphisms. -/
class PreservesZeroMorphisms (F : C ⥤ D) : Prop where
  /-- For any pair objects `F (0: X ⟶ Y) = (0 : F X ⟶ F Y)` -/
  map_zero : ∀ X Y : C, F.map (0 : X ⟶ Y) = 0 := by aesop

Functor Preserving Zero Morphisms

Informal description

A functor $ F : C \to D $ between categories $ C $ and $ D $ preserves zero morphisms if for every pair of objects $ X $ and $ Y $ in $ C $, the image of the zero morphism $ 0 : X \to Y $ under $ F $ is the zero morphism $ 0 : F(X) \to F(Y) $ in $ D $. This means that $ F $ maps zero morphisms in $ C $ to zero morphisms in $ D $.

CategoryTheory.Functor.map_zero theorem

(F : C ⥤ D) [PreservesZeroMorphisms F] (X Y : C) : F.map (0 : X ⟶ Y) = 0

Full source

@[simp]
protected theorem map_zero (F : C ⥤ D) [PreservesZeroMorphisms F] (X Y : C) :
    F.map (0 : X ⟶ Y) = 0 :=
  PreservesZeroMorphisms.map_zero _ _

Functor Preserves Zero Morphisms: $F(0) = 0$

Informal description

For any functor $F \colon C \to D$ that preserves zero morphisms, and for any objects $X, Y$ in $C$, the image of the zero morphism $0 \colon X \to Y$ under $F$ is the zero morphism $0 \colon F(X) \to F(Y)$ in $D$, i.e., $F(0) = 0$.

CategoryTheory.Functor.map_isZero theorem

(F : C ⥤ D) [PreservesZeroMorphisms F] {X : C} (hX : IsZero X) : IsZero (F.obj X)

Full source

lemma map_isZero (F : C ⥤ D) [PreservesZeroMorphisms F] {X : C} (hX : IsZero X) :
    IsZero (F.obj X) := by
  simp only [IsZero.iff_id_eq_zero] at hX ⊢
  rw [← F.map_id, hX, F.map_zero]

Preservation of Zero Objects under Functors Preserving Zero Morphisms

Informal description

Let $F \colon C \to D$ be a functor between categories $C$ and $D$ that preserves zero morphisms. If an object $X$ in $C$ is a zero object, then its image $F(X)$ under $F$ is also a zero object in $D$.

CategoryTheory.Functor.zero_of_map_zero theorem

(F : C ⥤ D) [PreservesZeroMorphisms F] [Faithful F] {X Y : C} (f : X ⟶ Y) (h : F.map f = 0) : f = 0

Full source

theorem zero_of_map_zero (F : C ⥤ D) [PreservesZeroMorphisms F] [Faithful F] {X Y : C} (f : X ⟶ Y)
    (h : F.map f = 0) : f = 0 :=
  F.map_injective <| h.trans <| Eq.symm <| F.map_zero _ _

Faithful Functors Reflect Zero Morphisms: $F(f) = 0 \implies f = 0$

Informal description

Let $F \colon C \to D$ be a faithful functor between categories $C$ and $D$ that preserves zero morphisms. For any morphism $f \colon X \to Y$ in $C$, if $F(f) = 0$ in $D$, then $f = 0$ in $C$.

CategoryTheory.Functor.map_eq_zero_iff theorem

(F : C ⥤ D) [PreservesZeroMorphisms F] [Faithful F] {X Y : C} {f : X ⟶ Y} : F.map f = 0 ↔ f = 0

Full source

theorem map_eq_zero_iff (F : C ⥤ D) [PreservesZeroMorphisms F] [Faithful F] {X Y : C} {f : X ⟶ Y} :
    F.map f = 0 ↔ f = 0 :=
  ⟨F.zero_of_map_zero _, by
    rintro rfl
    exact F.map_zero _ _⟩

Faithful Functors Preserving Zero Morphisms Reflect Zero Morphisms: $F(f) = 0 \iff f = 0$

Informal description

Let $F \colon C \to D$ be a faithful functor between categories $C$ and $D$ that preserves zero morphisms. For any morphism $f \colon X \to Y$ in $C$, the image $F(f)$ is the zero morphism in $D$ if and only if $f$ is the zero morphism in $C$, i.e., $F(f) = 0 \leftrightarrow f = 0$.

CategoryTheory.Functor.preservesZeroMorphisms_of_isLeftAdjoint instance

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

Full source

instance (priority := 100) preservesZeroMorphisms_of_isLeftAdjoint (F : C ⥤ D) [IsLeftAdjoint F] :
    PreservesZeroMorphisms F where
  map_zero X Y := by
    let adj := Adjunction.ofIsLeftAdjoint F
    calc
      F.map (0 : X ⟶ Y) = F.map 0 ≫ F.map (adj.unit.app Y) ≫ adj.counit.app (F.obj Y) := ?_
      _ = F.map 0 ≫ F.map ((rightAdjoint F).map (0 : F.obj X ⟶ _)) ≫ adj.counit.app (F.obj Y) := ?_
      _ = 0 := ?_
    · rw [Adjunction.left_triangle_components]
      exact (Category.comp_id _).symm
    · simp only [← Category.assoc, ← F.map_comp, zero_comp]
    · simp only [Adjunction.counit_naturality, comp_zero]

Left Adjoint Functors Preserve Zero Morphisms

Informal description

Every left adjoint functor between categories preserves zero morphisms. That is, if $F \colon C \to D$ is a left adjoint functor between categories $C$ and $D$ with zero morphisms, then $F$ maps the zero morphism $0 \colon X \to Y$ in $C$ to the zero morphism $0 \colon F(X) \to F(Y)$ in $D$ for all objects $X, Y \in C$.

CategoryTheory.Functor.preservesZeroMorphisms_of_isRightAdjoint instance

(G : C ⥤ D) [IsRightAdjoint G] : PreservesZeroMorphisms G

Full source

instance (priority := 100) preservesZeroMorphisms_of_isRightAdjoint (G : C ⥤ D) [IsRightAdjoint G] :
    PreservesZeroMorphisms G where
  map_zero X Y := by
    let adj := Adjunction.ofIsRightAdjoint G
    calc
      G.map (0 : X ⟶ Y) = adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) ≫ G.map 0 := ?_
      _ = adj.unit.app (G.obj X) ≫ G.map ((leftAdjoint G).map (0 : _ ⟶ G.obj X)) ≫ G.map 0 := ?_
      _ = 0 := ?_
    · rw [Adjunction.right_triangle_components_assoc]
    · simp only [← G.map_comp, comp_zero]
    · simp only [id_obj, comp_obj, Adjunction.unit_naturality_assoc, zero_comp]

Right Adjoint Functors Preserve Zero Morphisms

Informal description

Every right adjoint functor between categories preserves zero morphisms. That is, if $G \colon C \to D$ is a right adjoint functor between categories $C$ and $D$ with zero morphisms, then $G$ maps the zero morphism $0 \colon X \to Y$ in $C$ to the zero morphism $0 \colon G(X) \to G(Y)$ in $D$ for all objects $X, Y \in C$.

CategoryTheory.Functor.preservesZeroMorphisms_of_full instance

(F : C ⥤ D) [Full F] : PreservesZeroMorphisms F

Full source

instance (priority := 100) preservesZeroMorphisms_of_full (F : C ⥤ D) [Full F] :
    PreservesZeroMorphisms F where
  map_zero X Y :=
    calc
      F.map (0 : X ⟶ Y) = F.map (0 ≫ F.preimage (0 : F.obj Y ⟶ F.obj Y)) := by rw [zero_comp]
      _ = 0 := by rw [F.map_comp, F.map_preimage, comp_zero]

Full Functors Preserve Zero Morphisms

Informal description

Every full functor between categories preserves zero morphisms. That is, if $F \colon C \to D$ is a full functor between categories $C$ and $D$ with zero morphisms, then $F$ maps the zero morphism $0 \colon X \to Y$ in $C$ to the zero morphism $0 \colon F(X) \to F(Y)$ in $D$ for all objects $X, Y \in C$.

CategoryTheory.Functor.preservesZeroMorphisms_comp instance

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

Full source

instance preservesZeroMorphisms_comp (F : C ⥤ D) (G : D ⥤ E)
    [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] :
    (F ⋙ G).PreservesZeroMorphisms := ⟨by simp⟩

Composition of Zero-Morphism-Preserving Functors Preserves Zero Morphisms

Informal description

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

CategoryTheory.Functor.preservesZeroMorphisms_of_iso theorem

{F₁ F₂ : C ⥤ D} [F₁.PreservesZeroMorphisms] (e : F₁ ≅ F₂) : F₂.PreservesZeroMorphisms

Full source

lemma preservesZeroMorphisms_of_iso {F₁ F₂ : C ⥤ D} [F₁.PreservesZeroMorphisms] (e : F₁ ≅ F₂) :
    F₂.PreservesZeroMorphisms where
  map_zero X Y := by simp only [← cancel_epi (e.hom.app X), ← e.hom.naturality,
    F₁.map_zero, zero_comp, comp_zero]

Preservation of Zero Morphisms under Natural Isomorphism

Informal description

Given two functors $F_1, F_2 \colon C \to D$ and a natural isomorphism $e \colon F_1 \cong F_2$, if $F_1$ preserves zero morphisms, then $F_2$ also preserves zero morphisms.

CategoryTheory.Functor.preservesZeroMorphisms_evaluation_obj instance

(j : D) : PreservesZeroMorphisms ((evaluation D C).obj j)

Full source

instance preservesZeroMorphisms_evaluation_obj (j : D) :
    PreservesZeroMorphisms ((evaluation D C).obj j) where

Evaluation Functor Preserves Zero Morphisms at Each Object

Informal description

For any object $j$ in category $D$, the evaluation functor $(evaluation\, D\, C).obj\, j$ preserves zero morphisms. That is, it maps zero morphisms in the functor category $C \to D$ to zero morphisms in $D$.

CategoryTheory.Functor.instPreservesZeroMorphismsFlipOfObj instance

(F : C ⥤ D ⥤ E) [∀ X, (F.obj X).PreservesZeroMorphisms] : F.flip.PreservesZeroMorphisms

Full source

instance (F : C ⥤ D ⥤ E) [∀ X, (F.obj X).PreservesZeroMorphisms] :
    F.flip.PreservesZeroMorphisms where

Preservation of Zero Morphisms by Flipped Functors

Informal description

For any functor $F \colon C \to D \to E$ such that for every object $X$ in $C$, the functor $F(X) \colon D \to E$ preserves zero morphisms, the flipped functor $F^{\mathrm{flip}} \colon D \to C \to E$ also preserves zero morphisms.

CategoryTheory.Functor.instPreservesZeroMorphismsObjFlip instance

(F : C ⥤ D ⥤ E) [F.PreservesZeroMorphisms] (Y : D) : (F.flip.obj Y).PreservesZeroMorphisms

Full source

instance (F : C ⥤ D ⥤ E) [F.PreservesZeroMorphisms] (Y : D) :
    (F.flip.obj Y).PreservesZeroMorphisms where

Preservation of Zero Morphisms by Flipped Functor Components

Informal description

For any functor $F \colon C \to D \to E$ that preserves zero morphisms and any object $Y$ in $D$, the flipped functor $F.\text{flip}.obj\, Y \colon C \to E$ also preserves zero morphisms.

CategoryTheory.Functor.mapZeroObject definition

[PreservesZeroMorphisms F] : F.obj 0 ≅ 0

Full source

/-- A functor that preserves zero morphisms also preserves the zero object. -/
@[simps]
def mapZeroObject [PreservesZeroMorphisms F] : F.obj 0 ≅ 0 where
  hom := 0
  inv := 0
  hom_inv_id := by rw [← F.map_id, id_zero, F.map_zero, zero_comp]
  inv_hom_id := by rw [id_zero, comp_zero]

Preservation of zero object by a zero-morphism-preserving functor

Informal description

Given a functor $ F : C \to D $ between categories $ C $ and $ D $ that preserves zero morphisms, the image $ F(0) $ of the zero object $ 0 $ in $ C $ is isomorphic to the zero object $ 0 $ in $ D $. The isomorphism is given by the zero morphisms in both directions.

CategoryTheory.Functor.preservesZeroMorphisms_of_map_zero_object theorem

(i : F.obj 0 ≅ 0) : PreservesZeroMorphisms F

Full source

theorem preservesZeroMorphisms_of_map_zero_object (i : F.obj 0 ≅ 0) : PreservesZeroMorphisms F where
  map_zero X Y :=
    calc
      F.map (0 : X ⟶ Y) = F.map (0 : X ⟶ 0) ≫ F.map 0 := by rw [← Functor.map_comp, comp_zero]
      _ = F.map 0 ≫ (i.hom ≫ i.inv) ≫ F.map 0 := by rw [Iso.hom_inv_id, Category.id_comp]
      _ = 0 := by simp only [zero_of_to_zero i.hom, zero_comp, comp_zero]

Preservation of Zero Morphisms via Zero Object Isomorphism

Informal description

Given a functor $F \colon C \to D$ between categories with zero objects, if the image $F(0)$ of the zero object in $C$ is isomorphic to the zero object in $D$ via an isomorphism $i \colon F(0) \to 0$, then $F$ preserves zero morphisms.

CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_initial_object instance

[PreservesColimit (Functor.empty.{0} C) F] : PreservesZeroMorphisms F

Full source

instance (priority := 100) preservesZeroMorphisms_of_preserves_initial_object
    [PreservesColimit (Functor.empty.{0} C) F] : PreservesZeroMorphisms F :=
  preservesZeroMorphisms_of_map_zero_object <|
    F.mapIso HasZeroObject.zeroIsoInitial ≪≫
      PreservesInitial.iso F ≪≫ HasZeroObject.zeroIsoInitial.symm

Preservation of Zero Morphisms via Initial Object Preservation

Informal description

For any functor $F \colon C \to D$ between categories with zero objects, if $F$ preserves the initial object (i.e., $F$ preserves the colimit of the empty functor), then $F$ preserves zero morphisms.

CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_terminal_object instance

[PreservesLimit (Functor.empty.{0} C) F] : PreservesZeroMorphisms F

Full source

instance (priority := 100) preservesZeroMorphisms_of_preserves_terminal_object
    [PreservesLimit (Functor.empty.{0} C) F] : PreservesZeroMorphisms F :=
  preservesZeroMorphisms_of_map_zero_object <|
    F.mapIso HasZeroObject.zeroIsoTerminal ≪≫
      PreservesTerminal.iso F ≪≫ HasZeroObject.zeroIsoTerminal.symm

Preservation of Zero Morphisms via Terminal Object Preservation

Informal description

A functor $F \colon \mathcal{C} \to \mathcal{D}$ between categories preserves zero morphisms if it preserves the terminal object of $\mathcal{C}$ (i.e., maps it to a terminal object in $\mathcal{D}$).

CategoryTheory.Functor.preservesTerminalObject_of_preservesZeroMorphisms theorem

[PreservesZeroMorphisms F] : PreservesLimit (Functor.empty.{0} C) F

Full source

/-- Preserving zero morphisms implies preserving terminal objects. -/
lemma preservesTerminalObject_of_preservesZeroMorphisms [PreservesZeroMorphisms F] :
    PreservesLimit (Functor.empty.{0} C) F :=
  preservesTerminal_of_iso F <|
    F.mapIso HasZeroObject.zeroIsoTerminal.symm ≪≫ mapZeroObject F ≪≫ HasZeroObject.zeroIsoTerminal

Preservation of Terminal Objects by Zero-Morphism-Preserving Functors

Informal description

If a functor $F \colon \mathcal{C} \to \mathcal{D}$ preserves zero morphisms, then it preserves terminal objects. That is, $F$ maps the terminal object in $\mathcal{C}$ to the terminal object in $\mathcal{D}$.

CategoryTheory.Functor.preservesInitialObject_of_preservesZeroMorphisms theorem

[PreservesZeroMorphisms F] : PreservesColimit (Functor.empty.{0} C) F

Full source

/-- Preserving zero morphisms implies preserving terminal objects. -/
lemma preservesInitialObject_of_preservesZeroMorphisms [PreservesZeroMorphisms F] :
    PreservesColimit (Functor.empty.{0} C) F :=
  preservesInitial_of_iso F <|
    HasZeroObject.zeroIsoInitialHasZeroObject.zeroIsoInitial.symm ≪≫
      (mapZeroObject F).symm ≪≫ (F.mapIso HasZeroObject.zeroIsoInitial.symm).symm

Preservation of Initial Objects by Zero-Morphism-Preserving Functors

Informal description

If a functor $F \colon \mathcal{C} \to \mathcal{D}$ between categories with zero morphisms preserves zero morphisms, then it preserves initial objects. Specifically, $F$ maps the initial object of $\mathcal{C}$ to the initial object of $\mathcal{D}$.

CategoryTheory.Functor.preservesLimitsOfShape_of_isZero theorem

: PreservesLimitsOfShape J G

Full source

/-- A zero functor preserves limits. -/
lemma preservesLimitsOfShape_of_isZero : PreservesLimitsOfShape J G where
  preservesLimit {K} := ⟨fun _ => ⟨by
    rw [Functor.isZero_iff] at hG
    exact IsLimit.ofIsZero _ ((K ⋙ G).isZero (fun X ↦ hG _)) (hG _)⟩⟩

Zero Functors Preserve All Limits of a Given Shape

Informal description

If a functor $G \colon \mathcal{C} \to \mathcal{D}$ is a zero functor (i.e., it maps every object to a zero object and every morphism to a zero morphism), then $G$ preserves all limits of shape $J$ in $\mathcal{C}$.

CategoryTheory.Functor.preservesColimitsOfShape_of_isZero theorem

: PreservesColimitsOfShape J G

Full source

/-- A zero functor preserves colimits. -/
lemma preservesColimitsOfShape_of_isZero : PreservesColimitsOfShape J G where
  preservesColimit {K} := ⟨fun _ => ⟨by
    rw [Functor.isZero_iff] at hG
    exact IsColimit.ofIsZero _ ((K ⋙ G).isZero (fun X ↦ hG _)) (hG _)⟩⟩

Zero Functor Preserves All Colimits of a Given Shape

Informal description

A zero functor $G \colon \mathcal{C} \to \mathcal{D}$ preserves all colimits of shape $J$. That is, if $G$ maps every object and morphism in $\mathcal{C}$ to a zero object and zero morphism in $\mathcal{D}$, then for any diagram $F \colon J \to \mathcal{C}$, the functor $G$ preserves the colimit of $F$.

CategoryTheory.Functor.preservesLimitsOfSize_of_isZero theorem

: PreservesLimitsOfSize.{v, u} G

Full source

/-- A zero functor preserves limits. -/
lemma preservesLimitsOfSize_of_isZero : PreservesLimitsOfSize.{v, u} G where
  preservesLimitsOfShape := G.preservesLimitsOfShape_of_isZero hG _

Zero Functors Preserve All Limits of Any Size

Informal description

If a functor $G \colon \mathcal{C} \to \mathcal{D}$ is a zero functor (i.e., it maps every object to a zero object and every morphism to a zero morphism), then $G$ preserves all limits of any size (i.e., for any diagram shape $J$ in $\mathcal{C}$, $G$ preserves the limit of $J$).

CategoryTheory.Functor.preservesColimitsOfSize_of_isZero theorem

: PreservesColimitsOfSize.{v, u} G

Full source

/-- A zero functor preserves colimits. -/
lemma preservesColimitsOfSize_of_isZero : PreservesColimitsOfSize.{v, u} G where
  preservesColimitsOfShape := G.preservesColimitsOfShape_of_isZero hG _

Zero Functor Preserves All Colimits

Informal description

A zero functor $G \colon \mathcal{C} \to \mathcal{D}$ preserves all colimits of any size. That is, if $G$ maps every object and morphism in $\mathcal{C}$ to a zero object and zero morphism in $\mathcal{D}$, then $G$ preserves all colimits in $\mathcal{C}$ regardless of their shape or size.

Main results