Documentation

Mathlib.CategoryTheory.Functor.FullyFaithful

Full and faithful functors #

We define typeclasses Full and Faithful, decorating functors.

Main definitions and results #

See CategoryTheory.Equivalence.of_fullyFaithful_ess_surj for the fact that a functor is an equivalence if and only if it is fully faithful and essentially surjective.

class CategoryTheory.Full {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C D) :
Type (max(maxu₁v₁)v₂)
  • The data of a preimage for every f : F.obj X ⟶ F.obj Y⟶ F.obj Y.

    preimage : {X Y : C} → (F.obj X F.obj Y) → (X Y)
  • The property that Full.preimage f of maps to f via F.map.

    witness : autoParam (∀ {X Y : C} (f : F.obj X F.obj Y), F.map (preimage X Y f) = f) _auto✝

A functor F : C ⥤ D⥤ D is full if for each X Y : C, F.map is surjective. In fact, we use a constructive definition, so the Full F typeclass contains data, specifying a particular preimage of each f : F.obj X ⟶ F.obj Y⟶ F.obj Y.

See https://stacks.math.columbia.edu/tag/001C.

Instances
    class CategoryTheory.Faithful {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C D) :

    A functor F : C ⥤ D⥤ D is faithful if for each X Y : C, F.map is injective.

    See https://stacks.math.columbia.edu/tag/001C.

    Instances
      theorem CategoryTheory.Functor.map_injective {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {X : C} {Y : C} (F : C D) [inst : CategoryTheory.Faithful F] :
      def CategoryTheory.Functor.preimage {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {X : C} {Y : C} (F : C D) [inst : CategoryTheory.Full F] (f : F.obj X F.obj Y) :
      X Y

      The specified preimage of a morphism under a full functor.

      Equations
      @[simp]
      theorem CategoryTheory.Functor.image_preimage {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C D) [inst : CategoryTheory.Full F] {X : C} {Y : C} (f : F.obj X F.obj Y) :
      theorem CategoryTheory.Functor.map_surjective {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {X : C} {Y : C} (F : C D) [inst : CategoryTheory.Full F] :
      noncomputable def CategoryTheory.Functor.fullOfExists {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C D) (h : ∀ (X Y : C) (f : F.obj X F.obj Y), p, F.map p = f) :

      Deduce that F is full from the existence of preimages, using choice.

      Equations
      • One or more equations did not get rendered due to their size.
      noncomputable def CategoryTheory.Functor.fullOfSurjective {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C D) (h : ∀ (X Y : C), Function.Surjective (Prefunctor.map F.toPrefunctor)) :

      Deduce that F is full from surjectivity of F.map, using choice.

      Equations
      @[simp]
      theorem CategoryTheory.preimage_id {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {F : C D} [inst : CategoryTheory.Full F] [inst : CategoryTheory.Faithful F] {X : C} :
      @[simp]
      theorem CategoryTheory.preimage_comp {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {F : C D} [inst : CategoryTheory.Full F] [inst : CategoryTheory.Faithful F] {X : C} {Y : C} {Z : C} (f : F.obj X F.obj Y) (g : F.obj Y F.obj Z) :
      @[simp]
      theorem CategoryTheory.preimage_map {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {F : C D} [inst : CategoryTheory.Full F] [inst : CategoryTheory.Faithful F] {X : C} {Y : C} (f : X Y) :
      @[simp]
      theorem CategoryTheory.Functor.preimageIso_inv {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C D) [inst : CategoryTheory.Full F] [inst : CategoryTheory.Faithful F] {X : C} {Y : C} (f : F.obj X F.obj Y) :
      @[simp]
      theorem CategoryTheory.Functor.preimageIso_hom {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C D) [inst : CategoryTheory.Full F] [inst : CategoryTheory.Faithful F] {X : C} {Y : C} (f : F.obj X F.obj Y) :
      def CategoryTheory.Functor.preimageIso {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C D) [inst : CategoryTheory.Full F] [inst : CategoryTheory.Faithful F] {X : C} {Y : C} (f : F.obj X F.obj Y) :
      X Y

      If F : C ⥤ D⥤ D is fully faithful, every isomorphism F.obj X ≅ F.obj Y≅ F.obj Y has a preimage.

      Equations
      theorem CategoryTheory.isIso_of_fully_faithful {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C D) [inst : CategoryTheory.Full F] [inst : CategoryTheory.Faithful F] {X : C} {Y : C} (f : X Y) [inst : CategoryTheory.IsIso (F.map f)] :

      If the image of a morphism under a fully faithful functor in an isomorphism, then the original morphisms is also an isomorphism.

      @[simp]
      theorem CategoryTheory.equivOfFullyFaithful_symm_apply {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C D) [inst : CategoryTheory.Full F] [inst : CategoryTheory.Faithful F] {X : C} {Y : C} (f : F.obj X F.obj Y) :
      @[simp]
      theorem CategoryTheory.equivOfFullyFaithful_apply {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C D) [inst : CategoryTheory.Full F] [inst : CategoryTheory.Faithful F] {X : C} {Y : C} (f : X Y) :
      def CategoryTheory.equivOfFullyFaithful {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C D) [inst : CategoryTheory.Full F] [inst : CategoryTheory.Faithful F] {X : C} {Y : C} :
      (X Y) (F.obj X F.obj Y)

      If F is fully faithful, we have an equivalence of hom-sets X ⟶ Y⟶ Y and F X ⟶ F Y⟶ F Y.

      Equations
      • One or more equations did not get rendered due to their size.
      def CategoryTheory.isoEquivOfFullyFaithful {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] (F : C D) [inst : CategoryTheory.Full F] [inst : CategoryTheory.Faithful F] {X : C} {Y : C} :
      (X Y) (F.obj X F.obj Y)

      If F is fully faithful, we have an equivalence of iso-sets X ≅ Y≅ Y and F X ≅ F Y≅ F Y.

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem CategoryTheory.natTransOfCompFullyFaithful_app {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u_1} [inst : CategoryTheory.Category E] {F : C D} {G : C D} (H : D E) [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful H] (α : F H G H) (X : C) :
      def CategoryTheory.natTransOfCompFullyFaithful {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u_1} [inst : CategoryTheory.Category E] {F : C D} {G : C D} (H : D E) [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful H] (α : F H G H) :
      F G

      We can construct a natural transformation between functors by constructing a natural transformation between those functors composed with a fully faithful functor.

      Equations
      @[simp]
      theorem CategoryTheory.natIsoOfCompFullyFaithful_hom_app {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u_1} [inst : CategoryTheory.Category E] {F : C D} {G : C D} (H : D E) [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful H] (i : F H G H) (X : C) :
      @[simp]
      theorem CategoryTheory.natIsoOfCompFullyFaithful_inv_app {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u_1} [inst : CategoryTheory.Category E] {F : C D} {G : C D} (H : D E) [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful H] (i : F H G H) (X : C) :
      def CategoryTheory.natIsoOfCompFullyFaithful {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u_1} [inst : CategoryTheory.Category E] {F : C D} {G : C D} (H : D E) [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful H] (i : F H G H) :
      F G

      We can construct a natural isomorphism between functors by constructing a natural isomorphism between those functors composed with a fully faithful functor.

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem CategoryTheory.NatTrans.equivOfCompFullyFaithful_apply {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u_1} [inst : CategoryTheory.Category E] {F : C D} {G : C D} (H : D E) [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful H] (α : F G) :
      def CategoryTheory.NatTrans.equivOfCompFullyFaithful {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u_1} [inst : CategoryTheory.Category E] {F : C D} {G : C D} (H : D E) [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful H] :
      (F G) (F H G H)

      Horizontal composition with a fully faithful functor induces a bijection on natural transformations.

      Equations
      • One or more equations did not get rendered due to their size.
      def CategoryTheory.NatIso.equivOfCompFullyFaithful {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u_1} [inst : CategoryTheory.Category E] {F : C D} {G : C D} (H : D E) [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful H] :
      (F G) (F H G H)

      Horizontal composition with a fully faithful functor induces a bijection on natural isomorphisms.

      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      theorem CategoryTheory.Faithful.of_comp {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] (F : C D) (G : D E) [inst : CategoryTheory.Faithful (F G)] :
      def CategoryTheory.Full.ofIso {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {F : C D} {F' : C D} [inst : CategoryTheory.Full F] (α : F F') :

      If F is full, and naturally isomorphic to some F', then F' is also full.

      Equations
      theorem CategoryTheory.Faithful.of_iso {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {F : C D} {F' : C D} [inst : CategoryTheory.Faithful F] (α : F F') :
      theorem CategoryTheory.Faithful.of_comp_iso {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] {F : C D} {G : D E} {H : C E} [inst : CategoryTheory.Faithful H] (h : F G H) :
      theorem CategoryTheory.Iso.faithful_of_comp {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] {F : C D} {G : D E} {H : C E} [inst : CategoryTheory.Faithful H] (h : F G H) :

      Alias of CategoryTheory.Faithful.of_comp_iso.

      theorem CategoryTheory.Faithful.of_comp_eq {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] {F : C D} {G : D E} {H : C E} [ℋ : CategoryTheory.Faithful H] (h : F G = H) :
      theorem Eq.faithful_of_comp {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] {F : C D} {G : D E} {H : C E} [ℋ : CategoryTheory.Faithful H] (h : F G = H) :

      Alias of CategoryTheory.Faithful.of_comp_eq.

      def CategoryTheory.Faithful.div {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] (F : C E) (G : D E) [inst : CategoryTheory.Faithful G] (obj : CD) (h_obj : ∀ (X : C), G.obj (obj X) = F.obj X) (map : {X Y : C} → (X Y) → (obj X obj Y)) (h_map : ∀ {X Y : C} {f : X Y}, HEq (G.map (map X Y f)) (F.map f)) :
      C D

      “Divide” a functor by a faithful functor.

      Equations
      theorem CategoryTheory.Faithful.div_comp {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] (F : C E) [inst : CategoryTheory.Faithful F] (G : D E) [inst : CategoryTheory.Faithful G] (obj : CD) (h_obj : ∀ (X : C), G.obj (obj X) = F.obj X) (map : {X Y : C} → (X Y) → (obj X obj Y)) (h_map : ∀ {X Y : C} {f : X Y}, HEq (G.map (map X Y f)) (F.map f)) :
      CategoryTheory.Faithful.div F G obj h_obj map h_map G = F
      theorem CategoryTheory.Faithful.div_faithful {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] (F : C E) [inst : CategoryTheory.Faithful F] (G : D E) [inst : CategoryTheory.Faithful G] (obj : CD) (h_obj : ∀ (X : C), G.obj (obj X) = F.obj X) (map : {X Y : C} → (X Y) → (obj X obj Y)) (h_map : ∀ {X Y : C} {f : X Y}, HEq (G.map (map X Y f)) (F.map f)) :
      def CategoryTheory.Full.ofCompFaithful {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] (F : C D) (G : D E) [inst : CategoryTheory.Full (F G)] [inst : CategoryTheory.Faithful G] :

      If F ⋙ G⋙ G is full and G is faithful, then F is full.

      Equations
      def CategoryTheory.Full.ofCompFaithfulIso {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] {F : C D} {G : D E} {H : C E} [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful G] (h : F G H) :

      If F ⋙ G⋙ G is full and G is faithful, then F is full.

      Equations
      def CategoryTheory.fullyFaithfulCancelRight {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] {F : C D} {G : C D} (H : D E) [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful H] (comp_iso : F H G H) :
      F G

      Given a natural isomorphism between F ⋙ H⋙ H and G ⋙ H⋙ H for a fully faithful functor H, we can 'cancel' it to give a natural iso between F and G.

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem CategoryTheory.fullyFaithfulCancelRight_hom_app {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] {F : C D} {G : C D} {H : D E} [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful H] (comp_iso : F H G H) (X : C) :
      (CategoryTheory.fullyFaithfulCancelRight H comp_iso).hom.app X = CategoryTheory.Functor.preimage H (comp_iso.hom.app X)
      @[simp]
      theorem CategoryTheory.fullyFaithfulCancelRight_inv_app {C : Type u₁} [inst : CategoryTheory.Category C] {D : Type u₂} [inst : CategoryTheory.Category D] {E : Type u₃} [inst : CategoryTheory.Category E] {F : C D} {G : C D} {H : D E} [inst : CategoryTheory.Full H] [inst : CategoryTheory.Faithful H] (comp_iso : F H G H) (X : C) :
      (CategoryTheory.fullyFaithfulCancelRight H comp_iso).inv.app X = CategoryTheory.Functor.preimage H (comp_iso.inv.app X)