inr_comp_pushoutSymmetry_hom — Mathlib

English

The pushout symmetry interchanges the two inclusions of the pushout: pushout.inr composed with the symmetry equals pushout.inl.

Русский

Симметрия пушпойнта переставляет инклюзии: pushout.inr ≫ (pushoutSymmetry).hom = pushout.inl.

LaTeX

$$$\mathrm{pushout.inr} f g \; ≫ \; (\mathrm{pushoutSymmetry} f g).\mathrm{hom} = \mathrm{pushout.inl} g f.$$$

Lean4

@[reassoc (attr := simp)]
theorem inr_comp_pushoutSymmetry_hom [HasPushout f g] : pushout.inr _ _ ≫ (pushoutSymmetry f g).hom = pushout.inl _ _ :=
  (colimit.isColimit (span f g)).comp_coconePointUniqueUpToIso_hom (PushoutCocone.flipIsColimit (pushoutIsPushout g f))
    _

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