mk — Mathlib · SciLib

English

There is a natural isomorphism between the functor M ↦ ∧^0 M and the constant functor at ModuleCat.of R R.

Русский

Существует естественный изоморфизм между функтором M ↦ ∧^0 M и константным функтором в ModuleCat.of R R.

LaTeX

$$$$ \\operatorname{natIso}_0 : \\wedge^0 \;(-) \\cong \\mathrm{Const}_{R}(\\,\\!R\\, ) $$$$

Lean4

/-- The canonical projection into the colimit, as a quotient type. -/
def mk : (Σ j, F.obj j) → M F := fun x ↦ (F ⋙ forget (ModuleCat R)).ιColimitType x.1 x.2

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