natIso₀ — Mathlib

English

There is a natural isomorphism between the zero-th exterior power functor and the constant functor with value R.

Русский

Существует естественный изоморфизм между функцией нулевой внешней степени и константной функцией со значением R.

LaTeX

$$$$ \\operatorname{natIso}_0 : \\wedge^0 \\;\\cdot\\; \\text{functor} \\; R\\; 0 \\cong (\\mathrm{Functor.const}\\; _).\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\!\\! \\text{(ModuleCat.of } R R) $$$$

Lean4

/-- The natural isomorphism `M.exteriorPower 0 ≅ ModuleCat.of R R`. -/
noncomputable def natIso₀ : functor.{u} R 0 ≅ (Functor.const _).obj (ModuleCat.of R R) :=
  NatIso.ofComponents iso₀

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