Documentation

Mathlib.CategoryTheory.Core

The core of a category #

The core of a category C is the (non-full) subcategory of C consisting of all objects, and all isomorphisms. We construct it as a CategoryTheory.Groupoid.

CategoryTheory.Core.inclusion : Core C ⥤ C gives the faithful inclusion into the original category.

Any functor F from a groupoid G into C factors through CategoryTheory.Core C, but this is not functorial with respect to F.

structure CategoryTheory.Core (C : Type u₁) :
Type u₁

The core of a category C is the groupoid whose morphisms are all the isomorphisms of C.

  • of : C

    The object of the base category underlying an object in Core C.

Instances For
    structure CategoryTheory.CoreHom {C : Type u₁} [Category.{v₁, u₁} C] (X Y : Core C) :
    Type v₁

    The hom-type between two objects of Core C. It is defined as a one-field structure to prevent defeq abuses.

    • iso : X.of Y.of

      The isomorphism of objects of C underlying a morphism in Core C.

    Instances For
      theorem CategoryTheory.CoreHom.ext {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {X Y : Core C} {x y : CoreHom X Y} (iso : x.iso = y.iso) :
      x = y
      theorem CategoryTheory.CoreHom.ext_iff {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {X Y : Core C} {x y : CoreHom X Y} :
      x = y x.iso = y.iso
      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem CategoryTheory.coreCategory_comp_iso_inv {C : Type u₁} [Category.{v₁, u₁} C] {X✝ Y✝ Z✝ : Core C} (f : CoreHom X✝ Y✝) (g : CoreHom Y✝ Z✝) :
      @[simp]
      theorem CategoryTheory.coreCategory_inv_iso_inv {C : Type u₁} [Category.{v₁, u₁} C] {x✝ x✝¹ : Core C} (f : CoreHom x✝ x✝¹) :
      @[simp]
      theorem CategoryTheory.coreCategory_comp_iso_hom {C : Type u₁} [Category.{v₁, u₁} C] {X✝ Y✝ Z✝ : Core C} (f : CoreHom X✝ Y✝) (g : CoreHom Y✝ Z✝) :
      @[simp]
      theorem CategoryTheory.coreCategory_inv_iso_hom {C : Type u₁} [Category.{v₁, u₁} C] {x✝ x✝¹ : Core C} (f : CoreHom x✝ x✝¹) :
      @[simp]
      theorem CategoryTheory.coreCategory_comp_iso {C : Type u₁} [Category.{v₁, u₁} C] {x y z : Core C} (f : x y) (g : y z) :

      The core of a category is naturally included in the category.

      Equations
      Instances For
        @[simp]
        theorem CategoryTheory.Core.inclusion_obj (C : Type u₁) [Category.{v₁, u₁} C] (self : Core C) :
        (inclusion C).obj self = self.of
        @[simp]
        theorem CategoryTheory.Core.inclusion_map (C : Type u₁) [Category.{v₁, u₁} C] {X✝ Y✝ : Core C} (f : X✝ Y✝) :
        theorem CategoryTheory.Core.hom_ext {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Core C} {f g : X Y} (h : f.iso.hom = g.iso.hom) :
        f = g
        theorem CategoryTheory.Core.hom_ext_iff {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Core C} {f g : X Y} :
        f = g f.iso.hom = g.iso.hom

        A functor from a groupoid to a category C factors through the core of C.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem CategoryTheory.Core.functorToCore_map_iso_inv {C : Type u₁} [Category.{v₁, u₁} C] {G : Type u₂} [Groupoid G] (F : Functor G C) {X✝ Y✝ : G} (f : X✝ Y✝) :
          ((functorToCore F).map f).iso.inv = inv (F.map f)
          @[simp]
          theorem CategoryTheory.Core.functorToCore_map_iso_hom {C : Type u₁} [Category.{v₁, u₁} C] {G : Type u₂} [Groupoid G] (F : Functor G C) {X✝ Y✝ : G} (f : X✝ Y✝) :
          @[simp]
          theorem CategoryTheory.Core.functorToCore_obj_of {C : Type u₁} [Category.{v₁, u₁} C] {G : Type u₂} [Groupoid G] (F : Functor G C) (X : G) :
          ((functorToCore F).obj X).of = F.obj X

          We can functorially associate to any functor from a groupoid to the core of a category C, a functor from the groupoid to C, simply by composing with the embedding Core C ⥤ C.

          Equations
          Instances For
            @[simp]
            theorem CategoryTheory.Core.forgetFunctorToCore_map_app {C : Type u₁} [Category.{v₁, u₁} C] {G : Type u₂} [Groupoid G] {X✝ Y✝ : Functor G (Core C)} (α : X✝ Y✝) (X : G) :
            @[simp]
            theorem CategoryTheory.Core.forgetFunctorToCore_obj_map {C : Type u₁} [Category.{v₁, u₁} C] {G : Type u₂} [Groupoid G] (F : Functor G (Core C)) {X✝ Y✝ : G} (f : X✝ Y✝) :
            @[simp]

            A functor C ⥤ D induces a functor Core C ⥤ Core D.

            Equations
            Instances For
              @[simp]
              theorem CategoryTheory.Functor.core_map_iso_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X✝ Y✝ : Core C} (f : X✝ Y✝) :
              (F.core.map f).iso.inv = F.map f.iso.inv
              @[simp]
              theorem CategoryTheory.Functor.core_map_iso_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X✝ Y✝ : Core C} (f : X✝ Y✝) :
              (F.core.map f).iso.hom = F.map f.iso.hom
              @[simp]
              theorem CategoryTheory.Functor.core_obj_of {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (X : Core C) :
              (F.core.obj X).of = F.obj X.of

              The core of the identity functor is the identity functor on the cores.

              Equations
              Instances For

                The core of the composition of F and G is the composition of the cores.

                Equations
                Instances For
                  @[simp]
                  @[simp]
                  @[simp]
                  @[simp]
                  def CategoryTheory.Iso.core {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F G) :

                  A natural isomorphism of functors induces a natural isomorphism between their cores.

                  Equations
                  Instances For
                    @[simp]
                    theorem CategoryTheory.Iso.core_hom_app_iso_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F G) (X : Core C) :
                    (α.core.hom.app X).iso.hom = α.hom.app X.of
                    @[simp]
                    theorem CategoryTheory.Iso.core_hom_app_iso_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F G) (X : Core C) :
                    (α.core.hom.app X).iso.inv = α.inv.app X.of
                    @[simp]
                    theorem CategoryTheory.Iso.core_inv_app_iso_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F G) (X : Core C) :
                    (α.core.inv.app X).iso.hom = α.inv.app X.of
                    @[simp]
                    theorem CategoryTheory.Iso.core_inv_app_iso_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F G) (X : Core C) :
                    (α.core.inv.app X).iso.inv = α.hom.app X.of
                    @[simp]
                    theorem CategoryTheory.Iso.coreComp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G H : Functor C D} (α : F G) (β : G H) :
                    (α ≪≫ β).core = α.core ≪≫ β.core
                    @[simp]

                    Equivalent categories have equivalent cores.

                    Equations
                    Instances For
                      @[simp]
                      theorem CategoryTheory.Equivalence.core_inverse_map_iso_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : C D) {X✝ Y✝ : Core D} (f : X✝ Y✝) :
                      @[simp]
                      theorem CategoryTheory.Equivalence.core_functor_map_iso_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : C D) {X✝ Y✝ : Core C} (f : X✝ Y✝) :
                      @[simp]
                      theorem CategoryTheory.Equivalence.core_functor_map_iso_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : C D) {X✝ Y✝ : Core C} (f : X✝ Y✝) :
                      @[simp]
                      theorem CategoryTheory.Equivalence.core_inverse_map_iso_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : C D) {X✝ Y✝ : Core D} (f : X✝ Y✝) :

                      Taking the core of a functor is functorial if we discard non-invertible natural transformations.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        theorem CategoryTheory.coreFunctor_map_app_iso_inv (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] {X✝ Y✝ : Core (Functor C D)} (η : X✝ Y✝) (X : Core C) :
                        (((coreFunctor C D).map η).app X).iso.inv = η.iso.inv.app X.of
                        @[simp]
                        theorem CategoryTheory.coreFunctor_obj_map_iso_inv (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (F : Core (Functor C D)) {X✝ Y✝ : Core C} (f : X✝ Y✝) :
                        (((coreFunctor C D).obj F).map f).iso.inv = F.of.map f.iso.inv
                        @[simp]
                        theorem CategoryTheory.coreFunctor_obj_map_iso_hom (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (F : Core (Functor C D)) {X✝ Y✝ : Core C} (f : X✝ Y✝) :
                        (((coreFunctor C D).obj F).map f).iso.hom = F.of.map f.iso.hom
                        @[simp]
                        theorem CategoryTheory.coreFunctor_obj_obj_of (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] (F : Core (Functor C D)) (X : Core C) :
                        (((coreFunctor C D).obj F).obj X).of = F.of.obj X.of
                        @[simp]
                        theorem CategoryTheory.coreFunctor_map_app_iso_hom (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] {X✝ Y✝ : Core (Functor C D)} (η : X✝ Y✝) (X : Core C) :
                        (((coreFunctor C D).map η).app X).iso.hom = η.iso.hom.app X.of
                        def CategoryTheory.ofEquivFunctor (m : Type u₁ → Type u₂) [EquivFunctor m] :
                        Functor (Core (Type u₁)) (Core (Type u₂))

                        ofEquivFunctor m lifts a type-level EquivFunctor to a categorical functor Core (Type u₁) ⥤ Core (Type u₂).

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