of_map — Mathlib

English

Any two morphisms between objects in the WalkingCospan are equal; the hom-sets in WalkingCospan are singleton.

Русский

Похоже, что любые две стрелки между объектами в WalkingCospan равны; множество гомоморфизмов в WalkingCospan является единичным.

LaTeX

$$$ \\forall X,Y \\in \\mathrm{WalkingCospan},\\; X\\to Y \\text{ is unique} $$$

Lean4

theorem of_map [ReflectsColimit (span f g) F] (e : f ≫ h = g ≫ i)
    (H : IsPushout (F.map f) (F.map g) (F.map h) (F.map i)) : IsPushout f g h i :=
  by
  refine ⟨⟨e⟩, ⟨isColimitOfReflects F <| ?_⟩⟩
  refine (IsColimit.equivOfNatIsoOfIso (spanCompIso F f g) _ _ (WalkingSpan.ext ?_ ?_ ?_)).symm H.isColimit
  exacts [Iso.refl _, (Category.comp_id _).trans (Category.id_comp _), (Category.comp_id _).trans (Category.id_comp _)]

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