natIso₁ — Mathlib

English

There is a natural isomorphism between the first exterior power functor and the identity functor on ModuleCat.

Русский

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

LaTeX

$$$$ \\operatorname{natIso}_1 : \\wedge^1 \\;\\cdot\\; \\text{functor} \\; R\\; 1 \\cong \\mathrm{Id}_{\\text{ModuleCat}} $$$$

Lean4

/-- The natural isomorphism `M.exteriorPower 1 ≅ M`. -/
noncomputable def natIso₁ : functor.{u} R 1 ≅ 𝟭 _ :=
  NatIso.ofComponents iso₁

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