initial_mono — Mathlib

English

In a CCC, if I is initial, then the morphism I ⟶ B is mono for every B.

Русский

В CCC, если I начальный объект, то любой морфизм I ⟶ B является монономорфизмом.

LaTeX

$$$\forall B,\; \text{Mono}(\mathrm{initial.to}\,B)$$$

Lean4

/-- If an initial object `0` exists in a CCC then every morphism from it is monic. -/
theorem initial_mono {I : C} (B : C) (t : IsInitial I) [CartesianClosed C] : Mono (t.to B) :=
  ⟨fun g h _ => by
    haveI := strict_initial t g
    haveI := strict_initial t h
    exact eq_of_inv_eq_inv (t.hom_ext _ _)⟩

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