tensorInvEquiv — Mathlib

English

There is an isomorphism I ⊗_R ↑I⁻¹ ≃ₗ[R] R for invertible submodule I.

Русский

Существует изоморфизм I ⊗_R ↑I⁻¹ ≃ₗ[R] R для инвертируемого подмодуля I.

LaTeX

$$$ I \\otimes_R (I)^{-1} \\simeq_R R. $$$

Lean4

/-- Given an invertible `R`-submodule `I` in an `R`-algebra `A`, the `R`-linear map
from `I ⊗[R] I⁻¹` to `R` induced by multiplication is an isomorphism. -/
noncomputable def tensorInvEquiv : I ⊗[R] ↑I⁻¹ ≃ₗ[R] R :=
  tensorEquivMul S I _ ≪≫ₗ .ofEq _ _ (I.mul_inv.trans one_eq_range) ≪≫ₗ
    .symm (.ofInjective _ (FaithfulSMul.algebraMap_injective R A))

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