isLocalHom_algebraMap — Mathlib

English

The scalar embedding R → ExteriorAlgebra R M is a local hom; it preserves local behavior with respect to maximal ideals.

Русский

Вложение скаляров R в ExteriorAlgebra R M является локальным гомоморфизмом; сохраняет локальное поведение максимальных идеалов.

LaTeX

$$$\text{IsLocalHom} (\mathrm{algebraMap}\, R\, (\mathrm{ExteriorAlgebra}\, R\, M))$$$

Lean4

@[instance]
theorem isLocalHom_algebraMap : IsLocalHom (algebraMap R (ExteriorAlgebra R M)) :=
  isLocalHom_of_leftInverse _ (algebraMap_leftInverse M)

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