coeSubmoduleHom — Mathlib

English

There is a ring homomorphism from FractionalIdeal S P to Submodule R P given by the underlying submodule.

Русский

Существует гомоморфизм колебания (кольцевой) от дробных идеалов к подмодулям, задаваемый подлежащим подмодулем.

LaTeX

$$$\text{coeSubmoduleHom} : \mathrm{FractionalIdeal}(S,P) \to^+* \mathrm{Submodule}(R,P)$ with \text{toFun} = \mathrm{coeToSubmodule}$$$

Lean4

/-- `FractionalIdeal.coeToSubmodule` as a bundled `RingHom`. -/
@[simps]
def coeSubmoduleHom : FractionalIdeal S P →+* Submodule R P
    where
  toFun := coeToSubmodule
  map_one' := coe_one
  map_mul' := coe_mul
  map_zero' := coe_zero (S := S)
  map_add' := coe_add

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