pullbackIsoUnopPushout_hom_inl — Mathlib

English

A noncomputable definition giving an equivalence between IsColimit of a pushout cocone in Opposite C and IsLimit of its unop.

Русский

Не вычисляемое определение задающее эквивалентность между IsColimit кокона копроизведения в Opposite C и IsLimit его unop.

LaTeX

$$$$ \mathrm{Equiv}(\mathrm{IsColimit}(\mathrm{PushoutCocone}\; f\; g), \mathrm{IsLimit}(\mathrm{PushoutCocone}\; f\; g)^{\mathrm{unop}}). $$$$

Lean4

@[reassoc (attr := simp)]
theorem pullbackIsoUnopPushout_hom_inl {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] [HasPushout f.op g.op] :
    pushout.inl _ _ ≫ (pullbackIsoUnopPushout f g).hom.op = (pullback.fst f g).op :=
  by
  apply Quiver.Hom.unop_inj
  dsimp
  rw [← pullbackIsoUnopPushout_inv_fst, Iso.hom_inv_id_assoc]

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