eq_of_isLocalized₀_span — Mathlib

English

If the localized maps of two submodules coincide after suitable restriction, the submodules are equal.

Русский

Если локализованные отображения двух подмодулей совпадают после ограничений, то подмодули равны.

LaTeX

$$$$\forall P\,[P^{{\mathrm{Max}}}],\; N localized^{(R_p P)}(fP) = P localized^{(R_p P)}(fP) \Rightarrow N = P.$$$$

Lean4

theorem eq_of_isLocalized₀_span {N P : Submodule R M}
    (h : ∀ r : s, N.localized₀ (.powers r.1) (f r) = P.localized₀ (.powers r.1) (f r)) : N = P :=
  le_antisymm (le_of_isLocalized_span s span_eq _ _ fun r ↦ (h r).le)
    (le_of_isLocalized_span s span_eq _ _ fun r ↦ (h r).ge)

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