w_app — Mathlib

English

Naturality of morphisms in CatCommSqOver with respect to a map f: X→X′ expresses that composing F.map with fst.map f and then applying the isomorphism equals applying the isomorphism first and then G.map on snd.map f.

Русский

Естественность изоморфий в CatCommSqOver относительно отображения f: X→X′ выражает, что композиция с fst.map f после F.map совпадает с применением изоморфизма до того, как применить G.map к snd.map f.

LaTeX

$$$ F.map (S.fst.map f) \circ S.iso.hom.app x' = S.iso.hom.app x \circ G.map (S.snd.map f) $$$

Lean4

@[reassoc (attr := simp)]
theorem w_app {S S' : CatCommSqOver F G X} (φ : S ⟶ S') (x : X) :
    F.map (φ.fst.app x) ≫ S'.iso.hom.app x = S.iso.hom.app x ≫ G.map (φ.snd.app x) :=
  NatTrans.congr_app φ.w x

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