Documentation

Mathlib.CategoryTheory.Functor.EpiMono

Preservation and reflection of monomorphisms and epimorphisms #

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

A functor preserves monomorphisms if it maps monomorphisms to monomorphisms.

Instances

    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] :
    Equations
    • =

    A functor preserves epimorphisms if it maps epimorphisms to epimorphisms.

    Instances
      theorem CategoryTheory.Functor.PreservesEpimorphisms.preserves {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [self : F.PreservesEpimorphisms] {X : C} {Y : C} (f : X Y) [CategoryTheory.Epi 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] :
      Equations
      • =

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

      Instances
        theorem CategoryTheory.Functor.ReflectsMonomorphisms.reflects {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [self : F.ReflectsMonomorphisms] {X : C} {Y : C} (f : X Y) :

        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)) :

        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.

        Instances
          theorem CategoryTheory.Functor.ReflectsEpimorphisms.reflects {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [self : F.ReflectsEpimorphisms] {X : C} {Y : C} (f : X Y) :

          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)) :
          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
          @[instance 100]
          Equations
          • =
          @[instance 100]
          Equations
          • =
          @[instance 100]
          Equations
          • =
          @[instance 100]
          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] :

          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.
          Instances For

            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.
            Instances For
              @[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] :
              @[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] :

              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) [h₁ : F'.PreservesMonomorphisms] [h₂ : F.PreservesEpimorphisms] [CategoryTheory.StrongEpi f] :
              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
              • =