English
Let T, L, R, B form a commutative square of functors between categories. Then the inverse of the canonical isomorphism iso T L R B is natural with respect to morphisms f: x → y in C₁; i.e. B.map (L.map f) ≫ (iso T L R B).inv.app y = (iso T L R B).inv.app x ≫ R.map (T.map f).
Русский
Пусть T, L, R, B образуют коммутативный квадрат функторов между категориями. Тогда обобщенная обратная часть канонического изоморфизма iso T L R B натурализована по отношению к Морфизмам f: x → y в C₁; то есть B.map (L.map f) ∘ (iso T L R B).inv.app y = (iso T L R B).inv.app x ∘ R.map (T.map f).
LaTeX
$$$ B.map (L.map f) \circ (\mathrm{iso}(T,L,R,B)^{-1}).app y = (\mathrm{iso}(T,L,R,B)^{-1}).app x \circ R.map (T.map f) $$$
Lean4
@[reassoc (attr := simp)]
theorem iso_inv_naturality [h : CatCommSq T L R B] {x y : C₁} (f : x ⟶ y) :
B.map (L.map f) ≫ (iso T L R B).inv.app y = (iso T L R B).inv.app x ≫ R.map (T.map f) :=
(iso T L R B).inv.naturality f
