pullback_fst_map_snd_isPullback — Mathlib

English

There is an IsPullback structure for the square formed by fst composed with i₁ and the map between i₁ and i₂, with diagonal, showing a robust pullback property of the construction.

Русский

Существует структура IsPullback для квадрата, образованного fst, композиции с i₁ и отображения между i₁ и i₂ и диагонали, демонстрирующая устойчивость свойства предела.

LaTeX

$$$$ IsPullback\left( fst\,i_1,i_2 \right) $$$$

Lean4

theorem pullback_fst_map_snd_isPullback :
    IsPullback (fst _ _ ≫ i₁ ≫ fst _ _)
      (map i₁ i₂ (i₁ ≫ snd _ _) (i₂ ≫ snd _ _) _ _ _ (Category.id_comp _).symm (Category.id_comp _).symm) (diagonal f)
      (map (i₁ ≫ snd _ _) (i₂ ≫ snd _ _) f f (i₁ ≫ fst _ _) (i₂ ≫ fst _ _) i (by simp [condition])
        (by simp [condition])) :=
  IsPullback.of_iso_pullback ⟨by ext <;> simp [condition_assoc]⟩ (pullbackDiagonalMapIso f i i₁ i₂).symm
    (pullbackDiagonalMapIso.inv_fst f i i₁ i₂) (by cat_disch)

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