coeIdealHom — Mathlib

English

There is a ring homomorphism from Ideal(R) to FractionalIdeal(S,P) given by the natural embedding.

Русский

Существует кольцевой гомоморфизм от Ideal(R) в FractionalIdeal(S,P), заданный естественным включением.

LaTeX

$$$\mathrm{coeIdealHom} : \mathrm{Ideal}(R) \to+* \mathrm{FractionalIdeal}(S,P)$ with toFun = \mathrm{coeIdeal}$$$

Lean4

/-- `coeIdealHom (S : Submonoid R) P` is `(↑) : Ideal R → FractionalIdeal S P` as a ring hom -/
@[simps]
def coeIdealHom : Ideal R →+* FractionalIdeal S P
    where
  toFun := coeIdeal
  map_add' := coeIdeal_sup
  map_mul' := coeIdeal_mul
  map_one' := by rw [Ideal.one_eq_top, coeIdeal_top]
  map_zero' := coeIdeal_bot

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