pullbackAssoc_inv_fst_fst — Mathlib

English

A certain associativity equality of pullback inverses and projections holds.

Русский

Сохранение равенства между инверсией объединенного pullback и проекциями.

LaTeX

$$$(\text{pullbackAssoc } f_1 f_2 f_3 f_4)^{-1} \circ \text{pullback.fst} \circ \text{pullback.fst} = \text{pullback.fst} \circ (\text{pullback.snd} f_1 f_2) \Rightarrow \text{равенство}$$$

Lean4

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

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