isColimitMapCoconePushoutCoconeEquiv

English

The inverse map of the pushout inl under a preserving functor coincides with the mapped inl.

Русский

Обратный отображатель у pushout.inl после сохранения функтором совпадает с отображением inl.

LaTeX

$$$PreservesPushout.iso G f g)^{-1} \\circ G.map(pushout.inl f g) = pushout.inl (G.map f) (G.map g)$$$

Lean4

/-- The map of a pushout cocone is a colimit iff the cofork consisting of the mapped morphisms is a
colimit. This essentially lets us commute `PushoutCocone.mk` with `Functor.mapCocone`. -/
def isColimitMapCoconePushoutCoconeEquiv :
    IsColimit (mapCocone G (PushoutCocone.mk h k comm)) ≃
      IsColimit
        (PushoutCocone.mk (G.map h) (G.map k) (by simp only [← G.map_comp, comm]) :
          PushoutCocone (G.map f) (G.map g)) :=
  (IsColimit.precomposeHomEquiv (diagramIsoSpan.{v₂} _).symm _).symm.trans <|
    IsColimit.equivIsoColimit <|
      Cocones.ext (Iso.refl _) <| by
        rintro (_ | _ | _) <;> dsimp <;> simp only [Category.comp_id, Category.id_comp, ← G.map_comp]

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