instIsLocalizationAlgebraMapSubmonoidNonZeroDivisors

English

Under the stated hypotheses, the algebra A→S induces a localization of S at the image of the non-zero divisors of R.

Русский

При заданных условиях существует локализация пространства S по образу непрерывно обратимых делителей из R.

LaTeX

$$$\\operatorname{IsLocalization}(\\operatorname{algebraMapSubmonoid} S R^{\\circ}) S'.$$$

Lean4

instance : IsLocalization (algebraMapSubmonoid S R⁰) S' :=
  have := (FaithfulSMul.algebraMap_injective R S).noZeroDivisors _ (map_zero _) (map_mul _)
  (IsLocalization.iff_of_le_of_exists_dvd _ S⁰
        (map_le_nonZeroDivisors_of_injective _ (FaithfulSMul.algebraMap_injective ..) le_rfl) fun s hs ↦
        have ⟨r, ne, eq⟩ := (alg.1 s).exists_nonzero_dvd hs
        ⟨_, ⟨r, mem_nonZeroDivisors_of_ne_zero ne, rfl⟩, eq⟩).mpr
    inferInstance

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