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.

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

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

Equations

• CategoryTheory.Core C = C

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

Equations

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

@[simp]

theorem CategoryTheory.Core.id_hom {C : Type u₁} [Category.{v₁, u₁} C] (X : C) : (CategoryStruct.id X).hom = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Core.comp_hom {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : Core C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom

theorem CategoryTheory.Core.hom_ext {C : Type u₁} [Category.{v₁, u₁} C] {X Y : Core C} {f g : X ⟶ Y} (h : f.hom = g.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.hom = g.hom

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

• CategoryTheory.Core.inclusion C = { obj := id, map := fun {X Y : CategoryTheory.Core C} (f : X ⟶ Y) => f.hom, map_id := ⋯, map_comp := ⋯ }

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

@[simp]

theorem CategoryTheory.Core.inclusion_obj (C : Type u₁) [Category.{v₁, u₁} C] (a : Core C) : (inclusion C).obj a = a

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

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

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

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

• CategoryTheory.Core.forgetFunctorToCore = (CategoryTheory.whiskeringRight G (CategoryTheory.Core C) C).obj (CategoryTheory.Core.inclusion C)

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

• F.core = CategoryTheory.Core.functorToCore ((CategoryTheory.Core.inclusion C).comp F)

@[simp]

theorem CategoryTheory.Functor.core_map_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).hom = F.map f.hom

@[simp]

theorem CategoryTheory.Functor.core_map_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).inv = F.map (CategoryTheory.inv f).hom

@[simp]

theorem CategoryTheory.Functor.core_obj {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 = F.obj X

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

• CategoryTheory.Functor.coreId C = CategoryTheory.Iso.refl (CategoryTheory.Functor.id C).core

@[simp]

theorem CategoryTheory.Functor.coreId_inv_app (C : Type u₁) [Category.{v₁, u₁} C] (X : Core C) : (coreId C).inv.app X = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Functor.coreId_hom_app (C : Type u₁) [Category.{v₁, u₁} C] (X : Core C) : (coreId C).hom.app X = CategoryStruct.id X

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

• F.coreComp G = CategoryTheory.Iso.refl (F.comp G).core

@[simp]

theorem CategoryTheory.Functor.coreComp_inv_app {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 = CategoryStruct.id (G.obj (F.obj X))

@[simp]

theorem CategoryTheory.Functor.coreComp_hom_app {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 = CategoryStruct.id (G.obj (F.obj X))

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

• α.core = CategoryTheory.NatIso.ofComponents (fun (x : CategoryTheory.Core C) => (CategoryTheory.Groupoid.isoEquivHom (F.core.obj x) (G.core.obj x)).symm (α.app x)) ⋯

@[simp]

theorem CategoryTheory.Iso.core_inv_app {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 = CategoryTheory.inv (α.app X)

@[simp]

theorem CategoryTheory.Iso.core_hom_app {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 = α.app X

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

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

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) : (isoWhiskerLeft F η).core = F.coreComp G ≪≫ isoWhiskerLeft F.core η.core ≪≫ (F.coreComp H).symm

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) : (isoWhiskerRight η H).core = F.coreComp H ≪≫ isoWhiskerRight η.core H.core ≪≫ (G.coreComp H).symm

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 ≪≫ isoWhiskerRight (Functor.coreId C) F.core ≪≫ F.core.leftUnitor

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) ≪≫ isoWhiskerLeft F.core (Functor.coreId D) ≪≫ F.core.rightUnitor

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 ≪≫ isoWhiskerRight (F.coreComp G) H.core ≪≫ F.core.associator G.core H.core ≪≫ (isoWhiskerLeft F.core (G.coreComp H)).symm ≪≫ (F.coreComp (G.comp H)).symm

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

• E.core = { functor := E.functor.core, inverse := E.inverse.core, unitIso := E.unitIso.core, counitIso := E.counitIso.core, functor_unitIso_comp := ⋯ }

@[simp]

theorem CategoryTheory.Equivalence.core_inverse_obj {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 = E.inverse.obj X

@[simp]

theorem CategoryTheory.Equivalence.core_functor_map_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).hom = E.functor.map f.hom

@[simp]

theorem CategoryTheory.Equivalence.core_unitIso_inv_app_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).inv = E.unitIso.hom.app X

@[simp]

theorem CategoryTheory.Equivalence.core_unitIso_inv_app_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).hom = E.unitIso.inv.app X

@[simp]

theorem CategoryTheory.Equivalence.core_counitIso_hom_app_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).inv = E.counitIso.inv.app X

@[simp]

theorem CategoryTheory.Equivalence.core_inverse_map_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).inv = E.inverse.map (inv f).hom

@[simp]

theorem CategoryTheory.Equivalence.core_functor_obj {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 = E.functor.obj X

@[simp]

theorem CategoryTheory.Equivalence.core_functor_map_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).inv = E.functor.map (inv f).hom

@[simp]

theorem CategoryTheory.Equivalence.core_counitIso_hom_app_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).hom = E.counitIso.hom.app X

@[simp]

theorem CategoryTheory.Equivalence.core_counitIso_inv_app_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).hom = E.counitIso.inv.app X

@[simp]

theorem CategoryTheory.Equivalence.core_inverse_map_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).hom = E.inverse.map f.hom

@[simp]

theorem CategoryTheory.Equivalence.core_unitIso_hom_app_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).inv = E.unitIso.inv.app X

@[simp]

theorem CategoryTheory.Equivalence.core_counitIso_inv_app_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).inv = E.counitIso.hom.app X

@[simp]

theorem CategoryTheory.Equivalence.core_unitIso_hom_app_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).hom = E.unitIso.hom.app X

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

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

@[simp]

theorem CategoryTheory.coreFunctor_obj_map_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).hom = F.map f.hom

@[simp]

theorem CategoryTheory.coreFunctor_obj_obj (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 = F.obj X

@[simp]

theorem CategoryTheory.coreFunctor_map_app_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).hom = η.hom.app X

@[simp]

theorem CategoryTheory.coreFunctor_map_app_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).inv = η.inv.app X

@[simp]

theorem CategoryTheory.coreFunctor_obj_map_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).inv = F.map (inv f).hom

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.