Induced bicategories

In this file we develop API for constructing a full sub-bicategory of a bicategory C, given a map F : B → C. The objects of the induced bicategory are the objects of B, while the 1-morphisms and 2-morphisms are taken as all corresponding morphisms in C.

TODO

One might also want to develop "locally induced" bicategories, which should allow for a sub-class of 1-morphisms as well. However, this needs more thought. If one tries the naive approach of simply replacing the map F below with a "functor" (between CategoryStructs), one runs into the issue that map_comp and map_id might not be definitional equalities (which they should be in practice). Hence one needs to carefully carry these around, or specify F in a way that ensures they are def-eqs, perhaps constructing it from specified MorhpismPropertys.

def CategoryTheory.Bicategory.InducedBicategory {B : Type u_1} (C : Type u_2) (_F : B → C) : Type u_1

InducedBicategory B C, where F : B → C, is a typeclass synonym for B. This is given a bicategory structure where the 1-morphisms X ⟶ Y are the 1-morphisms in C from F X to F Y, and the 2-morphisms f ⟶ g are also the 2-morphisms in C from f to g.

Equations

• CategoryTheory.Bicategory.InducedBicategory C _F = B

instance CategoryTheory.Bicategory.InducedBicategory.hasCoeToSort {B : Type u_1} {C : Type u_2} {F : B → C} {α : Sort u_3} [CoeSort C α] : CoeSort (InducedBicategory C F) α

Equations

• CategoryTheory.Bicategory.InducedBicategory.hasCoeToSort = { coe := fun (c : CategoryTheory.Bicategory.InducedBicategory C F) => CoeSort.coe (F c) }

structure CategoryTheory.Bicategory.InducedBicategory.Hom {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} (X Y : InducedBicategory C F) : Type u_4

InducedBicategory.Hom X Y is a type-alias for morphisms between X Y : B viewed as objects of B with the induced bicategory structure. This is given a CategoryStruct instance below, where the identity and composition is induced from C.

• hom : F X ⟶ F Y

  The morphism in C underlying the morphism in InducedBicategory C F.

theorem CategoryTheory.Bicategory.InducedBicategory.Hom.ext_iff {B : Type u_1} {C : Type u_2} {inst✝ : Bicategory C} {F : B → C} {X Y : InducedBicategory C F} {x y : X.Hom Y} : x = y ↔ x.hom = y.hom

theorem CategoryTheory.Bicategory.InducedBicategory.Hom.ext {B : Type u_1} {C : Type u_2} {inst✝ : Bicategory C} {F : B → C} {X Y : InducedBicategory C F} {x y : X.Hom Y} (hom : x.hom = y.hom) : x = y

instance CategoryTheory.Bicategory.InducedBicategory.categoryStruct {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} : CategoryStruct.{u_4, u_1} (InducedBicategory C F)

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.InducedBicategory.categoryStruct_comp_hom {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} {X✝ Y✝ Z✝ : InducedBicategory C F} (u : X✝.Hom Y✝) (v : Y✝.Hom Z✝) : (CategoryStruct.comp u v).hom = CategoryStruct.comp u.hom v.hom

@[simp]

theorem CategoryTheory.Bicategory.InducedBicategory.categoryStruct_id_hom {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} (X : InducedBicategory C F) : (CategoryStruct.id X).hom = CategoryStruct.id (F X)

@[reducible, inline]

abbrev CategoryTheory.Bicategory.InducedBicategory.mkHom {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} {X Y : InducedBicategory C F} (f : F X ⟶ F Y) : X ⟶ Y

Synonym for Hom.mk which makes unification easier.

Equations

• CategoryTheory.Bicategory.InducedBicategory.mkHom f = { hom := f }

theorem CategoryTheory.Bicategory.InducedBicategory.hom_ext {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} {X Y : InducedBicategory C F} {f g : X ⟶ Y} (h : f.hom = g.hom) : f = g

theorem CategoryTheory.Bicategory.InducedBicategory.hom_ext_iff {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} {X Y : InducedBicategory C F} {f g : X ⟶ Y} : f = g ↔ f.hom = g.hom

structure CategoryTheory.Bicategory.InducedBicategory.Hom₂ {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} {X Y : InducedBicategory C F} (f g : X ⟶ Y) : Type u_3

InducedBicategory.Hom₂ f g is a type-alias for 2-morphisms between f g : X ⟶ Y, where f and g are 1-morphisms for the induced bicategory structure on B.

This is given a Category instance below, induced from the corresponding one in C.

• hom : f.hom ⟶ g.hom

  The 2-morphism in C underlying the 2-morphism in InducedBicategory C F.

theorem CategoryTheory.Bicategory.InducedBicategory.Hom₂.ext {B : Type u_1} {C : Type u_2} {inst✝ : Bicategory C} {F : B → C} {X Y : InducedBicategory C F} {f g : X ⟶ Y} {x y : Hom₂ f g} (hom : x.hom = y.hom) : x = y

theorem CategoryTheory.Bicategory.InducedBicategory.Hom₂.ext_iff {B : Type u_1} {C : Type u_2} {inst✝ : Bicategory C} {F : B → C} {X Y : InducedBicategory C F} {f g : X ⟶ Y} {x y : Hom₂ f g} : x = y ↔ x.hom = y.hom

instance CategoryTheory.Bicategory.InducedBicategory.Hom.category {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} (X Y : InducedBicategory C F) : Category.{u_3, u_4} (X ⟶ Y)

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.InducedBicategory.Hom.category_comp_hom {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} (X Y : InducedBicategory C F) {X✝ Y✝ Z✝ : X ⟶ Y} (u : Hom₂ X✝ Y✝) (v : Hom₂ Y✝ Z✝) : (CategoryStruct.comp u v).hom = CategoryStruct.comp u.hom v.hom

@[simp]

theorem CategoryTheory.Bicategory.InducedBicategory.Hom.category_id_hom {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} (X Y : InducedBicategory C F) (f : X ⟶ Y) : (CategoryStruct.id f).hom = CategoryStruct.id f.hom

theorem CategoryTheory.Bicategory.InducedBicategory.hom₂_ext {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} {X Y : InducedBicategory C F} {f g : X ⟶ Y} {η θ : f ⟶ g} (h : η.hom = θ.hom) : η = θ

theorem CategoryTheory.Bicategory.InducedBicategory.hom₂_ext_iff {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} {X Y : InducedBicategory C F} {f g : X ⟶ Y} {η θ : f ⟶ g} : η = θ ↔ η.hom = θ.hom

@[reducible, inline]

abbrev CategoryTheory.Bicategory.InducedBicategory.mkHom₂ {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} {a b : InducedBicategory C F} {f g : F a ⟶ F b} (η : f ⟶ g) : mkHom f ⟶ mkHom g

Synonym for the constructor of Hom₂ where the 1-morphisms f and g lie in C, and not given in the form f'.hom, g'.hom for some f' g' : InducedBicategory.Hom _ _.

Equations

• CategoryTheory.Bicategory.InducedBicategory.mkHom₂ η = { hom := η }

def CategoryTheory.Bicategory.InducedBicategory.isoMk {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} {X Y : InducedBicategory C F} {f g : X ⟶ Y} (φ : f.hom ≅ g.hom) : f ≅ g

Constructor for 2-isomorphisms in the induced bicategory.

Equations

• CategoryTheory.Bicategory.InducedBicategory.isoMk φ = { hom := { hom := φ.hom }, inv := { hom := φ.inv }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Bicategory.InducedBicategory.isoMk_inv_hom {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} {X Y : InducedBicategory C F} {f g : X ⟶ Y} (φ : f.hom ≅ g.hom) : (isoMk φ).inv.hom = φ.inv

@[simp]

theorem CategoryTheory.Bicategory.InducedBicategory.isoMk_hom_hom {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} {X Y : InducedBicategory C F} {f g : X ⟶ Y} (φ : f.hom ≅ g.hom) : (isoMk φ).hom.hom = φ.hom

instance CategoryTheory.Bicategory.InducedBicategory.bicategory {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} : Bicategory (InducedBicategory C F)

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.InducedBicategory.bicategory_whiskerRight_hom {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} {x✝ x✝¹ x✝² : InducedBicategory C F} {x✝³ x✝⁴ : x✝ ⟶ x✝¹} (η : x✝³ ⟶ x✝⁴) (h : x✝¹ ⟶ x✝²) : (whiskerRight η h).hom = whiskerRight η.hom h.hom

@[simp]

theorem CategoryTheory.Bicategory.InducedBicategory.bicategory_leftUnitor_hom_hom {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} {a✝ b✝ : InducedBicategory C F} (x : a✝ ⟶ b✝) : (leftUnitor x).hom.hom = (leftUnitor x.hom).hom

@[simp]

theorem CategoryTheory.Bicategory.InducedBicategory.bicategory_whiskerLeft_hom {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} {x✝ x✝¹ x✝² : InducedBicategory C F} (h : x✝ ⟶ x✝¹) {x✝³ x✝⁴ : x✝¹ ⟶ x✝²} (η : x✝³ ⟶ x✝⁴) : (whiskerLeft h η).hom = whiskerLeft h.hom η.hom

@[simp]

theorem CategoryTheory.Bicategory.InducedBicategory.bicategory_rightUnitor_inv_hom {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} {a✝ b✝ : InducedBicategory C F} (x : a✝ ⟶ b✝) : (rightUnitor x).inv.hom = (rightUnitor x.hom).inv

@[simp]

theorem CategoryTheory.Bicategory.InducedBicategory.bicategory_associator_inv_hom {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} {a✝ b✝ c✝ d✝ : InducedBicategory C F} (x : a✝ ⟶ b✝) (y : b✝ ⟶ c✝) (z : c✝ ⟶ d✝) : (associator x y z).inv.hom = (associator x.hom y.hom z.hom).inv

@[simp]

theorem CategoryTheory.Bicategory.InducedBicategory.bicategory_leftUnitor_inv_hom {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} {a✝ b✝ : InducedBicategory C F} (x : a✝ ⟶ b✝) : (leftUnitor x).inv.hom = (leftUnitor x.hom).inv

@[simp]

theorem CategoryTheory.Bicategory.InducedBicategory.bicategory_comp_hom {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} {X✝ Y✝ Z✝ : InducedBicategory C F} (u : X✝.Hom Y✝) (v : Y✝.Hom Z✝) : (CategoryStruct.comp u v).hom = CategoryStruct.comp u.hom v.hom

@[simp]

theorem CategoryTheory.Bicategory.InducedBicategory.bicategory_Hom {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} (X Y : InducedBicategory C F) : (X ⟶ Y) = X.Hom Y

@[simp]

theorem CategoryTheory.Bicategory.InducedBicategory.bicategory_homCategory_id_hom {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} (a b : InducedBicategory C F) (f : a ⟶ b) : (CategoryStruct.id f).hom = CategoryStruct.id f.hom

@[simp]

theorem CategoryTheory.Bicategory.InducedBicategory.bicategory_homCategory_comp_hom {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} (a b : InducedBicategory C F) {X✝ Y✝ Z✝ : a ⟶ b} (u : Hom₂ X✝ Y✝) (v : Hom₂ Y✝ Z✝) : (CategoryStruct.comp u v).hom = CategoryStruct.comp u.hom v.hom

@[simp]

theorem CategoryTheory.Bicategory.InducedBicategory.bicategory_associator_hom_hom {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} {a✝ b✝ c✝ d✝ : InducedBicategory C F} (x : a✝ ⟶ b✝) (y : b✝ ⟶ c✝) (z : c✝ ⟶ d✝) : (associator x y z).hom.hom = (associator x.hom y.hom z.hom).hom

@[simp]

theorem CategoryTheory.Bicategory.InducedBicategory.bicategory_rightUnitor_hom_hom {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} {a✝ b✝ : InducedBicategory C F} (x : a✝ ⟶ b✝) : (rightUnitor x).hom.hom = (rightUnitor x.hom).hom

@[simp]

theorem CategoryTheory.Bicategory.InducedBicategory.bicategory_id_hom {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} (X : InducedBicategory C F) : (CategoryStruct.id X).hom = CategoryStruct.id (F X)

def CategoryTheory.Bicategory.InducedBicategory.forget {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} : StrictPseudofunctor (InducedBicategory C F) C

The forgetful (strict) pseudofunctor from an induced bicategory to the original bicategory, forgetting the extra data.

Equations

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

@[simp]

theorem CategoryTheory.Bicategory.InducedBicategory.forget_mapId_inv {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} (x : InducedBicategory C F) : (forget.mapId x).inv = CategoryStruct.id (CategoryStruct.id (F x))

@[simp]

theorem CategoryTheory.Bicategory.InducedBicategory.forget_mapComp_inv {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} {a✝ b✝ c✝ : InducedBicategory C F} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : (forget.mapComp f g).inv = CategoryStruct.id (CategoryStruct.comp f.hom g.hom)

@[simp]

theorem CategoryTheory.Bicategory.InducedBicategory.forget_map {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} {X✝ Y✝ : InducedBicategory C F} (a✝ : X✝ ⟶ Y✝) : forget.map a✝ = a✝.hom

@[simp]

theorem CategoryTheory.Bicategory.InducedBicategory.forget_map₂ {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} {a✝ b✝ : InducedBicategory C F} {f✝ g✝ : a✝ ⟶ b✝} (a✝¹ : f✝ ⟶ g✝) : forget.map₂ a✝¹ = a✝¹.hom

@[simp]

theorem CategoryTheory.Bicategory.InducedBicategory.forget_mapComp_hom {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} {a✝ b✝ c✝ : InducedBicategory C F} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : (forget.mapComp f g).hom = CategoryStruct.id (CategoryStruct.comp f.hom g.hom)

@[simp]

theorem CategoryTheory.Bicategory.InducedBicategory.forget_mapId_hom {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} (x : InducedBicategory C F) : (forget.mapId x).hom = CategoryStruct.id (CategoryStruct.id (F x))

@[simp]

theorem CategoryTheory.Bicategory.InducedBicategory.forget_obj {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} (a✝ : InducedBicategory C F) : forget.obj a✝ = F a✝

@[simp]

theorem CategoryTheory.Bicategory.InducedBicategory.eqToHom_hom {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} {X Y : InducedBicategory C F} {f g : X ⟶ Y} (h : f = g) : (eqToHom h).hom = eqToHom ⋯

@[simp]

theorem CategoryTheory.Bicategory.InducedBicategory.mkHom_eqToHom {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} {X Y : InducedBicategory C F} {f g : F X ⟶ F Y} (h : f = g) : mkHom₂ (eqToHom h) = eqToHom ⋯

instance CategoryTheory.Bicategory.InducedBicategory.instStrict {B : Type u_1} {C : Type u_2} [Bicategory C] {F : B → C} [Strict C] : Strict (InducedBicategory C F)