Documentation

Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero

Preservation of zero objects and zero morphisms #

We define the class PreservesZeroMorphisms and show basic properties.

Main results #

We provide the following results:

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

A functor preserves zero morphisms if it sends zero morphisms to zero morphisms.

  • map_zero : ∀ (X Y : C), F.map 0 = 0

    For any pair objects F (0: X ⟶ Y) = (0 : F X ⟶ F Y)

Instances
    source
    theorem CategoryTheory.Functor.PreservesZeroMorphisms.map_zero {C : Type u₁} :
    ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D} {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {inst_3 : CategoryTheory.Limits.HasZeroMorphisms D} {F : CategoryTheory.Functor C D} [self : F.PreservesZeroMorphisms] (X Y : C), F.map 0 = 0

    For any pair objects F (0: X ⟶ Y) = (0 : F X ⟶ F Y)

    source
    @[simp]
    theorem CategoryTheory.Functor.map_zero {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] (X : C) (Y : C) :
    F.map 0 = 0
    source
    theorem CategoryTheory.Functor.map_isZero {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {X : C} (hX : CategoryTheory.Limits.IsZero X) :
    CategoryTheory.Limits.IsZero (F.obj X)
    source
    theorem CategoryTheory.Functor.zero_of_map_zero {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [F.Faithful] {X : C} {Y : C} (f : X ⟶ Y) (h : F.map f = 0) :
    f = 0
    source
    theorem CategoryTheory.Functor.map_eq_zero_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [F.Faithful] {X : C} {Y : C} {f : X ⟶ Y} :
    F.map f = 0 ↔ f = 0
    source
    @[instance 100]
    instance CategoryTheory.Functor.preservesZeroMorphisms_of_isLeftAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.IsLeftAdjoint] :
    F.PreservesZeroMorphisms
    Equations
    • ⋯ = ⋯
    source
    @[instance 100]
    instance CategoryTheory.Functor.preservesZeroMorphisms_of_isRightAdjoint {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D) [G.IsRightAdjoint] :
    G.PreservesZeroMorphisms
    Equations
    • ⋯ = ⋯
    source
    @[instance 100]
    instance CategoryTheory.Functor.preservesZeroMorphisms_of_full {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.Full] :
    F.PreservesZeroMorphisms
    Equations
    • ⋯ = ⋯
    source
    instance CategoryTheory.Functor.preservesZeroMorphisms_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] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.Limits.HasZeroMorphisms E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] :
    (F.comp G).PreservesZeroMorphisms
    Equations
    • ⋯ = ⋯
    source
    theorem CategoryTheory.Functor.preservesZeroMorphisms_of_iso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {F₁ : CategoryTheory.Functor C D} {F₂ : CategoryTheory.Functor C D} [F₁.PreservesZeroMorphisms] (e : F₁ ≅ F₂) :
    F₂.PreservesZeroMorphisms
    source
    instance CategoryTheory.Functor.preservesZeroMorphisms_evaluation_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms C] (j : D) :
    ((CategoryTheory.evaluation D C).obj j).PreservesZeroMorphisms
    Equations
    • ⋯ = ⋯
    source
    instance CategoryTheory.Functor.instPreservesZeroMorphismsFlipOfObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.Limits.HasZeroMorphisms E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) [∀ (X : C), (F.obj X).PreservesZeroMorphisms] :
    F.flip.PreservesZeroMorphisms
    Equations
    • ⋯ = ⋯
    source
    instance CategoryTheory.Functor.instPreservesZeroMorphismsObjFlip {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) [F.PreservesZeroMorphisms] (Y : D) :
    (F.flip.obj Y).PreservesZeroMorphisms
    Equations
    • ⋯ = ⋯
    source
    @[simp]
    theorem CategoryTheory.Functor.mapZeroObject_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] :
    F.mapZeroObject.hom = 0
    source
    @[simp]
    theorem CategoryTheory.Functor.mapZeroObject_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] :
    F.mapZeroObject.inv = 0
    source
    def CategoryTheory.Functor.mapZeroObject {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] :
    F.obj 0 ≅ 0

    A functor that preserves zero morphisms also preserves the zero object.

    Equations
    • F.mapZeroObject = { hom := 0, inv := 0, hom_inv_id := ⋯, inv_hom_id := ⋯ }
    Instances For
      source
      theorem CategoryTheory.Functor.preservesZeroMorphisms_of_map_zero_object {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {F : CategoryTheory.Functor C D} (i : F.obj 0 ≅ 0) :
      F.PreservesZeroMorphisms
      source
      @[instance 100]
      instance CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_initial_object {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) F] :
      F.PreservesZeroMorphisms
      Equations
      • ⋯ = ⋯
      source
      @[instance 100]
      instance CategoryTheory.Functor.preservesZeroMorphisms_of_preserves_terminal_object {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F] :
      F.PreservesZeroMorphisms
      Equations
      • ⋯ = ⋯
      source
      def CategoryTheory.Functor.preservesTerminalObjectOfPreservesZeroMorphisms {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] :
      CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) F

      Preserving zero morphisms implies preserving terminal objects.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def CategoryTheory.Functor.preservesInitialObjectOfPreservesZeroMorphisms {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] :
        CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) F

        Preserving zero morphisms implies preserving terminal objects.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def CategoryTheory.Functor.preservesLimitsOfShapeOfIsZero {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D) (hG : CategoryTheory.Limits.IsZero G) (J : Type u_1) [CategoryTheory.Category.{u_2, u_1} J] :
          CategoryTheory.Limits.PreservesLimitsOfShape J G

          A zero functor preserves limits.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def CategoryTheory.Functor.preservesColimitsOfShapeOfIsZero {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D) (hG : CategoryTheory.Limits.IsZero G) (J : Type u_1) [CategoryTheory.Category.{u_2, u_1} J] :
            CategoryTheory.Limits.PreservesColimitsOfShape J G

            A zero functor preserves colimits.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def CategoryTheory.Functor.preservesLimitsOfSizeOfIsZero {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D) (hG : CategoryTheory.Limits.IsZero G) :
              CategoryTheory.Limits.PreservesLimitsOfSize.{v, u, v₁, v₂, u₁, u₂} G

              A zero functor preserves limits.

              Equations
              Instances For
                source
                def CategoryTheory.Functor.preservesColimitsOfSizeOfIsZero {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D) (hG : CategoryTheory.Limits.IsZero G) :
                CategoryTheory.Limits.PreservesColimitsOfSize.{v, u, v₁, v₂, u₁, u₂} G

                A zero functor preserves colimits.

                Equations
                Instances For