English
The unbundled directLimit of modules is a colimit in the sense of CategoryTheory; the constructed cocone is universal for the diagram.
Русский
Необъединенный прямой предел модулей является колимотом в смысле CategoryTheory; сконструированный кокон универсален для диаграммы.
LaTeX
$$$\\text{directLimitIsColimit }(G,f)$$$
Lean4
/-- The unbundled `directLimit` of modules is a colimit
in the sense of `CategoryTheory`. -/
@[simps]
def directLimitIsColimit : IsColimit (directLimitCocone G f)
where
desc
s :=
ofHom <|
Module.DirectLimit.lift R ι G f (fun i => (s.ι.app i).hom) fun i j h x =>
by
simp only [Functor.const_obj_obj]
rw [← s.w (homOfLE h)]
rfl
fac s
i := by
ext
dsimp only [hom_comp, directLimitCocone, hom_ofHom, LinearMap.comp_apply]
apply DirectLimit.lift_of
uniq s m
h :=
by
have : s.ι.app = fun i => (ofHom (DirectLimit.of R ι (fun i => G i) (fun i j H => f i j H) i)) ≫ m :=
by
funext i
rw [← h]
rfl
ext
simp [this]
