pullbackAssoc_hom_snd_fst — Mathlib

English

Yet another equivalent expression of the same pullback associativity relation.

Русский

Ещё одно эквивалентное выражение той же самой связи ассоциативности pullback.

LaTeX

$$$\text{pullbackAssoc_inv_fst_fst}$ (third form)$$

Lean4

@[reassoc (attr := simp)]
theorem pullbackAssoc_hom_snd_fst [HasPullback ((pullback.snd _ _ : Z₁ ⟶ X₂) ≫ f₃) f₄]
    [HasPullback f₁ ((pullback.fst _ _ : Z₂ ⟶ X₂) ≫ f₂)] :
    (pullbackAssoc f₁ f₂ f₃ f₄).hom ≫ pullback.snd _ _ ≫ pullback.fst _ _ = pullback.fst _ _ ≫ pullback.snd _ _ :=
  by
  trans l₂ ≫ pullback.fst _ _
  · rw [← Category.assoc]
    congr 1
    exact IsLimit.conePointUniqueUpToIso_hom_comp _ _ WalkingCospan.right
  · exact pullback.lift_fst _ _ _

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