isoPullback_hom_fst — Mathlib

English

The canonical morphism from the pullback to X factors through fst, giving equality with the mate fst.

Русский

Канонический морфизм из предела к X факторизуется через fst, давая равенство с fst' (мотивируется через изоморфизм пределов).

LaTeX

$$$ h.isoPullback.hom \circ pullback.fst f g = fst $$$

Lean4

@[reassoc (attr := simp)]
theorem isoPullback_hom_fst (h : IsPullback fst snd f g) [HasPullback f g] :
    h.isoPullback.hom ≫ pullback.fst _ _ = fst :=
  by
  dsimp [isoPullback, cone, CommSq.cone]
  simp

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