algebraMap_leftInverse — Mathlib

English

The left inverse property holds: algebraMapInv is a left inverse of the canonical map algebraMap from R into SymmetricAlgebra R M. In particular, for every x in R, algebraMapInv (algebraMap x) = x.

Русский

Свойство левого обратного выполняется: algebraMapInv является левым обратным от канонической карты algebraMap от R в SymmetricAlgebra R M. В частности, для каждого x в R выполняется algebraMapInv (algebraMap x) = x.

LaTeX

$$$\text{There exists } \phi:\operatorname{Sym}_R(M) \to_R R\text{ with } \phi \circ \mathrm{algebraMap}_R = \mathrm{id}_R.\quad\text{Equivalently }(\mathrm{algebraMapInv} \circ \mathrm{algebraMap}) = \mathrm{id}_R.$$$

Lean4

theorem algebraMap_leftInverse : Function.LeftInverse algebraMapInv (algebraMap R <| SymmetricAlgebra R M) := fun x =>
  by simp [algebraMapInv]

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