basicOpen_le_basicOpen_iff_algebraMap_isUnit

English

The relation basicOpen f ≤ basicOpen g is equivalent to f lying in the radical of the span of g.

Русский

Порядок сопоставления basicOpen f ≤ basicOpen g эквивалентен тому, что f лежит в радикале генерированного g (span{g}).

LaTeX

$$$$ \\mathrm{basicOpen}(f) \\le \\mathrm{basicOpen}(g) \\iff f \\in \\operatorname{radical}( \\operatorname{span} \\{ g \\} ). $$$$

Lean4

theorem basicOpen_le_basicOpen_iff_algebraMap_isUnit {f g : R} [Algebra R S] [IsLocalization.Away f S] :
    basicOpen f ≤ basicOpen g ↔ IsUnit (algebraMap R S g) := by
  simp_rw [basicOpen_le_basicOpen_iff, Ideal.mem_radical_iff, Ideal.mem_span_singleton,
    IsLocalization.Away.algebraMap_isUnit_iff f]

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