pullbackAssoc_hom_fst — Mathlib

English

Another formulation of the previous associativity identity for pullbacks.

Русский

Другая формулировка предыдущего тождества ассоциативности pullback.

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem pullbackAssoc_hom_fst [HasPullback ((pullback.snd _ _ : Z₁ ⟶ X₂) ≫ f₃) f₄]
    [HasPullback f₁ ((pullback.fst _ _ : Z₂ ⟶ X₂) ≫ f₂)] :
    (pullbackAssoc f₁ f₂ f₃ f₄).hom ≫ pullback.fst _ _ = pullback.fst _ _ ≫ pullback.fst _ _ := by
  rw [← Iso.eq_inv_comp, pullbackAssoc_inv_fst_fst]

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