pullbackAssoc_hom_snd_snd — Mathlib

English

The corresponding associativity identity for the push/pull of the second component holds.

Русский

Соответствующее тождество ассоциативности для второй компоненты выполняется.

LaTeX

$$$\text{pullbackAssoc_hom_snd_snd}$$$

Lean4

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

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