eq_of_isLocalized_span — Mathlib

English

If N1,N2 are submodules with equal localized images across every P, then N1=N2.

Русский

Если L1 и L2 — подмодули, и их локализованные образы совпадают для каждого P, тогда N1=N2.

LaTeX

$$$$\forall P\,[P^{{\mathrm{Max}}}],\; N1 localized^{P} = N2 localized^{P} \Rightarrow N1 = N2.$$$$

Lean4

theorem eq_of_isLocalized_span (x y : M) (h : ∀ r : s, f r x = f r y) : x = y :=
  by
  suffices Module.eqIdeal R x y = ⊤ by simpa [Module.eqIdeal] using (eq_top_iff_one _).mp this
  by_contra ne
  have ⟨r, hrs, disj⟩ := exists_disjoint_powers_of_span_eq_top s span_eq _ ne
  let r : s := ⟨r, hrs⟩
  have ⟨⟨_, n, rfl⟩, eq⟩ := (IsLocalizedModule.eq_iff_exists (.powers r.1) _).mp (h r)
  exact Set.disjoint_left.mp disj eq ⟨n, rfl⟩

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