pullbackIsoUnopPushout_hom_inr — Mathlib

English

The morphism pushout.inr(op) composed with the hom part of pullbackIsoUnopPushout equals the op of pullback.snd.

Русский

Гомоморфизм pushout.inr(op) после композиции с hom-частью pullbackIsoUnopPushout равен op от pullback.snd.

LaTeX

$$$$\; pushout.inr(f^{op},g^{op})^{op} \circ (\mathrm{pullbackIsoUnopPushout}(f,g))^{op} = (\mathrm{pullback.snd}(f,g))^{op}. $$$$

Lean4

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

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