mapDesc_comp — Mathlib

English

A second formulation of mapDesc compatibility with composition, illustrating coherence of the construction.

Русский

Вторая формулировка совместимости mapDesc с композицией демонстрирует когерентность построения.

LaTeX

$$$\mathrm{pullback.mapDesc} f g (i i') = \mathrm{pullback.mapDesc} f g i \, \circ \, \mathrm{pullback.mapDesc} _ _ i' \, \circ \, (\mathrm{pullback.congrHom} \mathbf{1} \mathbf{1}).hom$$$

Lean4

theorem mapDesc_comp {X Y S T S' : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) (i' : S ⟶ S') [HasPullback f g]
    [HasPullback (f ≫ i) (g ≫ i)] [HasPullback (f ≫ i ≫ i') (g ≫ i ≫ i')] [HasPullback ((f ≫ i) ≫ i') ((g ≫ i) ≫ i')] :
    pullback.mapDesc f g (i ≫ i') =
      pullback.mapDesc f g i ≫
        pullback.mapDesc _ _ i' ≫ (pullback.congrHom (Category.assoc _ _ _) (Category.assoc _ _ _)).hom :=
  by cat_disch

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