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.

  • preimage : {X Y : C} → (F.obj X F.obj Y) → (X Y)

    The data of a preimage for every f : F.obj X ⟶ F.obj Y.

  • witness : ∀ {X Y : C} (f : F.obj X F.obj Y), F.map (CategoryTheory.Full.preimage f) = f

    The property that Full.preimage f of maps to f via F.map.

A functor F : C ⥤ 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.

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

Instances
    • map_injective : ∀ {X Y : C}, Function.Injective F.map

      F.map is injective for each X Y : C.

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

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

    Instances

      The specified preimage of a morphism under a full functor.

      Equations
      Instances For
        @[simp]
        theorem CategoryTheory.Functor.image_preimage {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Full F] {X : C} {Y : C} (f : F.obj X F.obj Y) :
        F.map (F.preimage f) = f
        noncomputable def CategoryTheory.Functor.fullOfExists {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor 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.
        Instances For

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

          Equations
          Instances For
            @[simp]
            theorem CategoryTheory.preimage_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} [CategoryTheory.Full F] [CategoryTheory.Faithful F] {X : C} {Y : C} {Z : C} (f : F.obj X F.obj Y) (g : F.obj Y F.obj Z) :
            F.preimage (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (F.preimage f) (F.preimage g)
            @[simp]

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

            Equations
            Instances For

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

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

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

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

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

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

                  Equations
                  Instances For

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

                    Equations
                    Instances For

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

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

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

                          Equations
                          Instances For
                            def CategoryTheory.Faithful.div {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 E) (G : CategoryTheory.Functor D E) [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)) :

                            “Divide” a functor by a faithful functor.

                            Equations
                            Instances For
                              theorem CategoryTheory.Faithful.div_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 E) [CategoryTheory.Faithful F] (G : CategoryTheory.Functor D E) [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)) :
                              theorem CategoryTheory.Faithful.div_faithful {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 E) [CategoryTheory.Faithful F] (G : CategoryTheory.Functor D E) [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)) :

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

                              Equations
                              Instances For