pullbackIsoUnopPushout_inv_fst — Mathlib

English

For f:X→Z and g:Y→Z with pullback and pushout, the inverse of the isomorphism pullbackIsoUnopPushout composed with pullback.fst equals the unop of pushout.inl.

Русский

При f:X→Z и g:Y→Z с пулбэком и копроизведением, обратная стрелка изоморфизма pullbackIsoUnopPushout, умноженная на pullback.fst, равна unop от pushout.inl.

LaTeX

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

Lean4

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

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