Locally discrete bicategories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A category C can be promoted to a strict bicategory locally_discrete C. The objects and the 1-morphisms in locally_discrete C are the same as the objects and the morphisms, respectively, in C, and the 2-morphisms in locally_discrete C are the equalities between 1-morphisms. In other words, the category consisting of the 1-morphisms between each pair of objects X and Y in locally_discrete C is defined as the discrete category associated with the type X ⟶ Y.

source

def category_theory.locally_discrete (C : Type u) :

Type u

A type synonym for promoting any type to a category, with the only morphisms being equalities.

Equations

category_theory.locally_discrete C = C

Instances for category_theory.locally_discrete

source

@[protected, instance]

def category_theory.locally_discrete.inhabited {C : Type u} [inhabited C] :

inhabited (category_theory.locally_discrete C)

Equations

category_theory.locally_discrete.inhabited = id

source

@[protected, instance]

def category_theory.locally_discrete.category_theory.category_struct {C : Type u} [category_theory.category_struct C] :

category_theory.category_struct (category_theory.locally_discrete C)

Equations

category_theory.locally_discrete.category_theory.category_struct = {to_quiver := {hom := λ (X Y : C), category_theory.discrete (X ⟶ Y)}, id := λ (X : C), {as := 𝟙 X}, comp := λ (X Y Z : category_theory.locally_discrete C) (f : X ⟶ Y) (g : Y ⟶ Z), {as := f.as ≫ g.as}}

source

@[protected, instance]

def category_theory.locally_discrete.hom_small_category {C : Type u} [category_theory.category_struct C] (X Y : category_theory.locally_discrete C) :

category_theory.small_category (X ⟶ Y)

Equations

X.hom_small_category Y = category_theory.discrete_category (X ⟶ Y)

source

theorem category_theory.locally_discrete.eq_of_hom {C : Type u} [category_theory.category_struct C] {X Y : category_theory.locally_discrete C} {f g : X ⟶ Y} (η : f ⟶ g) :

f = g

Extract the equation from a 2-morphism in a locally discrete 2-category.

source

@[protected, instance]

def category_theory.locally_discrete_bicategory (C : Type u) [category_theory.category C] :

category_theory.bicategory (category_theory.locally_discrete C)

The locally discrete bicategory on a category is a bicategory in which the objects and the 1-morphisms are the same as those in the underlying category, and the 2-morphisms are the equalities between 1-morphisms.

Equations

category_theory.locally_discrete_bicategory C = {to_category_struct := category_theory.locally_discrete.category_theory.category_struct category_theory.category.to_category_struct, hom_category := λ (X Z : category_theory.locally_discrete C), category_theory.discrete_category (X ⟶ Z), whisker_left := λ (X Y Z : category_theory.locally_discrete C) (f : X ⟶ Y) (g h : Y ⟶ Z) (η : g ⟶ h), category_theory.eq_to_hom _, whisker_right := λ (X Y Z : category_theory.locally_discrete C) (f g : X ⟶ Y) (η : f ⟶ g) (h : Y ⟶ Z), category_theory.eq_to_hom _, associator := λ (W X Y Z : category_theory.locally_discrete C) (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), category_theory.eq_to_iso _, left_unitor := λ (X Y : category_theory.locally_discrete C) (f : X ⟶ Y), category_theory.eq_to_iso _, right_unitor := λ (X Y : category_theory.locally_discrete C) (f : X ⟶ Y), category_theory.eq_to_iso _, whisker_left_id' := _, whisker_left_comp' := _, id_whisker_left' := _, comp_whisker_left' := _, id_whisker_right' := _, comp_whisker_right' := _, whisker_right_id' := _, whisker_right_comp' := _, whisker_assoc' := _, whisker_exchange' := _, pentagon' := _, triangle' := _}

source

@[protected, instance]

def category_theory.locally_discrete_bicategory.strict (C : Type u) [category_theory.category C] :

category_theory.bicategory.strict (category_theory.locally_discrete C)

A locally discrete bicategory is strict.

source

@[simp]

theorem category_theory.functor.to_oplax_functor_map_id {I : Type u₁} [category_theory.category I] {B : Type u₂} [category_theory.bicategory B] [category_theory.bicategory.strict B] (F : I ⥤ B) (i : category_theory.locally_discrete I) :

F.to_oplax_functor.map_id i = category_theory.eq_to_hom _

source

@[simp]

theorem category_theory.functor.to_oplax_functor_obj {I : Type u₁} [category_theory.category I] {B : Type u₂} [category_theory.bicategory B] [category_theory.bicategory.strict B] (F : I ⥤ B) (ᾰ : I) :

F.to_oplax_functor.obj ᾰ = F.obj ᾰ

source

@[simp]

theorem category_theory.functor.to_oplax_functor_map₂ {I : Type u₁} [category_theory.category I] {B : Type u₂} [category_theory.bicategory B] [category_theory.bicategory.strict B] (F : I ⥤ B) (i j : category_theory.locally_discrete I) (f g : i ⟶ j) (η : f ⟶ g) :

F.to_oplax_functor.map₂ η = category_theory.eq_to_hom _

source

def category_theory.functor.to_oplax_functor {I : Type u₁} [category_theory.category I] {B : Type u₂} [category_theory.bicategory B] [category_theory.bicategory.strict B] (F : I ⥤ B) :

category_theory.oplax_functor (category_theory.locally_discrete I) B

If B is a strict bicategory and I is a (1-)category, any functor (of 1-categories) I ⥤ B can be promoted to an oplax functor from locally_discrete I to B.

Equations

F.to_oplax_functor = {obj := F.obj, map := λ (X Y : category_theory.locally_discrete I) (f : X ⟶ Y), F.map f.as, map₂ := λ (i j : category_theory.locally_discrete I) (f g : i ⟶ j) (η : f ⟶ g), category_theory.eq_to_hom _, map_id := λ (i : category_theory.locally_discrete I), category_theory.eq_to_hom _, map_comp := λ (i j k : category_theory.locally_discrete I) (f : i ⟶ j) (g : j ⟶ k), category_theory.eq_to_hom _, map_comp_naturality_left' := _, map_comp_naturality_right' := _, map₂_id' := _, map₂_comp' := _, map₂_associator' := _, map₂_left_unitor' := _, map₂_right_unitor' := _}

source

@[simp]

theorem category_theory.functor.to_oplax_functor_map_comp {I : Type u₁} [category_theory.category I] {B : Type u₂} [category_theory.bicategory B] [category_theory.bicategory.strict B] (F : I ⥤ B) (i j k : category_theory.locally_discrete I) (f : i ⟶ j) (g : j ⟶ k) :

F.to_oplax_functor.map_comp f g = category_theory.eq_to_hom _

source

@[simp]

theorem category_theory.functor.to_oplax_functor_map {I : Type u₁} [category_theory.category I] {B : Type u₂} [category_theory.bicategory B] [category_theory.bicategory.strict B] (F : I ⥤ B) (X Y : category_theory.locally_discrete I) (f : X ⟶ Y) :

F.to_oplax_functor.map f = F.map f.as