pullbackIsoUnopPushout_inv_snd — Mathlib

English

The analogous equality holds with pullback.snd and pushout.inr under the same hypotheses.

Русский

Аналогичное равенство выполняется для pullback.snd и pushout.inr в тех же гипотезах.

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem pullbackIsoUnopPushout_inv_snd {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] [HasPushout f.op g.op] :
    (pullbackIsoUnopPushout f g).inv ≫ pullback.snd f g = (pushout.inr _ _ : _ ⟶ pushout f.op g.op).unop :=
  (IsLimit.conePointUniqueUpToIso_inv_comp _ _ _).trans (by simp [unop_id (X := { unop := Y })])

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