(2,1)-categories

A bicategory B is said to be locally groupoidal (or a (2,1)-category) if for every pair of objects x, y, the Hom-category x ⟶ y is a groupoid (which is expressed using the CategoryTheory.IsGroupoid typeclass).

Given a bicategory B, we construct a bicategory Pith B which is obtained from B by discarding non-invertible 2-morphisms. This is realized in practice by applying Core to each hom-category of C. By construction, Pith B is a (2,1)-category, and for every (2,1)-category B', every pseudofunctor B' ⥤ B factors (essentially) uniquely through the inclusion from Pith B to B (see CategoryTheory.Bicategory.Pith.pseudofunctorToPith).

References

• Kerodon, section 1.2.2.

@[reducible, inline]

abbrev CategoryTheory.Bicategory.IsLocallyGroupoid (B : Type u₁) [Bicategory B] : Prop

A bicategory is locally groupoidal if the categories of 1-morphisms are groupoids.

structure CategoryTheory.Bicategory.Pith (B : Type u₁) : Type u₁

Given a bicategory B, Pith B is the bicategory obtained by discarding the non-invertible 2-cells from B. We implement this as a wrapper type for B, and use CategoryTheory.Core to discard the non-invertible morphisms.

• as : B

  The underlying object of the bicategory.

theorem CategoryTheory.Bicategory.Pith.mk_as (B : Type u₁) (b : Pith B) : { as := b.as } = b

instance CategoryTheory.Bicategory.Pith.instInhabited (B : Type u₁) [Inhabited B] : Inhabited (Pith B)

instance CategoryTheory.Bicategory.Pith.categoryStruct (B : Type u₁) [Bicategory B] : CategoryStruct.{v₁, u₁} (Pith B)

@[simp]

theorem CategoryTheory.Bicategory.Pith.id_of (B : Type u₁) [Bicategory B] (a : Pith B) : (CategoryStruct.id a).of = CategoryStruct.id a.as

@[simp]

theorem CategoryTheory.Bicategory.Pith.comp_of (B : Type u₁) [Bicategory B] {a b c : Pith B} (f : a ⟶ b) (g : b ⟶ c) : (CategoryStruct.comp f g).of = CategoryStruct.comp f.of g.of

instance CategoryTheory.Bicategory.Pith.homGroupoid (B : Type u₁) [Bicategory B] (a b : Pith B) : Groupoid (a ⟶ b)

theorem CategoryTheory.Bicategory.Pith.hom₂_ext (B : Type u₁) [Bicategory B] {a b : Pith B} {x y : a ⟶ b} {f g : x ⟶ y} (h : f.iso.hom = g.iso.hom) : f = g

theorem CategoryTheory.Bicategory.Pith.hom₂_ext_iff {B : Type u₁} [Bicategory B] {a b : Pith B} {x y : a ⟶ b} {f g : x ⟶ y} : f = g ↔ f.iso.hom = g.iso.hom

@[simp]

theorem CategoryTheory.Bicategory.Pith.comp₂_iso_hom (B : Type u₁) [Bicategory B] {a b : Pith B} {x y z : a ⟶ b} {f : x ⟶ y} {g : y ⟶ z} : (CategoryStruct.comp f g).iso.hom = CategoryStruct.comp f.iso.hom g.iso.hom

theorem CategoryTheory.Bicategory.Pith.comp₂_iso_hom_assoc (B : Type u₁) [Bicategory B] {a b : Pith B} {x y z : a ⟶ b} {f : x ⟶ y} {g : y ⟶ z} {Z : a.as ⟶ b.as} (h : z.of ⟶ Z) : CategoryStruct.comp (CategoryStruct.comp f g).iso.hom h = CategoryStruct.comp f.iso.hom (CategoryStruct.comp g.iso.hom h)

@[simp]

theorem CategoryTheory.Bicategory.Pith.comp₂_iso_inv (B : Type u₁) [Bicategory B] {a b : Pith B} {x y z : a ⟶ b} {f : x ⟶ y} {g : y ⟶ z} : (CategoryStruct.comp f g).iso.inv = CategoryStruct.comp g.iso.inv f.iso.inv

theorem CategoryTheory.Bicategory.Pith.comp₂_iso_inv_assoc (B : Type u₁) [Bicategory B] {a b : Pith B} {x y z : a ⟶ b} {f : x ⟶ y} {g : y ⟶ z} {Z : a.as ⟶ b.as} (h : x.of ⟶ Z) : CategoryStruct.comp (CategoryStruct.comp f g).iso.inv h = CategoryStruct.comp g.iso.inv (CategoryStruct.comp f.iso.inv h)

@[simp]

theorem CategoryTheory.Bicategory.Pith.id₂_iso_hom (B : Type u₁) [Bicategory B] {a b : Pith B} {x : a ⟶ b} : (CategoryStruct.id x).iso.hom = CategoryStruct.id x.of

@[simp]

theorem CategoryTheory.Bicategory.Pith.id₂_iso_inv (B : Type u₁) [Bicategory B] {a b : Pith B} {x : a ⟶ b} : (CategoryStruct.id x).iso.inv = CategoryStruct.id x.of

instance CategoryTheory.Bicategory.Pith.inst (B : Type u₁) [Bicategory B] : Bicategory (Pith B)

@[simp]

theorem CategoryTheory.Bicategory.Pith.rightUnitor_inv_iso_inv (B : Type u₁) [Bicategory B] {a✝ b✝ : Pith B} (x : a✝ ⟶ b✝) : (rightUnitor x).inv.iso.inv = (rightUnitor x.of).hom

@[simp]

theorem CategoryTheory.Bicategory.Pith.whiskerLeft_iso_hom (B : Type u₁) [Bicategory B] {a✝ b✝ c✝ : Pith B} (x : a✝ ⟶ b✝) (x✝ x✝¹ : b✝ ⟶ c✝) (f : x✝ ⟶ x✝¹) : (whiskerLeft x f).iso.hom = whiskerLeft x.of f.iso.hom

@[simp]

theorem CategoryTheory.Bicategory.Pith.whiskerLeft_iso_inv (B : Type u₁) [Bicategory B] {a✝ b✝ c✝ : Pith B} (x : a✝ ⟶ b✝) (x✝ x✝¹ : b✝ ⟶ c✝) (f : x✝ ⟶ x✝¹) : (whiskerLeft x f).iso.inv = whiskerLeft x.of f.iso.inv

@[simp]

theorem CategoryTheory.Bicategory.Pith.associator_inv_iso_hom (B : Type u₁) [Bicategory B] {a✝ b✝ c✝ d✝ : Pith B} (x : a✝ ⟶ b✝) (y : b✝ ⟶ c✝) (z : c✝ ⟶ d✝) : (associator x y z).inv.iso.hom = (associator x.of y.of z.of).inv

@[simp]

theorem CategoryTheory.Bicategory.Pith.associator_hom_iso (B : Type u₁) [Bicategory B] {a✝ b✝ c✝ d✝ : Pith B} (x : a✝ ⟶ b✝) (y : b✝ ⟶ c✝) (z : c✝ ⟶ d✝) : (associator x y z).hom.iso = associator x.of y.of z.of

@[simp]

theorem CategoryTheory.Bicategory.Pith.rightUnitor_hom_iso (B : Type u₁) [Bicategory B] {a✝ b✝ : Pith B} (x : a✝ ⟶ b✝) : (rightUnitor x).hom.iso = rightUnitor x.of

@[simp]

theorem CategoryTheory.Bicategory.Pith.associator_inv_iso_inv (B : Type u₁) [Bicategory B] {a✝ b✝ c✝ d✝ : Pith B} (x : a✝ ⟶ b✝) (y : b✝ ⟶ c✝) (z : c✝ ⟶ d✝) : (associator x y z).inv.iso.inv = (associator x.of y.of z.of).hom

@[simp]

theorem CategoryTheory.Bicategory.Pith.leftUnitor_inv_iso_hom (B : Type u₁) [Bicategory B] {a✝ b✝ : Pith B} (x : a✝ ⟶ b✝) : (leftUnitor x).inv.iso.hom = (leftUnitor x.of).inv

@[simp]

theorem CategoryTheory.Bicategory.Pith.leftUnitor_hom_iso (B : Type u₁) [Bicategory B] {a✝ b✝ : Pith B} (x : a✝ ⟶ b✝) : (leftUnitor x).hom.iso = leftUnitor x.of

@[simp]

theorem CategoryTheory.Bicategory.Pith.whiskerRight_iso_inv (B : Type u₁) [Bicategory B] {a✝ b✝ c✝ : Pith B} {f✝ g✝ : a✝ ⟶ b✝} (f : f✝ ⟶ g✝) (y : b✝ ⟶ c✝) : (whiskerRight f y).iso.inv = whiskerRight f.iso.inv y.of

@[simp]

theorem CategoryTheory.Bicategory.Pith.whiskerRight_iso_hom (B : Type u₁) [Bicategory B] {a✝ b✝ c✝ : Pith B} {f✝ g✝ : a✝ ⟶ b✝} (f : f✝ ⟶ g✝) (y : b✝ ⟶ c✝) : (whiskerRight f y).iso.hom = whiskerRight f.iso.hom y.of

@[simp]

theorem CategoryTheory.Bicategory.Pith.rightUnitor_inv_iso_hom (B : Type u₁) [Bicategory B] {a✝ b✝ : Pith B} (x : a✝ ⟶ b✝) : (rightUnitor x).inv.iso.hom = (rightUnitor x.of).inv

def CategoryTheory.Bicategory.Pith.inclusion (B : Type u₁) [Bicategory B] : Pseudofunctor (Pith B) B

The canonical inclusion from the pith of B to B, as a Pseudofunctor.

@[simp]

theorem CategoryTheory.Bicategory.Pith.inclusion_mapComp (B : Type u₁) [Bicategory B] {a✝ b✝ c✝ : Pith B} (x✝ : a✝ ⟶ b✝) (x✝¹ : b✝ ⟶ c✝) : (inclusion B).mapComp x✝ x✝¹ = Iso.refl (CategoryStruct.comp x✝ x✝¹).of

@[simp]

theorem CategoryTheory.Bicategory.Pith.inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map (B : Type u₁) [Bicategory B] {X✝ Y✝ : Pith B} (f : X✝ ⟶ Y✝) : (inclusion B).map f = f.of

@[simp]

theorem CategoryTheory.Bicategory.Pith.inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_map₂ (B : Type u₁) [Bicategory B] {a✝ b✝ : Pith B} {f✝ g✝ : a✝ ⟶ b✝} (η : f✝ ⟶ g✝) : (inclusion B).map₂ η = η.iso.hom

@[simp]

theorem CategoryTheory.Bicategory.Pith.inclusion_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj (B : Type u₁) [Bicategory B] (x : Pith B) : (inclusion B).obj x = x.as

@[simp]

theorem CategoryTheory.Bicategory.Pith.inclusion_mapId (B : Type u₁) [Bicategory B] (x✝ : Pith B) : (inclusion B).mapId x✝ = Iso.refl (CategoryStruct.id x✝).of

noncomputable def CategoryTheory.Bicategory.Pith.pseudofunctorToPith {B : Type u₁} [Bicategory B] {B' : Type u₂} [Bicategory B'] [IsLocallyGroupoid B'] (F : Pseudofunctor B' B) : Pseudofunctor B' (Pith B)

Any pseudofunctor from a (2,1)-category to a bicategory factors through the pith of the target bicategory.

@[simp]

theorem CategoryTheory.Bicategory.Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_as {B : Type u₁} [Bicategory B] {B' : Type u₂} [Bicategory B'] [IsLocallyGroupoid B'] (F : Pseudofunctor B' B) (x : B') : ((pseudofunctorToPith F).obj x).as = F.obj x

@[simp]

theorem CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapId_inv_iso_inv {B : Type u₁} [Bicategory B] {B' : Type u₂} [Bicategory B'] [IsLocallyGroupoid B'] (F : Pseudofunctor B' B) (x : B') : ((pseudofunctorToPith F).mapId x).inv.iso.inv = (F.mapId x).hom

@[simp]

theorem CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapComp_hom_iso {B : Type u₁} [Bicategory B] {B' : Type u₂} [Bicategory B'] [IsLocallyGroupoid B'] (F : Pseudofunctor B' B) {a✝ b✝ c✝ : B'} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : ((pseudofunctorToPith F).mapComp f g).hom.iso = F.mapComp f g

@[simp]

theorem CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapId_inv_iso_hom {B : Type u₁} [Bicategory B] {B' : Type u₂} [Bicategory B'] [IsLocallyGroupoid B'] (F : Pseudofunctor B' B) (x : B') : ((pseudofunctorToPith F).mapId x).inv.iso.hom = (F.mapId x).inv

@[simp]

theorem CategoryTheory.Bicategory.Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_iso_inv {B : Type u₁} [Bicategory B] {B' : Type u₂} [Bicategory B'] [IsLocallyGroupoid B'] (F : Pseudofunctor B' B) {a✝ b✝ : B'} {f✝ g✝ : a✝ ⟶ b✝} (f : f✝ ⟶ g✝) : ((pseudofunctorToPith F).map₂ f).iso.inv = inv (F.map₂ f)

@[simp]

theorem CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapId_hom_iso {B : Type u₁} [Bicategory B] {B' : Type u₂} [Bicategory B'] [IsLocallyGroupoid B'] (F : Pseudofunctor B' B) (x : B') : ((pseudofunctorToPith F).mapId x).hom.iso = F.mapId x

@[simp]

theorem CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapComp_inv_iso_hom {B : Type u₁} [Bicategory B] {B' : Type u₂} [Bicategory B'] [IsLocallyGroupoid B'] (F : Pseudofunctor B' B) {a✝ b✝ c✝ : B'} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : ((pseudofunctorToPith F).mapComp f g).inv.iso.hom = (F.mapComp f g).inv

@[simp]

theorem CategoryTheory.Bicategory.Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_map₂_iso_hom {B : Type u₁} [Bicategory B] {B' : Type u₂} [Bicategory B'] [IsLocallyGroupoid B'] (F : Pseudofunctor B' B) {a✝ b✝ : B'} {f✝ g✝ : a✝ ⟶ b✝} (f : f✝ ⟶ g✝) : ((pseudofunctorToPith F).map₂ f).iso.hom = F.map₂ f

@[simp]

theorem CategoryTheory.Bicategory.Pith.pseudofunctorToPith_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_map_of {B : Type u₁} [Bicategory B] {B' : Type u₂} [Bicategory B'] [IsLocallyGroupoid B'] (F : Pseudofunctor B' B) {X✝ Y✝ : B'} (f : X✝ ⟶ Y✝) : ((pseudofunctorToPith F).map f).of = F.map f

@[simp]

theorem CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapComp_inv_iso_inv {B : Type u₁} [Bicategory B] {B' : Type u₂} [Bicategory B'] [IsLocallyGroupoid B'] (F : Pseudofunctor B' B) {a✝ b✝ c✝ : B'} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : ((pseudofunctorToPith F).mapComp f g).inv.iso.inv = (F.mapComp f g).hom

noncomputable def CategoryTheory.Bicategory.Pith.pseudofunctorToPithCompInclusionStrongIsoHom {B : Type u₁} [Bicategory B] {B' : Type u₂} [Bicategory B'] [IsLocallyGroupoid B'] (F : Pseudofunctor B' B) : ((pseudofunctorToPith F).comp (inclusion B)).StrongTrans F

The hom direction of the (strong) natural isomorphism of pseudofunctors between (pseudofunctorToPith F).comp (inclusion B) and F.

noncomputable def CategoryTheory.Bicategory.Pith.pseudofunctorToPithCompInclusionStrongIsoInv {B : Type u₁} [Bicategory B] {B' : Type u₂} [Bicategory B'] [IsLocallyGroupoid B'] (F : Pseudofunctor B' B) : F.StrongTrans ((pseudofunctorToPith F).comp (inclusion B))

The inv direction of the (strong) natural isomorphism of pseudofunctors between (pseudofunctorToPith F).comp (inclusion B) and F.

noncomputable def CategoryTheory.Bicategory.Pseudofunctor.ofLaxFunctorToLocallyGroupoid {B : Type u₁} [Bicategory B] {B' : Type u₂} [Bicategory B'] [IsLocallyGroupoid B] (F : LaxFunctor B' B) : F.PseudoCore

If B is a (2,1)-category, then every lax functor F from a bicategory to B defines a CategoryTheory.LaxFunctor.PseudoCore structure on F that can be used to promote F to a pseudofunctor using CategoryTheory.Pseudofunctor.mkOfLax.

@[simp]

theorem CategoryTheory.Bicategory.Pseudofunctor.ofLaxFunctorToLocallyGroupoid_mapIdIso_inv {B : Type u₁} [Bicategory B] {B' : Type u₂} [Bicategory B'] [IsLocallyGroupoid B] (F : LaxFunctor B' B) (x : B') : ((ofLaxFunctorToLocallyGroupoid F).mapIdIso x).inv = F.mapId x

@[simp]

theorem CategoryTheory.Bicategory.Pseudofunctor.ofLaxFunctorToLocallyGroupoid_mapCompIso_hom {B : Type u₁} [Bicategory B] {B' : Type u₂} [Bicategory B'] [IsLocallyGroupoid B] (F : LaxFunctor B' B) {a✝ b✝ c✝ : B'} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : ((ofLaxFunctorToLocallyGroupoid F).mapCompIso f g).hom = inv (F.mapComp f g)

@[simp]

theorem CategoryTheory.Bicategory.Pseudofunctor.ofLaxFunctorToLocallyGroupoid_mapIdIso_hom {B : Type u₁} [Bicategory B] {B' : Type u₂} [Bicategory B'] [IsLocallyGroupoid B] (F : LaxFunctor B' B) (x : B') : ((ofLaxFunctorToLocallyGroupoid F).mapIdIso x).hom = inv (F.mapId x)

@[simp]

theorem CategoryTheory.Bicategory.Pseudofunctor.ofLaxFunctorToLocallyGroupoid_mapCompIso_inv {B : Type u₁} [Bicategory B] {B' : Type u₂} [Bicategory B'] [IsLocallyGroupoid B] (F : LaxFunctor B' B) {a✝ b✝ c✝ : B'} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : ((ofLaxFunctorToLocallyGroupoid F).mapCompIso f g).inv = F.mapComp f g

noncomputable def CategoryTheory.Bicategory.Pseudofunctor.ofOplaxFunctorToLocallyGroupoid {B : Type u₁} [Bicategory B] {B' : Type u₂} [Bicategory B'] [IsLocallyGroupoid B] (F : OplaxFunctor B' B) : F.PseudoCore

If B is a (2,1)-category, then every oplax functor F from a bicategory to B defines a CategoryTheory.OplaxFunctor.PseudoCore structure on F that can be used to promote F to a pseudofunctor using CategoryTheory.Pseudofunctor.mkOfOplax.

@[simp]

theorem CategoryTheory.Bicategory.Pseudofunctor.ofOplaxFunctorToLocallyGroupoid_mapIdIso_inv {B : Type u₁} [Bicategory B] {B' : Type u₂} [Bicategory B'] [IsLocallyGroupoid B] (F : OplaxFunctor B' B) (x : B') : ((ofOplaxFunctorToLocallyGroupoid F).mapIdIso x).inv = inv (F.mapId x)

@[simp]

theorem CategoryTheory.Bicategory.Pseudofunctor.ofOplaxFunctorToLocallyGroupoid_mapIdIso_hom {B : Type u₁} [Bicategory B] {B' : Type u₂} [Bicategory B'] [IsLocallyGroupoid B] (F : OplaxFunctor B' B) (x : B') : ((ofOplaxFunctorToLocallyGroupoid F).mapIdIso x).hom = F.mapId x

@[simp]

theorem CategoryTheory.Bicategory.Pseudofunctor.ofOplaxFunctorToLocallyGroupoid_mapCompIso_hom {B : Type u₁} [Bicategory B] {B' : Type u₂} [Bicategory B'] [IsLocallyGroupoid B] (F : OplaxFunctor B' B) {a✝ b✝ c✝ : B'} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : ((ofOplaxFunctorToLocallyGroupoid F).mapCompIso f g).hom = F.mapComp f g

@[simp]

theorem CategoryTheory.Bicategory.Pseudofunctor.ofOplaxFunctorToLocallyGroupoid_mapCompIso_inv {B : Type u₁} [Bicategory B] {B' : Type u₂} [Bicategory B'] [IsLocallyGroupoid B] (F : OplaxFunctor B' B) {a✝ b✝ c✝ : B'} (f : a✝ ⟶ b✝) (g : b✝ ⟶ c✝) : ((ofOplaxFunctorToLocallyGroupoid F).mapCompIso f g).inv = inv (F.mapComp f g)