Documentation

TauCeti.CategoryTheory.Core

Functors into the core of a category #

A functor F : D ⥤ C sending every morphism of D to an isomorphism of C factors through the core Core C, the groupoid of objects of C and isomorphisms between them. Mathlib's CategoryTheory.Core.functorToCore is the case where D is a groupoid.

source
noncomputable def CategoryTheory.Core.functorToCoreOfIsIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor D C) (hF : ∀ ⦃X Y : D⦄ (f : X ⟶ Y), IsIso (F.map f)) :
Functor D (Core C)

A functor sending every morphism to an isomorphism, as a functor to the core.

Instances For
    source
    @[simp]
    theorem CategoryTheory.Core.functorToCoreOfIsIso_map_iso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor D C) (hF : ∀ ⦃X Y : D⦄ (f : X ⟶ Y), IsIso (F.map f)) {X✝ Y✝ : D} (f : X✝ ⟶ Y✝) :
    ((functorToCoreOfIsIso F hF).map f).iso = asIso (F.map f)
    source
    @[simp]
    theorem CategoryTheory.Core.functorToCoreOfIsIso_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor D C) (hF : ∀ ⦃X Y : D⦄ (f : X ⟶ Y), IsIso (F.map f)) (X : D) :
    (functorToCoreOfIsIso F hF).obj X = { of := F.obj X }
    source
    @[simp]
    theorem CategoryTheory.Core.functorToCoreOfIsIso_comp_inclusion {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor D C) (hF : ∀ ⦃X Y : D⦄ (f : X ⟶ Y), IsIso (F.map f)) :
    (functorToCoreOfIsIso F hF).comp (inclusion C) = F
    source
    theorem CategoryTheory.Core.functorToCoreOfIsIso_comp_left {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (G : Functor E D) (F : Functor D C) (hF : ∀ ⦃X Y : D⦄ (f : X ⟶ Y), IsIso (F.map f)) :
    functorToCoreOfIsIso (G.comp F) ⋯ = G.comp (functorToCoreOfIsIso F hF)

    The functor functorToCoreOfIsIso (G ⋙ F) factors through functorToCoreOfIsIso F.

    source
    @[simp]
    theorem CategoryTheory.Core.functorToCoreOfIsIso_comp_inclusion_self {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor D (Core C)) :
    functorToCoreOfIsIso (G.comp (inclusion C)) ⋯ = G

    A functor to the core is recovered from its composite with the inclusion of the core.