iso_hom_naturality — Mathlib

English

For CatCommSqOver structure, the naturality of the iso hom expresses that the square commutes with the action of a whiskered morphism on the left and right components.

Русский

В структуре CatCommSqOver естествность изоморфизма hom выражает, что квадрат коммутирует с действием морфицирований по левой и правой частям.

LaTeX

$$$S.iso.hom \\text{ is natural: } F.map (S.fst.map f) \\circ S.iso.hom = S.iso.hom \\circ G.map (S.snd.map f)$$$

Lean4

@[reassoc (attr := simp)]
theorem iso_hom_naturality (S : CatCommSqOver F G X) {x x' : X} (f : x ⟶ x') :
    F.map (S.fst.map f) ≫ S.iso.hom.app x' = S.iso.hom.app x ≫ G.map (S.snd.map f) :=
  S.iso.hom.naturality f

Похожие утверждения