English
Any monomorphism in Type is a coproduct injection: if f: X → Y is mono, then the cofan with left leg f and right leg Subtype.val is a colimit.
Русский
Любой моно отображение в Type является инъекцией копрода: если f: X → Y моно, то бинарный коэфан с левой ножкой f и правой ножкой Subtype.val образует колимит.
LaTeX
$$$$ IsColimit (BinaryCofan.mk f Subtype.val) $$$$
Lean4
/-- Any monomorphism in `Type` is a coproduct injection. -/
noncomputable def isCoprodOfMono {X Y : Type u} (f : X ⟶ Y) [Mono f] :
IsColimit (BinaryCofan.mk f (Subtype.val : ↑(Set.range f)ᶜ → Y)) :=
by
apply Nonempty.some
rw [binaryCofan_isColimit_iff]
refine ⟨(mono_iff_injective f).mp inferInstance, Subtype.val_injective, ?_⟩
symm
rw [← eq_compl_iff_isCompl]
exact Subtype.range_val