Documentation

Mathlib.CategoryTheory.FullSubcategory

Induced categories and full subcategories #

Given a category D and a function F : C → D from a type C to the objects of D, there is an essentially unique way to give C a category structure such that F becomes a fully faithful functor, namely by taking $$ Hom_C(X, Y) = Hom_D(FX, FY) $$. We call this the category induced from D along F.

As a special case, if C is a subtype of D, this produces the full subcategory of D on the objects belonging to C. In general the induced category is equivalent to the full subcategory of D on the image of F.

Implementation notes #

It looks odd to make D an explicit argument of InducedCategory, when it is determined by the argument F anyways. The reason to make D explicit is in order to control its syntactic form, so that instances like InducedCategory.has_forget₂ (elsewhere) refer to the correct form of D. This is used to set up several algebraic categories like

def CommMon : Type (u+1) := InducedCategory Mon (Bundled.map @CommMonoid.toMonoid) -- not InducedCategory (Bundled Monoid) (Bundled.map @CommMonoid.toMonoid), -- even though MonCat = Bundled Monoid!

def CategoryTheory.InducedCategory {C : Type u₁} (D : Type u₂) (_F : CD) :
Type u₁

InducedCategory D F, where F : C → D, is a typeclass synonym for C, which provides a category structure so that the morphisms X ⟶ Y are the morphisms in D from F X to F Y.

Equations
Instances For
    instance CategoryTheory.InducedCategory.hasCoeToSort {C : Type u₁} {D : Type u₂} (F : CD) {α : Sort u_1} [CoeSort D α] :
    Equations
    @[simp]
    theorem CategoryTheory.inducedFunctor_map {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] (F : CD) :
    ∀ {X Y : CategoryTheory.InducedCategory D F} (f : X Y), (CategoryTheory.inducedFunctor F).map f = f
    @[simp]
    theorem CategoryTheory.inducedFunctor_obj {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] (F : CD) :
    ∀ (a : C), (CategoryTheory.inducedFunctor F).obj a = F a

    The forgetful functor from an induced category to the original category, forgetting the extra data.

    Equations
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      theorem CategoryTheory.FullSubcategory.ext {C : Type u₁} {Z : CProp} (x : CategoryTheory.FullSubcategory Z) (y : CategoryTheory.FullSubcategory Z) (obj : x.obj = y.obj) :
      x = y
      structure CategoryTheory.FullSubcategory {C : Type u₁} (Z : CProp) :
      Type u₁

      A subtype-like structure for full subcategories. Morphisms just ignore the property. We don't use actual subtypes since the simp-normal form ↑X of X.val does not work well for full subcategories.

      See . We do not define 'strictly full' subcategories.

      • obj : C

        The category of which this is a full subcategory

      • property : Z self.obj

        The predicate satisfied by all objects in this subcategory

      Instances For

        The forgetful functor from a full subcategory into the original category ("forgetting" the condition).

        Equations
        Instances For
          @[simp]
          theorem CategoryTheory.FullSubcategory.map_obj_obj {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {Z : CProp} {Z' : CProp} (h : ∀ ⦃X : C⦄, Z XZ' X) (X : CategoryTheory.FullSubcategory Z) :
          @[simp]
          theorem CategoryTheory.FullSubcategory.map_map {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {Z : CProp} {Z' : CProp} (h : ∀ ⦃X : C⦄, Z XZ' X) :

          An implication of predicates Z → Z' induces a functor between full subcategories.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            instance CategoryTheory.FullSubcategory.full_map {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {Z : CProp} {Z' : CProp} (h : ∀ ⦃X : C⦄, Z XZ' X) :
            Equations
            • One or more equations did not get rendered due to their size.
            Equations
            • =
            @[simp]
            theorem CategoryTheory.FullSubcategory.lift_obj_obj {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (P : DProp) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) (X : C) :
            ((CategoryTheory.FullSubcategory.lift P F hF).obj X).obj = F.obj X
            @[simp]
            theorem CategoryTheory.FullSubcategory.lift_map {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (P : DProp) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) :
            ∀ {X Y : C} (f : X Y), (CategoryTheory.FullSubcategory.lift P F hF).map f = F.map f

            A functor which maps objects to objects satisfying a certain property induces a lift through the full subcategory of objects satisfying that property.

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

              Composing the lift of a functor through a full subcategory with the inclusion yields the original functor. This is actually true definitionally.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem CategoryTheory.fullSubcategoryInclusion_map_lift_map {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (P : DProp) (F : CategoryTheory.Functor C D) (hF : ∀ (X : C), P (F.obj X)) {X : C} {Y : C} (f : X Y) :