submoduleInfHom — Mathlib

English

The additive submonoid generated by all images of single_R i on F.N(i) across all i equals the AddSubmonoid underlying F.submodule.

Русский

Аддитивный подмонсоид, порожденный всеми образами single_R(i) на F.N(i) по всем i, равен подмодулю F.submodule в смысле AddSubmonoid.

LaTeX

$$AddSubmonoid.closure (⋃ i, image (PolynomialModule.single R i) (F.N i : Set M)) = F.submodule.toAddSubmonoid$$

Lean4

/-- `Ideal.Filtration.submodule` as an `InfHom`. -/
noncomputable def submoduleInfHom : InfHom (I.Filtration M) (Submodule (reesAlgebra I) (PolynomialModule R M))
    where
  toFun := Ideal.Filtration.submodule
  map_inf' := inf_submodule

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