English
An ideal I of R equals the infimum of the comap/map family along Away- localizations, provided a span condition holds.
Русский
Идеал I равен инфимууму по семейству comap/map над локализациями Away при выполнении условия покрытия.
LaTeX
$$$I=\\bigwedge_{f\\in S}(\\operatorname{Ideal.comap}(\\mathrm{algebraMap}\\;R\\;\\mathrm{Localization.Away}f)(\\operatorname{Ideal.map}(\\mathrm{algebraMap}\\;R\\;\\mathrm{Localization.Away}f)I))$$$
Lean4
theorem ideal_eq_iInf_comap_map_away {S : Finset R} (hS : Ideal.span (α := R) S = ⊤) (I : Ideal R) :
I = ⨅ f ∈ S, (I.map (algebraMap R (Localization.Away f))).comap (algebraMap R (Localization.Away f)) :=
by
apply le_antisymm
· simp only [le_iInf₂_iff, ← Ideal.map_le_iff_le_comap, le_refl, implies_true]
· intro x hx
apply Submodule.mem_of_span_eq_top_of_smul_pow_mem _ _ hS
rintro ⟨s, hs⟩
simp only [Ideal.mem_iInf, Ideal.mem_comap] at hx
obtain ⟨⟨y, ⟨_, n, rfl⟩⟩, e⟩ := (IsLocalization.mem_map_algebraMap_iff (.powers s) _).mp (hx s hs)
dsimp only at e
rw [← map_mul, IsLocalization.eq_iff_exists (.powers s)] at e
obtain ⟨⟨_, m, rfl⟩, e⟩ := e
use m + n
dsimp at e ⊢
rw [pow_add, mul_assoc, ← mul_comm x, e]
exact I.mul_mem_left _ y.2
