Skip to content

Commit

Permalink
refactor(category_theory/bicategory): set simp-normal form for 2-morp…
Browse files Browse the repository at this point in the history 
…hisms (#13185)

## Problem

The definition of bicategories contains the following axioms:
```lean
associator_naturality_left : ∀ {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d),
  (η ▷ g) ▷ h ≫ (α_ f' g h).hom = (α_ f g h).hom ≫ η ▷ (g ≫ h)

associator_naturality_middle : ∀ (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d),
  (f ◁ η) ▷ h ≫ (α_ f g' h).hom = (α_ f g h).hom ≫ f ◁ (η ▷ h)

associator_naturality_right : ∀ (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h'),
  (f ≫ g) ◁ η ≫ (α_ f g h').hom = (α_ f g h).hom ≫ f ◁ (g ◁ η) 

left_unitor_naturality : ∀ {f g : a ⟶ b} (η : f ⟶ g),
  𝟙 a ◁ η ≫ (λ_ g).hom = (λ_ f).hom ≫ η

right_unitor_naturality : ∀ {f g : a ⟶ b} (η : f ⟶ g) :
  η ▷ 𝟙 b ≫ (ρ_ g).hom = (ρ_ f).hom ≫ η
```

By using these axioms, we can see that, for example, 2-morphisms `(f₁ ≫ f₂) ◁ (f₃ ◁ (η ▷ (f₄ ≫ f₅)))` and `f₁ ◁ ((𝟙_ ≫ f₂ ≫ f₃) ◁ ((η ▷ f₄) ▷ f₅))` are equal up to some associators and unitors. The problem is that the proof of this fact requires tedious rewriting. We should insert appropriate associators and unitors, and then rewrite using the above axioms manually.

This tedious rewriting is also a problem when we use the (forthcoming) `coherence` tactic (bicategorical version of #13125), which only works if the non-structural 2-morphisms in the LHS and the RHS are the same.

## Main change

The main proposal of this PR is to introduce a normal form of such 2-morphisms, and put simp attributes to suitable lemmas in order to rewrite any 2-morphism into the normal form. For example, the normal form of the previouse example is `f₁ ◁ (f₂ ◁ (f₃ ◁ ((η ▷ f₄) ▷ f₅)))`. The precise definition of the normal form can be found in the docs in `basic.lean` file. The new simp lemmas introduced in this PR are the following:

```lean
whisker_right_comp : ∀ {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d),
  η ▷ (g ≫ h) = (α_ f g h).inv ≫ η ▷ g ▷ h ≫ (α_ f' g h).hom 

whisker_assoc : ∀ (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d),
  (f ◁ η) ▷ h = (α_ f g h).hom ≫ f ◁ (η ▷ h) ≫ (α_ f g' h).inv

comp_whisker_left : ∀ (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h'),
  (f ≫ g) ◁ η = (α_ f g h).hom ≫ f ◁ g ◁ η ≫ (α_ f g h').inv

id_whisker_left : ∀ {f g : a ⟶ b} (η : f ⟶ g),
  𝟙 a ◁ η = (λ_ f).hom ≫ η ≫ (λ_ g).inv

whisker_right_id : ∀ {f g : a ⟶ b} (η : f ⟶ g),
  η ▷ 𝟙 b = (ρ_ f).hom ≫ η ≫ (ρ_ g).inv
```

Logically, these are equivalent to the five axioms presented above. The point is that these equalities have the definite simplification direction.

## Improvement 

Some proofs that had been based on tedious rewriting are now automated. For example, the conditions in `oplax_nat_trans.id`, `oplax_nat_trans.comp`, and several functions in `functor_bicategory.lean` are now proved by `tidy`.

## Specific changes

- The new simp lemmas `whisker_right_comp` etc. actually have been included in the definition of bicategories instead of `associate_naturality_left` etc. so that the latter lemmas are proved in later of the file just by `simp`.
- The precedence of the whiskering notations "infixr ` ◁ `:70" and "infixr ` ◁ `:70" have been changed into "infixr ` ◁ `:81" and "infixr ` ◁ `:81", which is now higher than that of the composition `≫`. This setting is consistent with the normal form introduced in this PR in the sence that an expression is in normal form only if it has the minimal number of parentheses in this setting. For example, the normal form `f₁ ◁ (f₂ ◁ (f₃ ◁ ((η ▷ f₄) ▷ f₅)))` can be written as `f₁ ◁ f₂ ◁ f₃ ◁ η ▷ f₄ ▷ f₅`.
- The unneeded parentheses caused by the precedence change have been removed.
- The lemmas `whisker_right_id` and `whisker_right_comp` have been renamed to `id_whisker_right` and `comp_whisker_right` since these are more consistent with the notation. Note that the name `whisker_right_id` and `whisker_right_comp` are now used for the two of the five simp lemmas presented above.
- The lemmas in `basic.lean` have been rearranged to be more logically consistent.

## Future work
I would like to apply a similar strategy for monoidal categories.
  • Loading branch information
@yuma-mizuno
yuma-mizuno committed Apr 7, 2022
1 parent 44c31d8 commit 4ff75f5
Show file tree
Hide file tree
Showing 7 changed files with 378 additions and 463 deletions.
518 changes: 255 additions & 263 deletions src/category_theory/bicategory/basic.lean
View file

Large diffs are not rendered by default.

38 changes: 10 additions & 28 deletions src/category_theory/bicategory/coherence.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -71,6 +71,11 @@ def preinclusion (B : Type u) [quiver.{v+1} B] :
map := λ a b, (inclusion_path a b).obj,
map₂ := λ a b, (inclusion_path a b).map }

@[simp]
lemma preinclusion_obj (a : B) :
(preinclusion B).obj a = a :=
rfl

/--
The normalization of the composition of `p : path a b` and `f : hom b c`.
`p` will eventually be taken to be `nil` and we then get the normalization
Expand Down Expand Up @@ -135,7 +140,7 @@ end

/-- The 2-isomorphism `normalize_iso p f` is natural in `f`. -/
lemma normalize_naturality {a b c : B} (p : path a b) {f g : hom b c} (η : f ⟶ g) :
((preinclusion B).map p ◁ η) ≫ (normalize_iso p g).hom =
(preinclusion B).map p ◁ η ≫ (normalize_iso p g).hom =
(normalize_iso p f).hom ≫ eq_to_hom (congr_arg _ (normalize_aux_congr p η)) :=
begin
rcases η, induction η,
Expand All @@ -146,37 +151,14 @@ begin
slice_lhs 1 2 { rw ihf },
simp },
case whisker_left : _ _ _ _ _ _ _ ih
{ dsimp,
slice_lhs 1 2 { rw associator_inv_naturality_right },
slice_lhs 2 3 { rw whisker_exchange },
slice_lhs 3 4 { erw ih }, /- p ≠ nil required! See the docstring of `normalize_aux`. -/
simp only [assoc] },
/- p ≠ nil required! See the docstring of `normalize_aux`. -/
{ dsimp, simp_rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc, ih, assoc] },
case whisker_right : _ _ _ _ _ h η ih
{ dsimp,
slice_lhs 1 2 { rw associator_inv_naturality_middle },
slice_lhs 2 3 { erw [←bicategory.whisker_right_comp, ih, bicategory.whisker_right_comp] },
rw [associator_inv_naturality_middle_assoc, ←comp_whisker_right_assoc, ih, comp_whisker_right],
have := dcongr_arg (λ x, (normalize_iso x h).hom) (normalize_aux_congr p (quot.mk _ η)),
dsimp at this, simp [this] },
case associator
{ dsimp,
slice_lhs 3 4 { erw associator_inv_naturality_left },
slice_lhs 1 3 { erw pentagon_hom_inv_inv_inv_inv },
simpa only [assoc, bicategory.whisker_right_comp, comp_id] },
case associator_inv
{ dsimp,
slice_rhs 2 3 { erw associator_inv_naturality_left },
slice_rhs 1 2 { erw ←pentagon_inv },
simpa only [bicategory.whisker_right_comp, assoc, comp_id] },
case left_unitor { erw [comp_id, ←triangle_assoc_comp_right_assoc], refl },
case left_unitor_inv
{ dsimp,
slice_lhs 1 2 { erw triangle_assoc_comp_left_inv },
rw [inv_hom_whisker_right, id_comp, comp_id] },
case right_unitor
{ erw [comp_id, whisker_left_right_unitor, assoc, ←right_unitor_naturality], refl },
case right_unitor_inv
{ erw [comp_id, whisker_left_right_unitor_inv, assoc, iso.hom_inv_id_assoc,
right_unitor_conjugation] }
all_goals { dsimp, dsimp [id_def, comp_def], simp }
end

@[simp]
Expand Down
66 changes: 32 additions & 34 deletions src/category_theory/bicategory/free.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -93,24 +93,28 @@ inductive rel : Π {a b : B} {f g : hom a b}, hom₂ f g → hom₂ f g → Prop
| whisker_left_id {a b c} (f : hom a b) (g : hom b c) :
rel (f ◁ 𝟙 g) (𝟙 (f.comp g))
| whisker_left_comp {a b c} (f : hom a b) {g h i : hom b c} (η : hom₂ g h) (θ : hom₂ h i) :
rel (f ◁ (η ≫ θ)) ((f ◁ η) ≫ (f ◁ θ))
rel (f ◁ (η ≫ θ)) (f ◁ η ≫ f ◁ θ)
| id_whisker_left {a b} {f g : hom a b} (η : hom₂ f g) :
rel (hom.id a ◁ η) (λ_ f ≫ η ≫ λ⁻¹_ g)
| comp_whisker_left
{a b c d} (f : hom a b) (g : hom b c) {h h' : hom c d} (η : hom₂ h h') :
rel ((f.comp g) ◁ η) (α_ f g h ≫ f ◁ g ◁ η ≫ α⁻¹_ f g h')
| whisker_right {a b c} (f g : hom a b) (h : hom b c) (η η' : hom₂ f g) :
rel η η' → rel (η ▷ h) (η' ▷ h)
| whisker_right_id {a b c} (f : hom a b) (g : hom b c) :
| id_whisker_right {a b c} (f : hom a b) (g : hom b c) :
rel (𝟙 f ▷ g) (𝟙 (f.comp g))
| whisker_right_comp {a b c} {f g h : hom a b} (i : hom b c) (η : hom₂ f g) (θ : hom₂ g h) :
rel ((η ≫ θ) ▷ i) ((η ▷ i) ≫ (θ ▷ i))
| whisker_exchange {a b c} {f g : hom a b} {h i : hom b c} (η : hom₂ f g) (θ : hom₂ h i) :
rel ((f ◁ θ) ≫ (η ▷ i)) ((η ▷ h) ≫ (g ◁ θ))
| associator_naturality_left
| comp_whisker_right {a b c} {f g h : hom a b} (i : hom b c) (η : hom₂ f g) (θ : hom₂ g h) :
rel ((η ≫ θ) ▷ i) (η ▷ i ≫ θ ▷ i)
| whisker_right_id {a b} {f g : hom a b} (η : hom₂ f g) :
rel (η ▷ hom.id b) (ρ_ f ≫ η ≫ ρ⁻¹_ g)
| whisker_right_comp
{a b c d} {f f' : hom a b} (g : hom b c) (h : hom c d) (η : hom₂ f f') :
rel (((η ▷ g) ▷ h) ≫ α_ f' g h) (α_ f g h ≫ (η ▷ (g.comp h)))
| associator_naturality_middle
rel (η ▷ (g.comp h)) (α⁻¹_ f g h ≫ η ▷ g ▷ h ≫ α_ f' g h)
| whisker_assoc
{a b c d} (f : hom a b) {g g' : hom b c} (η : hom₂ g g') (h : hom c d) :
rel (((f ◁ η) ▷ h) ≫ α_ f g' h) (α_ f g h ≫ (f ◁ (η ▷ h)))
| associator_naturality_right
{a b c d} (f : hom a b) (g : hom b c) {h h' : hom c d} (η : hom₂ h h') :
rel (((f.comp g) ◁ η) ≫ α_ f g h') (α_ f g h ≫ (f ◁ (g ◁ η)))
rel ((f ◁ η) ▷ h) (α_ f g h ≫ f ◁ (η ▷ h)≫ α⁻¹_ f g' h)
| whisker_exchange {a b c} {f g : hom a b} {h i : hom b c} (η : hom₂ f g) (θ : hom₂ h i) :
rel (f ◁ θ ≫ η ▷ i) (η ▷ h ≫ g ◁ θ)
| associator_hom_inv {a b c d} (f : hom a b) (g : hom b c) (h : hom c d) :
rel (α_ f g h ≫ α⁻¹_ f g h) (𝟙 ((f.comp g).comp h))
| associator_inv_hom {a b c d} (f : hom a b) (g : hom b c) (h : hom c d) :
Expand All @@ -119,19 +123,15 @@ inductive rel : Π {a b : B} {f g : hom a b}, hom₂ f g → hom₂ f g → Prop
rel (λ_ f ≫ λ⁻¹_ f) (𝟙 ((hom.id a).comp f))
| left_unitor_inv_hom {a b} (f : hom a b) :
rel (λ⁻¹_ f ≫ λ_ f) (𝟙 f)
| left_unitor_naturality {a b} {f f' : hom a b} (η : hom₂ f f') :
rel ((hom.id a ◁ η) ≫ λ_ f') (λ_ f ≫ η)
| right_unitor_hom_inv {a b} (f : hom a b) :
rel (ρ_ f ≫ ρ⁻¹_ f) (𝟙 (f.comp (hom.id b)))
| right_unitor_inv_hom {a b} (f : hom a b) :
rel (ρ⁻¹_ f ≫ ρ_ f) (𝟙 f)
| right_unitor_naturality {a b} {f f' : hom a b} (η : hom₂ f f') :
rel ((η ▷ hom.id b) ≫ ρ_ f') (ρ_ f ≫ η)
| pentagon {a b c d e} (f : hom a b) (g : hom b c) (h : hom c d) (i : hom d e) :
rel ((α_ f g h ▷ i) ≫ α_ f (g.comp h) i ≫ (f ◁ α_ g h i))
rel (α_ f g h ▷ i ≫ α_ f (g.comp h) i ≫ f ◁ α_ g h i)
(α_ (f.comp g) h i ≫ α_ f g (h.comp i))
| triangle {a b c} (f : hom a b) (g : hom b c) :
rel (α_ f (hom.id b) g ≫ (f ◁ λ_ g)) (ρ_ f ▷ g)
rel (α_ f (hom.id b) g ≫ f ◁ λ_ g) (ρ_ f ▷ g)

end

Expand All @@ -156,38 +156,38 @@ instance bicategory : bicategory (free_bicategory B) :=
whisker_left_id' := λ a b c f g, quot.sound (rel.whisker_left_id f g),
whisker_left_comp' := by
{ rintros a b c f g h i ⟨η⟩ ⟨θ⟩, exact quot.sound (rel.whisker_left_comp f η θ) },
id_whisker_left' := by
{ rintros a b f g ⟨η⟩, exact quot.sound (rel.id_whisker_left η) },
comp_whisker_left' := by
{ rintros a b c d f g h h' ⟨η⟩, exact quot.sound (rel.comp_whisker_left f g η) },
whisker_right := λ a b c f g η h,
quot.map (hom₂.whisker_right h) (rel.whisker_right f g h) η,
whisker_right_id' := λ a b c f g, quot.sound (rel.whisker_right_id f g),
id_whisker_right' := λ a b c f g, quot.sound (rel.id_whisker_right f g),
comp_whisker_right' := by
{ rintros a b c f g h ⟨η⟩ ⟨θ⟩ i, exact quot.sound (rel.comp_whisker_right i η θ) },
whisker_right_id' := by
{ rintros a b f g ⟨η⟩, exact quot.sound (rel.whisker_right_id η) },
whisker_right_comp' := by
{ rintros a b c f g h ⟨η⟩ ⟨θ⟩ i, exact quot.sound (rel.whisker_right_comp i η θ) },
{ rintros a b c d f f' ⟨η⟩ g h, exact quot.sound (rel.whisker_right_comp g h η) },
whisker_assoc' := by
{ rintros a b c d f g g' ⟨η⟩ h, exact quot.sound (rel.whisker_assoc f η h) },
whisker_exchange' := by
{ rintros a b c f g h i ⟨η⟩ ⟨θ⟩, exact quot.sound (rel.whisker_exchange η θ) },
associator := λ a b c d f g h,
{ hom := quot.mk rel (hom₂.associator f g h),
inv := quot.mk rel (hom₂.associator_inv f g h),
hom_inv_id' := quot.sound (rel.associator_hom_inv f g h),
inv_hom_id' := quot.sound (rel.associator_inv_hom f g h) },
associator_naturality_left' := by
{ rintros a b c d f f' ⟨η⟩ g h, exact quot.sound (rel.associator_naturality_left g h η) },
associator_naturality_middle' := by
{ rintros a b c d f g g' ⟨η⟩ h, exact quot.sound (rel.associator_naturality_middle f η h) },
associator_naturality_right' := by
{ rintros a b c d f g h h' ⟨η⟩, exact quot.sound (rel.associator_naturality_right f g η) },
left_unitor := λ a b f,
{ hom := quot.mk rel (hom₂.left_unitor f),
inv := quot.mk rel (hom₂.left_unitor_inv f),
hom_inv_id' := quot.sound (rel.left_unitor_hom_inv f),
inv_hom_id' := quot.sound (rel.left_unitor_inv_hom f) },
left_unitor_naturality' := by
{ rintros a b f f' ⟨η⟩, exact quot.sound (rel.left_unitor_naturality η) },
right_unitor := λ a b f,
{ hom := quot.mk rel (hom₂.right_unitor f),
inv := quot.mk rel (hom₂.right_unitor_inv f),
hom_inv_id' := quot.sound (rel.right_unitor_hom_inv f),
inv_hom_id' := quot.sound (rel.right_unitor_inv_hom f) },
right_unitor_naturality' := by
{ rintros a b f f' ⟨η⟩, exact quot.sound (rel.right_unitor_naturality η) },
pentagon' := λ a b c d e f g h i, quot.sound (rel.pentagon f g h i),
triangle' := λ a b c f g, quot.sound (rel.triangle f g) }

Expand Down Expand Up @@ -255,9 +255,7 @@ def lift_hom₂ : ∀ {a b : B} {f g : hom a b}, hom₂ f g → (lift_hom F f
| _ _ _ _ (hom₂.whisker_left f η) := lift_hom F f ◁ lift_hom₂ η
| _ _ _ _ (hom₂.whisker_right h η) := lift_hom₂ η ▷ lift_hom F h

local attribute [simp]
associator_naturality_left associator_naturality_middle associator_naturality_right
left_unitor_naturality right_unitor_naturality pentagon
local attribute [simp] whisker_exchange

lemma lift_hom₂_congr {a b : B} {f g : hom a b} {η θ : hom₂ f g} (H : rel η θ) :
lift_hom₂ F η = lift_hom₂ F θ :=
Expand Down
28 changes: 14 additions & 14 deletions src/category_theory/bicategory/functor.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -126,8 +126,8 @@ def oplax_functor.map₂_associator_aux
(map₂ : Π {a b : B} {f g : a ⟶ b}, (f ⟶ g) → (map f ⟶ map g))
(map_comp : Π {a b c : B} (f : a ⟶ b) (g : b ⟶ c), map (f ≫ g) ⟶ map f ≫ map g)
{a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : Prop :=
map₂ (α_ f g h).hom ≫ map_comp f (g ≫ h) ≫ (map f ◁ map_comp g h) =
map_comp (f ≫ g) h ≫ (map_comp f g ▷ map h) ≫ (α_ (map f) (map g) (map h)).hom
map₂ (α_ f g h).hom ≫ map_comp f (g ≫ h) ≫ map f ◁ map_comp g h =
map_comp (f ≫ g) h ≫ map_comp f g ▷ map h ≫ (α_ (map f) (map g) (map h)).hom

/--
An oplax functor `F` between bicategories `B` and `C` consists of a function between objects
Expand All @@ -146,19 +146,19 @@ structure oplax_functor (B : Type u₁) [bicategory.{w₁ v₁} B] (C : Type u
(map_id (a : B) : map (𝟙 a) ⟶ 𝟙 (obj a))
(map_comp {a b c : B} (f : a ⟶ b) (g : b ⟶ c) : map (f ≫ g) ⟶ map f ≫ map g)
(map_comp_naturality_left' : ∀ {a b c : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c),
map₂ (η ▷ g) ≫ map_comp f' g = map_comp f g ≫ (map₂ η ▷ map g) . obviously)
map₂ (η ▷ g) ≫ map_comp f' g = map_comp f g ≫ map₂ η ▷ map g . obviously)
(map_comp_naturality_right' : ∀ {a b c : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g'),
map₂ (f ◁ η) ≫ map_comp f g' = map_comp f g ≫ (map f ◁ map₂ η) . obviously)
map₂ (f ◁ η) ≫ map_comp f g' = map_comp f g ≫ map f ◁ map₂ η . obviously)
(map₂_id' : ∀ {a b : B} (f : a ⟶ b), map₂ (𝟙 f) = 𝟙 (map f) . obviously)
(map₂_comp' : ∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
map₂ (η ≫ θ) = map₂ η ≫ map₂ θ . obviously)
(map₂_associator' : ∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
oplax_functor.map₂_associator_aux obj (λ a b, map) (λ a b f g, map₂) (λ a b c, map_comp) f g h
. obviously)
(map₂_left_unitor' : ∀ {a b : B} (f : a ⟶ b),
map₂ (λ_ f).hom = map_comp (𝟙 a) f ≫ (map_id a ▷ map f) ≫ (λ_ (map f)).hom . obviously)
map₂ (λ_ f).hom = map_comp (𝟙 a) f ≫ map_id a ▷ map f ≫ (λ_ (map f)).hom . obviously)
(map₂_right_unitor' : ∀ {a b : B} (f : a ⟶ b),
map₂ (ρ_ f).hom = map_comp f (𝟙 b) ≫ (map f ◁ map_id b) ≫ (ρ_ (map f)).hom . obviously)
map₂ (ρ_ f).hom = map_comp f (𝟙 b) ≫ map f ◁ map_id b ≫ (ρ_ (map f)).hom . obviously)

namespace oplax_functor

Expand Down Expand Up @@ -225,11 +225,11 @@ def comp (F : oplax_functor B C) (G : oplax_functor C D) : oplax_functor B D :=
simp only [map₂_associator, ←map₂_comp_assoc, ←map_comp_naturality_right_assoc,
whisker_left_comp, assoc],
simp only [map₂_associator, map₂_comp, map_comp_naturality_left_assoc,
whisker_right_comp, assoc] },
comp_whisker_right, assoc] },
map₂_left_unitor' := λ a b f, by
{ dsimp,
simp only [map₂_left_unitor, map₂_comp, map_comp_naturality_left_assoc,
whisker_right_comp, assoc] },
comp_whisker_right, assoc] },
map₂_right_unitor' := λ a b f, by
{ dsimp,
simp only [map₂_right_unitor, map₂_comp, map_comp_naturality_right_assoc,
Expand Down Expand Up @@ -270,8 +270,8 @@ def pseudofunctor.map₂_associator_aux
(map₂ : Π {a b : B} {f g : a ⟶ b}, (f ⟶ g) → (map f ⟶ map g))
(map_comp : Π {a b c : B} (f : a ⟶ b) (g : b ⟶ c), map (f ≫ g) ≅ map f ≫ map g)
{a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : Prop :=
map₂ (α_ f g h).hom = (map_comp (f ≫ g) h).hom ≫ ((map_comp f g).hom ▷ map h) ≫
(α_ (map f) (map g) (map h)).hom ≫ (map f ◁ (map_comp g h).inv) ≫ (map_comp f (g ≫ h)).inv
map₂ (α_ f g h).hom = (map_comp (f ≫ g) h).hom ≫ (map_comp f g).hom ▷ map h ≫
(α_ (map f) (map g) (map h)).hom ≫ map f ◁ (map_comp g h).inv ≫ (map_comp f (g ≫ h)).inv

/--
A pseudofunctor `F` between bicategories `B` and `C` consists of a function between objects
Expand All @@ -293,17 +293,17 @@ structure pseudofunctor (B : Type u₁) [bicategory.{w₁ v₁} B] (C : Type u
(map₂_comp' : ∀ {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h),
map₂ (η ≫ θ) = map₂ η ≫ map₂ θ . obviously)
(map₂_whisker_left' : ∀ {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h),
map₂ (f ◁ η) = (map_comp f g).hom ≫ (map f ◁ map₂ η) ≫ (map_comp f h).inv . obviously)
map₂ (f ◁ η) = (map_comp f g).hom ≫ map f ◁ map₂ η ≫ (map_comp f h).inv . obviously)
(map₂_whisker_right' : ∀ {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
map₂ (η ▷ h) = (map_comp f h).hom ≫ (map₂ η ▷ map h) ≫ (map_comp g h).inv . obviously)
map₂ (η ▷ h) = (map_comp f h).hom ≫ map₂ η ▷ map h ≫ (map_comp g h).inv . obviously)
(map₂_associator' : ∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
pseudofunctor.map₂_associator_aux obj (λ a b, map) (λ a b f g, map₂) (λ a b c, map_comp) f g h
. obviously)
(map₂_left_unitor' : ∀ {a b : B} (f : a ⟶ b),
map₂ (λ_ f).hom = (map_comp (𝟙 a) f).hom ≫ ((map_id a).hom ▷ map f) ≫ (λ_ (map f)).hom
map₂ (λ_ f).hom = (map_comp (𝟙 a) f).hom ≫ (map_id a).hom ▷ map f ≫ (λ_ (map f)).hom
. obviously)
(map₂_right_unitor' : ∀ {a b : B} (f : a ⟶ b),
map₂ (ρ_ f).hom = (map_comp f (𝟙 b)).hom ≫ (map f ◁ (map_id b).hom) ≫ (ρ_ (map f)).hom
map₂ (ρ_ f).hom = (map_comp f (𝟙 b)).hom ≫ map f ◁ (map_id b).hom ≫ (ρ_ (map f)).hom
. obviously)

namespace pseudofunctor
Expand Down
52 changes: 7 additions & 45 deletions src/category_theory/bicategory/functor_bicategory.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,61 +31,29 @@ namespace oplax_nat_trans
def whisker_left (η : F ⟶ G) {θ ι : G ⟶ H} (Γ : θ ⟶ ι) : η ≫ θ ⟶ η ≫ ι :=
{ app := λ a, η.app a ◁ Γ.app a,
naturality' := λ a b f, by
{ dsimp,
simp only [assoc],
rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc,
associator_naturality_right_assoc, Γ.whisker_left_naturality_assoc,
associator_inv_naturality_middle] } }
{ dsimp, rw [associator_inv_naturality_right_assoc, whisker_exchange_assoc], simp } }

/-- Right whiskering of an oplax natural transformation and a modification. -/
@[simps]
def whisker_right {η θ : F ⟶ G} (Γ : η ⟶ θ) (ι : G ⟶ H) : η ≫ ι ⟶ θ ≫ ι :=
{ app := λ a, Γ.app a ▷ ι.app a,
naturality' := λ a b f, by
{ dsimp,
simp only [assoc],
rw [associator_inv_naturality_middle_assoc, Γ.whisker_right_naturality_assoc,
associator_naturality_left_assoc, ←whisker_exchange_assoc,
associator_inv_naturality_left] } }
{ dsimp, simp_rw [assoc, ←associator_inv_naturality_left, whisker_exchange_assoc], simp } }

/-- Associator for the vertical composition of oplax natural transformations. -/
@[simps]
def associator (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) : (η ≫ θ) ≫ ι ≅ η ≫ (θ ≫ ι) :=
modification_iso.of_components (λ a, α_ (η.app a) (θ.app a) (ι.app a))
begin
intros a b f,
dsimp,
simp only [whisker_right_comp, whisker_left_comp, assoc],
rw [←pentagon_inv_inv_hom_hom_inv_assoc, ←associator_naturality_left_assoc,
pentagon_hom_hom_inv_hom_hom_assoc, ←associator_naturality_middle_assoc,
←pentagon_inv_hom_hom_hom_hom_assoc, ←associator_naturality_right_assoc,
pentagon_hom_inv_inv_inv_hom]
end
modification_iso.of_components (λ a, α_ (η.app a) (θ.app a) (ι.app a)) (by tidy)

/-- Left unitor for the vertical composition of oplax natural transformations. -/
@[simps]
def left_unitor (η : F ⟶ G) : 𝟙 F ≫ η ≅ η :=
modification_iso.of_components (λ a, λ_ (η.app a))
begin
intros a b f,
dsimp,
simp only [triangle_assoc_comp_right_assoc, whisker_right_comp, assoc, whisker_exchange_assoc],
rw [←left_unitor_comp, left_unitor_naturality, left_unitor_comp],
simp only [iso.hom_inv_id_assoc, inv_hom_whisker_right_assoc, assoc, whisker_exchange_assoc]
end
modification_iso.of_components (λ a, λ_ (η.app a)) (by tidy)

/-- Right unitor for the vertical composition of oplax natural transformations. -/
@[simps]
def right_unitor (η : F ⟶ G) : η ≫ 𝟙 G ≅ η :=
modification_iso.of_components (λ a, ρ_ (η.app a))
begin
intros a b f,
dsimp,
simp only [triangle_assoc_comp_left_inv, inv_hom_whisker_right_assoc, whisker_exchange,
assoc, whisker_left_comp],
rw [←right_unitor_comp, right_unitor_naturality, right_unitor_comp],
simp only [iso.inv_hom_id_assoc, assoc]
end
modification_iso.of_components (λ a, ρ_ (η.app a)) (by tidy)

end oplax_nat_trans

Expand All @@ -96,15 +64,9 @@ variables (B C)
instance oplax_functor.bicategory : bicategory (oplax_functor B C) :=
{ whisker_left := λ F G H η _ _ Γ, oplax_nat_trans.whisker_left η Γ,
whisker_right := λ F G H _ _ Γ η, oplax_nat_trans.whisker_right Γ η,
associator := λ F G H I, oplax_nat_trans.associator,
associator := λ F G H I, oplax_nat_trans.associator,
left_unitor := λ F G, oplax_nat_trans.left_unitor,
right_unitor := λ F G, oplax_nat_trans.right_unitor,
associator_naturality_left' := by { intros, ext, apply associator_naturality_left },
associator_naturality_middle' := by { intros, ext, apply associator_naturality_middle },
associator_naturality_right' := by { intros, ext, apply associator_naturality_right },
left_unitor_naturality' := by { intros, ext, apply left_unitor_naturality },
right_unitor_naturality' := by { intros, ext, apply right_unitor_naturality },
pentagon' := by { intros, ext, apply pentagon },
triangle' := by { intros, ext, apply triangle } }
whisker_exchange' := by { intros, ext, apply whisker_exchange } }

end category_theory
Loading

0 comments on commit 4ff75f5

Please sign in to comment.