Lean4
/-- Suppose we have a square of functors (where the top and bottom are adjunctions `L₁ ⊣ R₁`
and `L₂ ⊣ R₂` respectively).
```
C ↔ D
G ↓ ↓ H
E ↔ F
```
Then we have a bijection between natural transformations `G ⋙ L₂ ⟶ L₁ ⋙ H` and
`R₁ ⋙ G ⟶ H ⋙ R₂`. This can be seen as a bijection of the 2-cells:
```
L₁ R₁
C --→ D C ←-- D
G ↓ ↗ ↓ H G ↓ ↘ ↓ H
E --→ F E ←-- F
L₂ R₂
```
Note that if one of the transformations is an iso, it does not imply the other is an iso.
-/
@[simps]
def mateEquiv : TwoSquare G L₁ L₂ H ≃ TwoSquare R₁ H G R₂
where
toFun
α :=
.mk _ _ _ _ <|
(rightUnitor _).inv ≫
whiskerLeft (R₁ ⋙ G) adj₂.unit ≫
(associator _ _ _).hom ≫
whiskerLeft _ (associator _ _ _).inv ≫
whiskerLeft R₁ (whiskerRight α.natTrans R₂) ≫
whiskerLeft _ (associator _ _ _).hom ≫
(associator _ _ _).inv ≫ whiskerRight adj₁.counit (H ⋙ R₂) ≫ (leftUnitor _).hom
invFun
β :=
.mk _ _ _ _ <|
(leftUnitor _).inv ≫
whiskerRight adj₁.unit (G ⋙ L₂) ≫
(associator _ _ _).inv ≫
whiskerRight (associator _ _ _).hom _ ≫
whiskerRight (whiskerLeft L₁ β.natTrans) L₂ ≫
whiskerRight (associator _ _ _).inv _ ≫
(associator _ _ _).hom ≫ whiskerLeft (L₁ ⋙ H) adj₂.counit ≫ (rightUnitor _).hom
left_inv
α := by
ext
simp only [comp_obj, whiskerLeft_comp, whiskerLeft_twice, assoc, Iso.hom_inv_id_assoc, whiskerRight_comp, comp_app,
id_obj, leftUnitor_inv_app, Functor.whiskerRight_app, Functor.comp_map, associator_inv_app, associator_hom_app,
map_id, Functor.whiskerLeft_app, rightUnitor_inv_app, leftUnitor_hom_app, rightUnitor_hom_app, comp_id, id_comp,
counit_naturality, counit_naturality_assoc, left_triangle_components_assoc]
rw [← assoc, ← Functor.comp_map, α.natTrans.naturality, Functor.comp_map, assoc, ← H.map_comp,
left_triangle_components, map_id]
simp only [comp_obj, comp_id]
right_inv
β := by
ext
simp only [comp_obj, whiskerRight_comp, whiskerRight_twice, assoc, Iso.inv_hom_id_assoc, whiskerLeft_comp, comp_app,
id_obj, rightUnitor_inv_app, Functor.whiskerLeft_app, associator_hom_app, associator_inv_app,
Functor.whiskerRight_app, leftUnitor_inv_app, map_id, Functor.comp_map, rightUnitor_hom_app, leftUnitor_hom_app,
comp_id, id_comp, unit_naturality_assoc, right_triangle_components_assoc]
rw [← assoc, ← Functor.comp_map, assoc, ← β.natTrans.naturality, ← assoc, Functor.comp_map, ← G.map_comp,
right_triangle_components, map_id, id_comp]
