Skip to content

Commit b6ea121

Browse files
joelriouRida-Hamadani
joelriou
authored and
Rida-Hamadani
committed
feat(CategoryTheory): pseudofunctors from strict bicategories (leanprover-community#24382)
This PR provides an API for pseudofunctors `F` from a strict bicategory `B`. In particular, this shall apply to pseudofunctors from locally discrete bicategories. We first introduce more flexible variants of `mapId` and `mapComp`: for example, if `f` and `g` are composable morphisms and `fg` is such that `h : fg = f ≫ f`, we provide an isomorphism `F.mapComp' f g fg h : F.map fg ≅ F.map f ≫ F.map g`. We study the compatibilities of these isomorphisms with respect to composition with identities and associativity. Secondly, given a commutative square `t ≫ r = l ≫ b` in `B`, we construct an isomorphism `F.map t ≫ F.map r ≅ F.map l ≫ F.map b`. Co-authored-by: Christian Merten <christian@merten.dev> Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
1 parent 7fac55f commit b6ea121

File tree

3 files changed

+168
-0
lines changed

3 files changed

+168
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1928,6 +1928,7 @@ import Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
19281928
import Mathlib.CategoryTheory.Bicategory.Functor.Oplax
19291929
import Mathlib.CategoryTheory.Bicategory.Functor.Prelax
19301930
import Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
1931+
import Mathlib.CategoryTheory.Bicategory.Functor.Strict
19311932
import Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
19321933
import Mathlib.CategoryTheory.Bicategory.Grothendieck
19331934
import Mathlib.CategoryTheory.Bicategory.Kan.Adjunction

‎Mathlib/CategoryTheory/Bicategory/Functor/Pseudofunctor.lean‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -240,6 +240,27 @@ lemma whiskerLeft_mapId_inv (f : a ⟶ b) : F.map f ◁ (F.mapId b).inv =
240240
(ρ_ (F.map f)).hom ≫ F.map₂ (ρ_ f).inv ≫ (F.mapComp f (𝟙 b)).hom := by
241241
simpa using congrArg (·.inv) (F.whiskerLeftIso_mapId f)
242242

243+
/-- More flexible variant of `mapId`. (See the file `Bicategory.Functor.Strict`
244+
for applications to strict bicategories.) -/
245+
def mapId' {b : B} (f : b ⟶ b) (hf : f = 𝟙 b := by aesop_cat) :
246+
F.map f ≅ 𝟙 (F.obj b) :=
247+
F.map₂Iso (eqToIso (by rw [hf])) ≪≫ F.mapId _
248+
249+
lemma mapId'_eq_mapId (b : B) :
250+
F.mapId' (𝟙 b) rfl = F.mapId b := by
251+
simp [mapId']
252+
253+
/-- More flexible variant of `mapComp`. (See `Bicategory.Functor.Strict`
254+
for applications to strict bicategories.) -/
255+
def mapComp' {b₀ b₁ b₂ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (fg : b₀ ⟶ b₂)
256+
(h : f ≫ g = fg := by aesop_cat) :
257+
F.map fg ≅ F.map f ≫ F.map g :=
258+
F.map₂Iso (eqToIso (by rw [h])) ≪≫ F.mapComp f g
259+
260+
lemma mapComp'_eq_mapComp {b₀ b₁ b₂ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) :
261+
F.mapComp' f g _ rfl = F.mapComp f g := by
262+
simp [mapComp']
263+
243264
end
244265

245266
/-- Construct a pseudofunctor from an oplax functor whose `mapId` and `mapComp` are isomorphisms. -/

‎Mathlib/CategoryTheory/Bicategory/Functor/Strict.lean‎

Lines changed: 146 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,146 @@
1+
/-
2+
Copyright (c) 2025 Joël Riou. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Joël Riou, Christian Merten
5+
-/
6+
import Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
7+
import Mathlib.CategoryTheory.CommSq
8+
9+
/-!
10+
# Pseudofunctors from strict bicategory
11+
12+
This file provides an API for pseudofunctors `F` from a strict bicategory `B`. In
13+
particular, this shall apply to pseudofunctors from locally discrete bicategories.
14+
15+
Firstly, we study the compatibilities of the flexible variants `mapId'` and `mapComp'`
16+
of `mapId` and `mapComp` with respect to the composition with identities and the
17+
associativity.
18+
19+
Secondly, given a commutative square `t ≫ r = l ≫ b` in `B`, we construct an
20+
isomorphism `F.map t ≫ F.map r ≅ F.map l ≫ F.map b`
21+
(see `Pseudofunctor.isoMapOfCommSq`).
22+
23+
-/
24+
25+
namespace CategoryTheory
26+
27+
open Bicategory
28+
29+
namespace Pseudofunctor
30+
31+
variable {B C : Type*} [Bicategory B] [Strict B] [Bicategory C] (F : Pseudofunctor B C)
32+
33+
lemma mapComp'_comp_id {b₀ b₁ : B} (f : b₀ ⟶ b₁) :
34+
F.mapComp' f (𝟙 b₁) f = (ρ_ _).symm ≪≫ whiskerLeftIso _ (F.mapId b₁).symm := by
35+
ext
36+
rw [mapComp']
37+
dsimp
38+
rw [F.mapComp_id_right_hom f, Strict.rightUnitor_eqToIso, eqToIso.hom,
39+
← F.map₂_comp_assoc, eqToHom_trans, eqToHom_refl, PrelaxFunctor.map₂_id,
40+
Category.id_comp]
41+
42+
lemma mapComp'_id_comp {b₀ b₁ : B} (f : b₀ ⟶ b₁) :
43+
F.mapComp' (𝟙 b₀) f f = (λ_ _).symm ≪≫ whiskerRightIso (F.mapId b₀).symm _ := by
44+
ext
45+
rw [mapComp']
46+
dsimp
47+
rw [F.mapComp_id_left_hom f, Strict.leftUnitor_eqToIso, eqToIso.hom,
48+
← F.map₂_comp_assoc, eqToHom_trans, eqToHom_refl, PrelaxFunctor.map₂_id,
49+
Category.id_comp]
50+
51+
section associativity
52+
53+
variable {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
54+
(f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
55+
(h₀₂ : f₀₁ ≫ f₁₂ = f₀₂) (h₁₃ : f₁₂ ≫ f₂₃ = f₁₃)
56+
57+
@[reassoc]
58+
lemma mapComp'_hom_comp_whiskerLeft_mapComp'_hom (hf : f₀₁ ≫ f₁₃ = f) :
59+
(F.mapComp' f₀₁ f₁₃ f).hom ≫ F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom =
60+
(F.mapComp' f₀₂ f₂₃ f).hom ≫
61+
(F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ ≫ (α_ _ _ _).hom := by
62+
subst h₀₂ h₁₃ hf
63+
simp [mapComp_assoc_right_hom, Strict.associator_eqToIso, mapComp']
64+
65+
@[reassoc]
66+
lemma mapComp'_inv_comp_mapComp'_hom (hf : f₀₁ ≫ f₁₃ = f) :
67+
(F.mapComp' f₀₁ f₁₃ f).inv ≫ (F.mapComp' f₀₂ f₂₃ f).hom =
68+
F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom ≫
69+
(α_ _ _ _).inv ≫ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃ := by
70+
rw [← cancel_epi (F.mapComp' f₀₁ f₁₃ f hf).hom, Iso.hom_inv_id_assoc,
71+
F.mapComp'_hom_comp_whiskerLeft_mapComp'_hom_assoc _ _ _ _ _ _ h₀₂ h₁₃ hf]
72+
simp
73+
74+
@[reassoc]
75+
lemma whiskerLeft_mapComp'_inv_comp_mapComp'_inv (hf : f₀₁ ≫ f₁₃ = f) :
76+
F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv ≫ (F.mapComp' f₀₁ f₁₃ f hf).inv =
77+
(α_ _ _ _).inv ≫ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃ ≫
78+
(F.mapComp' f₀₂ f₂₃ f).inv := by
79+
simp [← cancel_mono (F.mapComp' f₀₂ f₂₃ f).hom,
80+
F.mapComp'_inv_comp_mapComp'_hom _ _ _ _ _ _ h₀₂ h₁₃ hf]
81+
82+
@[reassoc]
83+
lemma mapComp'_hom_comp_mapComp'_hom_whiskerRight (hf : f₀₂ ≫ f₂₃ = f) :
84+
(F.mapComp' f₀₂ f₂₃ f).hom ≫ (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom ▷ F.map f₂₃ =
85+
(F.mapComp' f₀₁ f₁₃ f).hom ≫ F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom ≫
86+
(α_ _ _ _).inv := by
87+
rw [F.mapComp'_hom_comp_whiskerLeft_mapComp'_hom_assoc _ _ _ _ _ f h₀₂ h₁₃ (by aesop_cat)]
88+
simp
89+
90+
@[reassoc]
91+
lemma mapComp'_inv_whiskerRight_comp_mapComp'_inv (hf : f₀₂ ≫ f₂₃ = f) :
92+
(F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv ▷ F.map f₂₃ ≫ (F.mapComp' f₀₂ f₂₃ f).inv =
93+
(α_ _ _ _).hom ≫ F.map f₀₁ ◁ (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv ≫
94+
(F.mapComp' f₀₁ f₁₃ f).inv := by
95+
rw [whiskerLeft_mapComp'_inv_comp_mapComp'_inv _ _ _ _ _ _ f h₀₂ h₁₃,
96+
Iso.hom_inv_id_assoc]
97+
98+
end associativity
99+
100+
section CommSq
101+
102+
variable {X₁ X₂ Y₁ Y₂ Z₁ Z₂ : B}
103+
104+
section
105+
106+
variable {t : X₁ ⟶ Y₁} {l : X₁ ⟶ X₂} {r : Y₁ ⟶ Y₂} {b : X₂ ⟶ Y₂} (sq : CommSq t l r b)
107+
108+
/-- Given a commutative square `CommSq t l r b` in a strict bicategory `B` and
109+
a pseudofunctor from `B`, this is the natural isomorphism
110+
`F.map t ≫ F.map r ≅ F.map l ≫ F.map b`. -/
111+
def isoMapOfCommSq : F.map t ≫ F.map r ≅ F.map l ≫ F.map b :=
112+
(F.mapComp t r).symm ≪≫ F.mapComp' _ _ _ (by rw [sq.w])
113+
114+
lemma isoMapOfCommSq_eq (φ : X₁ ⟶ Y₂) (hφ : t ≫ r = φ) :
115+
F.isoMapOfCommSq sq = (F.mapComp' t r φ (by rw [hφ])).symm ≪≫
116+
F.mapComp' l b φ (by rw [← hφ, sq.w]) := by
117+
subst hφ
118+
simp [isoMapOfCommSq, mapComp'_eq_mapComp]
119+
120+
end
121+
122+
/-- Equational lemma for `Pseudofunctor.isoMapOfCommSq` when
123+
both vertical maps of the square are the same and horizontal maps are identities. -/
124+
lemma isoMapOfCommSq_horiz_id (f : X₁ ⟶ X₂) :
125+
F.isoMapOfCommSq (t := 𝟙 _) (l := f) (r := f) (b := 𝟙 _) ⟨by simp⟩ =
126+
whiskerRightIso (F.mapId X₁) (F.map f) ≪≫ λ_ _ ≪≫ (ρ_ _).symm ≪≫
127+
(whiskerLeftIso (F.map f) (F.mapId X₂)).symm := by
128+
ext
129+
rw [isoMapOfCommSq_eq _ _ f (by simp), mapComp'_comp_id, mapComp'_id_comp]
130+
simp
131+
132+
/-- Equational lemma for `Pseudofunctor.isoMapOfCommSq` when
133+
both horizontal maps of the square are the same and vertical maps are identities. -/
134+
lemma isoMapOfCommSq_vert_id (f : X₁ ⟶ X₂) :
135+
F.isoMapOfCommSq (t := f) (l := 𝟙 _) (r := 𝟙 _) (b := f) ⟨by simp⟩ =
136+
whiskerLeftIso (F.map f) (F.mapId X₂) ≪≫ ρ_ _ ≪≫ (λ_ _).symm ≪≫
137+
(whiskerRightIso (F.mapId X₁) (F.map f)).symm := by
138+
ext
139+
rw [isoMapOfCommSq_eq _ _ f (by simp), mapComp'_comp_id, mapComp'_id_comp]
140+
simp
141+
142+
end CommSq
143+
144+
end Pseudofunctor
145+
146+
end CategoryTheory

0 commit comments

Comments
 (0)