inl_pushoutLeftPushoutInrIso_inv — Mathlib

English

The left leg of a pushout pasting admits an associated iso that makes a simple coherence with the inl maps hold.

Русский

Левая нога пушаута, склейка из которой образует изоморфизм, удовлетворяющий простое когерентное равенство с картами inl.

LaTeX

$$$(\\mathrm{pushout.inl} f g) \\circ (\\mathrm{pushoutLeftPushoutInrIso}(f,g,g')).inv = \\mathrm{pushout.inl} f g' \\circ \\mathrm{pushout.inl}(\\mathrm{pushout.inr} f g, g')$$$

Lean4

@[reassoc (attr := simp)]
theorem inl_pushoutLeftPushoutInrIso_inv :
    (pushout.inl f (g ≫ g')) ≫ (pushoutLeftPushoutInrIso f g g').inv =
      (pushout.inl f g) ≫ (pushout.inl (pushout.inr f g) g') :=
  IsColimit.comp_coconePointUniqueUpToIso_inv _ _ WalkingSpan.left

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