English
Invertibility in the exterior algebra corresponds to invertibility in the base ring: there is a natural equivalence between invertible elements of algebraMap(R, ExteriorAlgebra(R,M)) and invertible elements of R.
Русский
Обратимость в внешней алгебре соответствует обратимости в базовом кольце: существует естественное эквивалентное соотношение между инвертируемыми элементами algebraMap(R, ExteriorAlgebra(R,M)) и инвертируемыми элементами R.
LaTeX
$$$\mathrm{Invertible}(\mathrm{algebraMap}_R(\mathrm{ExteriorAlgebra} \ R \ M)) \simeq \mathrm{Invertible}(R)$$$
Lean4
/-- Invertibility in the exterior algebra is the same as invertibility of the base ring. -/
@[simps!]
def invertibleAlgebraMapEquiv (r : R) : Invertible (algebraMap R (ExteriorAlgebra R M) r) ≃ Invertible r :=
invertibleEquivOfLeftInverse _ _ _ (algebraMap_leftInverse M)
