English
The unit element of the colimit is the image of the unit in any component; i.e., the colimit unit equals the representative with j and the unit of F.obj j.
Русский
Единица коллимита совпадает с образцом единицы в любой компоненте диаграммы; то есть единица коллимита равна элементу вида (j, 1).
LaTeX
$$$1 = M.mk F \langle j, 1 \rangle$$$
Lean4
/-- The definition of the "one" in the colimit is independent of the chosen object of `J`.
In particular, this lemma allows us to "unfold" the definition of `colimit_one` at a custom chosen
object `j`.
-/
@[to_additive /-- The definition of the "zero" in the colimit is independent of the chosen object
of `J`. In particular, this lemma allows us to "unfold" the definition of `colimit_zero` at
a custom chosen object `j`. -/
]
theorem colimit_one_eq (j : J) : (1 : M.{v, u} F) = M.mk F ⟨j, 1⟩ :=
by
apply M.mk_eq
refine ⟨max' _ j, IsFiltered.leftToMax _ j, IsFiltered.rightToMax _ j, ?_⟩
simp
