English
In a CatCommSq square of functors T, L, R, B, the naturality of the hom component of the iso between R⊗T and B⊗L is given by the standard naturality equation: R.map (T.map f) ; iso.hom.app y = iso.hom.app x ; B.map (L.map f).
Русский
В квадрате CatCommSq для категориальных функций T, L, R, B натуральность компоненты гомоморфизма изоморфизма между R∘T и B∘L задаётся стандартным уравнением натуральности: R.map (T.map f) ; hom = hom ; B.map (L.map f).
LaTeX
$$$R.map (T.map f) \\\\; \\\\; (\\\\text{iso}(T,L,R,B)).hom.{app}\\text{ } y = (\\\\text{iso}(T,L,R,B)).hom.{app} x \\\\;\\\\; B.map (L.map f)$$$
Lean4
@[reassoc (attr := simp)]
theorem iso_hom_naturality [h : CatCommSq T L R B] {x y : C₁} (f : x ⟶ y) :
R.map (T.map f) ≫ (iso T L R B).hom.app y = (iso T L R B).hom.app x ≫ B.map (L.map f) :=
(iso T L R B).hom.naturality f
