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.

source

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

source

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

source

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

source

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

source

instance CategoryTheory.coreCategory {C : Type u₁} [Category.{v₁, u₁} C] :

Groupoid (Core C)

Equations

source

@[simp]

theorem CategoryTheory.coreCategory_inv_iso_inv {C : Type u₁} [Category.{v₁, u₁} C] {x✝ x✝¹ : Core C} (f : CoreHom x✝ x✝¹) :

(Groupoid.inv f).iso.inv = f.iso.hom

source

@[simp]

theorem CategoryTheory.coreCategory_id_iso_inv {C : Type u₁} [Category.{v₁, u₁} C] (X : Core C) :

(CategoryStruct.id X).iso.inv = CategoryStruct.id X.of

source

@[simp]

theorem CategoryTheory.coreCategory_id_iso_hom {C : Type u₁} [Category.{v₁, u₁} C] (X : Core C) :

(CategoryStruct.id X).iso.hom = CategoryStruct.id X.of

source

@[simp]

theorem CategoryTheory.coreCategory_inv_iso_hom {C : Type u₁} [Category.{v₁, u₁} C] {x✝ x✝¹ : Core C} (f : CoreHom x✝ x✝¹) :

(Groupoid.inv f).iso.hom = f.iso.inv

source

@[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✝) :

(CategoryStruct.comp f g).iso.hom = CategoryStruct.comp f.iso.hom g.iso.hom

source

@[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✝) :

(CategoryStruct.comp f g).iso.inv = CategoryStruct.comp g.iso.inv f.iso.inv

source

@[simp]

theorem CategoryTheory.coreCategory_comp_iso {C : Type u₁} [Category.{v₁, u₁} C] {x y z : Core C} (f : x ⟶ y) (g : y ⟶ z) :

(CategoryStruct.comp f g).iso = f.iso ≪≫ g.iso

source

def CategoryTheory.Core.inclusion (C : Type u₁) [Category.{v₁, u₁} C] :

Functor (Core C) C

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

Equations

Instances For

source

@[simp]

theorem CategoryTheory.Core.inclusion_map (C : Type u₁) [Category.{v₁, u₁} C] {X✝ Y✝ : Core C} (f : X✝ ⟶ Y✝) :

(inclusion C).map f = f.iso.hom

source

@[simp]

theorem CategoryTheory.Core.inclusion_obj (C : Type u₁) [Category.{v₁, u₁} C] (self : Core C) :

(inclusion C).obj self = self.of

source

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

source

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

source

def CategoryTheory.Core.isoMk {C : Type u₁} [Category.{v₁, u₁} C] {x y : Core C} (e : x.of ≅ y.of) :

x ≅ y

Construct an isomorphism in Core C from an isomorphism in C.

Equations

Instances For

source

@[simp]

theorem CategoryTheory.Core.isoMk_inv_iso {C : Type u₁} [Category.{v₁, u₁} C] {x y : Core C} (e : x.of ≅ y.of) :

(isoMk e).inv.iso = e.symm

source

@[simp]

theorem CategoryTheory.Core.isoMk_hom_iso {C : Type u₁} [Category.{v₁, u₁} C] {x y : Core C} (e : x.of ≅ y.of) :

(isoMk e).hom.iso = e

source

instance CategoryTheory.Core.instFaithfulInclusion (C : Type u₁) [Category.{v₁, u₁} C] :

(inclusion C).Faithful

source

def CategoryTheory.Core.functorToCore {C : Type u₁} [Category.{v₁, u₁} C] {G : Type u₂} [Groupoid G] (F : Functor G C) :

Functor G (Core C)

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

Equations

Instances For

source

@[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

source

@[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✝) :

((functorToCore F).map f).iso.hom = F.map f

source

@[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)

source

def CategoryTheory.Core.forgetFunctorToCore {C : Type u₁} [Category.{v₁, u₁} C] {G : Type u₂} [Groupoid G] :

Functor (Functor G (Core C)) (Functor G C)

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

source

@[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✝) :

(forgetFunctorToCore.obj F).map f = (F.map f).iso.hom

source

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

(forgetFunctorToCore.map α).app X = (α.app X).iso.hom

source

@[simp]

theorem CategoryTheory.Core.forgetFunctorToCore_obj_obj {C : Type u₁} [Category.{v₁, u₁} C] {G : Type u₂} [Groupoid G] (F : Functor G (Core C)) (X : G) :

(forgetFunctorToCore.obj F).obj X = (F.obj X).of

source

def CategoryTheory.Functor.core {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) :

Functor (Core C) (Core D)

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

Equations

Instances For

source

@[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

source

@[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

source

@[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

source

def CategoryTheory.Functor.coreId (C : Type u₁) [Category.{v₁, u₁} C] :

(Functor.id C).core ≅ Functor.id (Core C)

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

Equations

Instances For

source

@[simp]

theorem CategoryTheory.Functor.coreId_hom_app_iso_hom (C : Type u₁) [Category.{v₁, u₁} C] (X : Core C) :

((coreId C).hom.app X).iso.hom = CategoryStruct.id X.of

source

@[simp]

theorem CategoryTheory.Functor.coreId_hom_app_iso_inv (C : Type u₁) [Category.{v₁, u₁} C] (X : Core C) :

((coreId C).hom.app X).iso.inv = CategoryStruct.id X.of

source

@[simp]

theorem CategoryTheory.Functor.coreId_inv_app_iso_hom (C : Type u₁) [Category.{v₁, u₁} C] (X : Core C) :

((coreId C).inv.app X).iso.hom = CategoryStruct.id X.of

source

@[simp]

theorem CategoryTheory.Functor.coreId_inv_app_iso_inv (C : Type u₁) [Category.{v₁, u₁} C] (X : Core C) :

((coreId C).inv.app X).iso.inv = CategoryStruct.id X.of

source

def CategoryTheory.Functor.coreComp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) :

(F.comp G).core ≅ F.core.comp G.core

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

Equations

Instances For

source

@[simp]

theorem CategoryTheory.Functor.coreComp_inv_app_iso_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) (X : Core C) :

((F.coreComp G).inv.app X).iso.hom = CategoryStruct.id (G.obj (F.obj X.of))

source

@[simp]

theorem CategoryTheory.Functor.coreComp_hom_app_iso_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) (X : Core C) :

((F.coreComp G).hom.app X).iso.hom = CategoryStruct.id (G.obj (F.obj X.of))

source

@[simp]

theorem CategoryTheory.Functor.coreComp_inv_app_iso_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) (X : Core C) :

((F.coreComp G).inv.app X).iso.inv = CategoryStruct.id (G.obj (F.obj X.of))

source

@[simp]

theorem CategoryTheory.Functor.coreComp_hom_app_iso_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) (X : Core C) :

((F.coreComp G).hom.app X).iso.inv = CategoryStruct.id (G.obj (F.obj X.of))

source

def CategoryTheory.Functor.coreCompInclusionIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) :

F.core.comp (Core.inclusion D) ≅ (Core.inclusion C).comp F

The natural isomorphism

                  F.core
            Core C ⥤ Core D
 inclusion C  ‖          ‖  inclusion D
              V          V
              C    ⥤    D
                    F

thought of as pseudonaturality of inclusion, when viewing Core as a pseudofunctor.

Equations

Instances For

source

@[simp]

theorem CategoryTheory.Functor.coreCompInclusionIso_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (X : Core C) :

F.coreCompInclusionIso.inv.app X = CategoryStruct.id (F.obj X.of)

source

@[simp]

theorem CategoryTheory.Functor.coreCompInclusionIso_hom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) (X : Core C) :

F.coreCompInclusionIso.hom.app X = CategoryStruct.id (F.obj X.of)

source

theorem CategoryTheory.Functor.core_comp_inclusion {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) :

F.core.comp (Core.inclusion D) = (Core.inclusion C).comp F

source

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

F.core ≅ G.core

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

Equations

Instances For

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

@[simp]

theorem CategoryTheory.Iso.coreId {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} :

(refl F).core = refl F.core

source

theorem CategoryTheory.Iso.coreWhiskerLeft {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) {G H : Functor D E} (η : G ≅ H) :

(F.isoWhiskerLeft η).core = F.coreComp G ≪≫ F.core.isoWhiskerLeft η.core ≪≫ (F.coreComp H).symm

source

theorem CategoryTheory.Iso.coreWhiskerRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F G : Functor C D} (η : F ≅ G) (H : Functor D E) :

(Functor.isoWhiskerRight η H).core = F.coreComp H ≪≫ Functor.isoWhiskerRight η.core H.core ≪≫ (G.coreComp H).symm

source

theorem CategoryTheory.Iso.coreLeftUnitor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} :

F.leftUnitor.core = (Functor.id C).coreComp F ≪≫ Functor.isoWhiskerRight (Functor.coreId C) F.core ≪≫ F.core.leftUnitor

source

theorem CategoryTheory.Iso.coreRightUnitor {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} :

F.rightUnitor.core = F.coreComp (Functor.id D) ≪≫ F.core.isoWhiskerLeft (Functor.coreId D) ≪≫ F.core.rightUnitor

source

theorem CategoryTheory.Iso.coreAssociator {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {E' : Type u₄} [Category.{v₄, u₄} E'] (F : Functor C D) (G : Functor D E) (H : Functor E E') :

(F.associator G H).core = (F.comp G).coreComp H ≪≫ Functor.isoWhiskerRight (F.coreComp G) H.core ≪≫ F.core.associator G.core H.core ≪≫ (F.core.isoWhiskerLeft (G.coreComp H)).symm ≪≫ (F.coreComp (G.comp H)).symm

source

def CategoryTheory.Core.functorToCoreCompLeftIso {C : Type u₁} [Category.{v₁, u₁} C] {G : Type u₂} [Groupoid G] {G' : Type u₃} [Groupoid G'] (H : Functor G C) (F : Functor G' G) :

functorToCore (F.comp H) ≅ F.comp (functorToCore H)

The functor functorToCore (F ⋙ H) factors through functorToCore H.

Equations

Instances For

source

theorem CategoryTheory.Core.functorToCore_comp_left {C : Type u₁} [Category.{v₁, u₁} C] {G : Type u₂} [Groupoid G] {G' : Type u₃} [Groupoid G'] (H : Functor G C) (F : Functor G' G) :

functorToCore (F.comp H) = F.comp (functorToCore H)

source

def CategoryTheory.Core.functorToCoreCompRightIso {C : Type u₁} [Category.{v₁, u₁} C] {G : Type u₂} [Groupoid G] {C' : Type u₄} [Category.{v₄, u₄} C'] (H : Functor G C) (F : Functor C C') :

functorToCore (H.comp F) ≅ (functorToCore H).comp F.core

The functor functorToCore (H ⋙ F) factors through functorToCore H.

Equations

Instances For

source

theorem CategoryTheory.Core.functorToCore_comp_right {C : Type u₁} [Category.{v₁, u₁} C] {G : Type u₂} [Groupoid G] {C' : Type u₄} [Category.{v₄, u₄} C'] (H : Functor G C) (F : Functor C C') :

functorToCore (H.comp F) = (functorToCore H).comp F.core

source

def CategoryTheory.Core.inclusionCompFunctorToCoreIso {G : Type u₂} [Groupoid G] :

(inclusion G).comp (functorToCore (Functor.id G)) ≅ Functor.id (Core G)

The functor functorToCore (𝟭 G) is a section of inclusion G.

Equations

Instances For

source

theorem CategoryTheory.Core.inclusion_comp_functorToCore {G : Type u₂} [Groupoid G] :

(inclusion G).comp (functorToCore (Functor.id G)) = Functor.id (Core G)

source

def CategoryTheory.Core.functorToCoreInclusionIso {C : Type u₁} [Category.{v₁, u₁} C] :

functorToCore (inclusion C) ≅ Functor.id (Core C)

The functor functorToCore (inclusion C) is isomorphic to the identity on Core C.

Equations

Instances For

source

theorem CategoryTheory.Core.functorToCore_inclusion {C : Type u₁} [Category.{v₁, u₁} C] :

functorToCore (inclusion C) = Functor.id (Core C)

source

def CategoryTheory.Equivalence.core {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : C ≌ D) :

Core C ≌ Core D

Equivalent categories have equivalent cores.

Equations

Instances For

source

@[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✝) :

(E.core.inverse.map f).iso.hom = E.inverse.map f.iso.hom

source

@[simp]

theorem CategoryTheory.Equivalence.core_unitIso_hom_app_iso_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : C ≌ D) (X : Core C) :

(E.core.unitIso.hom.app X).iso.inv = E.unitIso.inv.app X.of

source

@[simp]

theorem CategoryTheory.Equivalence.core_counitIso_inv_app_iso_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : C ≌ D) (X : Core D) :

(E.core.counitIso.inv.app X).iso.hom = E.counitIso.inv.app X.of

source

@[simp]

theorem CategoryTheory.Equivalence.core_unitIso_hom_app_iso_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : C ≌ D) (X : Core C) :

(E.core.unitIso.hom.app X).iso.hom = E.unitIso.hom.app X.of

source

@[simp]

theorem CategoryTheory.Equivalence.core_counitIso_hom_app_iso_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : C ≌ D) (X : Core D) :

(E.core.counitIso.hom.app X).iso.hom = E.counitIso.hom.app X.of

source

@[simp]

theorem CategoryTheory.Equivalence.core_counitIso_hom_app_iso_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : C ≌ D) (X : Core D) :

(E.core.counitIso.hom.app X).iso.inv = E.counitIso.inv.app X.of

source

@[simp]

theorem CategoryTheory.Equivalence.core_functor_obj_of {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : C ≌ D) (X : Core C) :

(E.core.functor.obj X).of = E.functor.obj X.of

source

@[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✝) :

(E.core.functor.map f).iso.hom = E.functor.map f.iso.hom

source

@[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✝) :

(E.core.inverse.map f).iso.inv = E.inverse.map f.iso.inv

source

@[simp]

theorem CategoryTheory.Equivalence.core_inverse_obj_of {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : C ≌ D) (X : Core D) :

(E.core.inverse.obj X).of = E.inverse.obj X.of

source

@[simp]

theorem CategoryTheory.Equivalence.core_counitIso_inv_app_iso_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : C ≌ D) (X : Core D) :

(E.core.counitIso.inv.app X).iso.inv = E.counitIso.hom.app X.of

source

@[simp]

theorem CategoryTheory.Equivalence.core_unitIso_inv_app_iso_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : C ≌ D) (X : Core C) :

(E.core.unitIso.inv.app X).iso.hom = E.unitIso.inv.app X.of

source

@[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✝) :

(E.core.functor.map f).iso.inv = E.functor.map f.iso.inv

source

@[simp]

theorem CategoryTheory.Equivalence.core_unitIso_inv_app_iso_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (E : C ≌ D) (X : Core C) :

(E.core.unitIso.inv.app X).iso.inv = E.unitIso.hom.app X.of

source

def CategoryTheory.coreFunctor (C : Type u₁) [Category.{v₁, u₁} C] (D : Type u₂) [Category.{v₂, u₂} D] :

Functor (Core (Functor C D)) (Functor (Core C) (Core D))

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

Equations

Instances For

source

@[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

source

@[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

source

@[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

source

@[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

source

@[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

source

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

Instances For

Documentation

Mathlib.CategoryTheory.Core

The core of a category #