Inserter categories

Let F G : C ⥤ D be a parallel pair of functors. In this file, we define a category Inserter F G. Objects of Inserter F G correspond to pairs (K : C) × (F.obj K ⟶ G.obj K). Such categories can be used to encode data such as algebra for endofunctors. They are also a basic building block for bicategorical limits of categories.

Main constructions

• Inserter F G: the inserter category
• Inserter.proj: the projection functor Inserter F G ⥤ C
• Inserter.τ: the structure morphism of the inserter as a natural transformation proj F G ⋙ F ⟶ proj F G ⋙ G.

References

• nLab, inserter.

Future work

• Link Inserter F (𝟭 C) with Endofunctor.Algebra F when F is an endofunctor.
• Link Inserter (𝟭 C) F with Endofunctor.Coalgebra F when F is an endofunctor.
• Show that Inserter F G is an accessible category when F and G are accessible functors.

structure CategoryTheory.Inserter {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F G : Functor C D) : Type (max u_1 v_2)

The inserter of a pair of parallel functors F G : C ⥤ D is the category of arrows F.obj K ⟶ G.obj K, with morphisms K ⟶ K' making the obvious square commute as morphims.

• obj : C

  the object of C underlying the object

• hom : F.obj self.obj ⟶ G.obj self.obj

  the morphism F.obj obj ⟶ G.obj obj corresponding to the object

structure CategoryTheory.Inserter.Hom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F G : Functor C D} (x y : Inserter F G) : Type v_1

Morphisms in the inserter category are given by morphisms between the underlying objects that make the obvious square commute.

• hom : x.obj ⟶ y.obj

  The morphism between the underlying objects.

• comm : CategoryStruct.comp (F.map self.hom) y.hom = CategoryStruct.comp x.hom (G.map self.hom)

theorem CategoryTheory.Inserter.Hom.ext_iff {C : Type u_1} {D : Type u_2} {inst✝ : Category.{v_1, u_1} C} {inst✝¹ : Category.{v_2, u_2} D} {F G : Functor C D} {x y : Inserter F G} {x✝ y✝ : x.Hom y} : x✝ = y✝ ↔ x✝.hom = y✝.hom

theorem CategoryTheory.Inserter.Hom.ext {C : Type u_1} {D : Type u_2} {inst✝ : Category.{v_1, u_1} C} {inst✝¹ : Category.{v_2, u_2} D} {F G : Functor C D} {x y : Inserter F G} {x✝ y✝ : x.Hom y} (hom : x✝.hom = y✝.hom) : x✝ = y✝

@[instance_reducible]

instance CategoryTheory.Inserter.instCategory {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F G : Functor C D} : Category.{v_1, max v_2 u_1} (Inserter F G)

Equations

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

@[simp]

theorem CategoryTheory.Inserter.id_hom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F G : Functor C D} (x : Inserter F G) : (CategoryStruct.id x).hom = CategoryStruct.id x.obj

@[simp]

theorem CategoryTheory.Inserter.comp_hom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F G : Functor C D} {x y z : Inserter F G} (f : x ⟶ y) (g : y ⟶ z) : (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom

theorem CategoryTheory.Inserter.comp_hom_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F G : Functor C D} {x y z : Inserter F G} (f : x ⟶ y) (g : y ⟶ z) {Z : C} (h : z.obj ⟶ Z) : CategoryStruct.comp (CategoryStruct.comp f g).hom h = CategoryStruct.comp f.hom (CategoryStruct.comp g.hom h)

@[simp]

theorem CategoryTheory.Inserter.comm {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F G : Functor C D} {x y : Inserter F G} (f : x ⟶ y) : CategoryStruct.comp (F.map f.hom) y.hom = CategoryStruct.comp x.hom (G.map f.hom)

@[simp]

theorem CategoryTheory.Inserter.comm_assoc {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F G : Functor C D} {x y : Inserter F G} (f : x ⟶ y) {Z : D} (h : G.obj y.obj ⟶ Z) : CategoryStruct.comp (F.map f.hom) (CategoryStruct.comp y.hom h) = CategoryStruct.comp x.hom (CategoryStruct.comp (G.map f.hom) h)

theorem CategoryTheory.Inserter.hom_ext {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F G : Functor C D} {x y : Inserter F G} {f g : x ⟶ y} (h : f.hom = g.hom) : f = g

theorem CategoryTheory.Inserter.hom_ext_iff {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F G : Functor C D} {x y : Inserter F G} {f g : x ⟶ y} : f = g ↔ f.hom = g.hom

@[implicit_reducible]

def CategoryTheory.Inserter.proj {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F G : Functor C D) : Functor (Inserter F G) C

The projection Inserter F G ⥤ C that sends an object to its underlying object of C.

Equations

• CategoryTheory.Inserter.proj F G = { obj := fun (x : CategoryTheory.Inserter F G) => x.obj, map := fun {X Y : CategoryTheory.Inserter F G} (f : X ⟶ Y) => f.hom, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.Inserter.proj_map {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F G : Functor C D) {X✝ Y✝ : Inserter F G} (f : X✝ ⟶ Y✝) : (proj F G).map f = f.hom

@[simp]

theorem CategoryTheory.Inserter.proj_obj {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F G : Functor C D) (x : Inserter F G) : (proj F G).obj x = x.obj

instance CategoryTheory.Inserter.instFaithfulProj {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F G : Functor C D) : (proj F G).Faithful

def CategoryTheory.Inserter.τ {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F G : Functor C D) : (proj F G).comp F ⟶ (proj F G).comp G

The structure morphisms of objects of the inserter assemble into a natural transformation proj ⋙ F ⟶ proj ⋙ G.

Equations

• CategoryTheory.Inserter.τ F G = { app := fun (x : CategoryTheory.Inserter F G) => x.hom, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Inserter.τ_app {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F G : Functor C D) (x : Inserter F G) : (τ F G).app x = x.hom

def CategoryTheory.Inserter.mkIso {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F G : Functor C D} {E E' : Inserter F G} (e : E.obj ≅ E'.obj) (he : CategoryStruct.comp (F.map e.hom) E'.hom = CategoryStruct.comp E.hom (G.map e.hom) := by cat_disch) : E ≅ E'

Construct an isomorphism of inserters from an isomorphism of the underlying objects

Equations

• CategoryTheory.Inserter.mkIso e he = { hom := { hom := e.hom, comm := he }, inv := { hom := e.inv, comm := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Inserter.mkIso_hom_hom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F G : Functor C D} {E E' : Inserter F G} (e : E.obj ≅ E'.obj) (he : CategoryStruct.comp (F.map e.hom) E'.hom = CategoryStruct.comp E.hom (G.map e.hom) := by cat_disch) : (mkIso e he).hom.hom = e.hom

@[simp]

theorem CategoryTheory.Inserter.mkIso_inv_hom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] {F G : Functor C D} {E E' : Inserter F G} (e : E.obj ≅ E'.obj) (he : CategoryStruct.comp (F.map e.hom) E'.hom = CategoryStruct.comp E.hom (G.map e.hom) := by cat_disch) : (mkIso e he).inv.hom = e.inv

instance CategoryTheory.Inserter.instIsIsoHom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F G : Functor C D) {E E' : Inserter F G} (f : E ⟶ E') [IsIso f] : IsIso f.hom

@[simp]

theorem CategoryTheory.Inserter.inv_hom {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F G : Functor C D) {E E' : Inserter F G} (f : E ⟶ E') [IsIso f] : (inv f).hom = inv f.hom

instance CategoryTheory.Inserter.instReflectsIsomorphismsProj {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F G : Functor C D) : (proj F G).ReflectsIsomorphisms

theorem CategoryTheory.Inserter.isIso_iff {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F G : Functor C D) {E E' : Inserter F G} (f : E ⟶ E') : IsIso f ↔ IsIso f.hom