isUnit_to_map_iff — Mathlib

English

The natural R-action on Localization.AtPrime S P is faithful; i.e., the algebra map R → Localization.AtPrime I is injective on S.

Русский

Натуральное действие R на Localization.AtPrime S P безошибочно сохраняет структуру; отображение R → Localization.AtPrime I инъективно на S.

LaTeX

$$$$ \text{faithfulSMul } R\ S $$$$

Lean4

theorem isUnit_to_map_iff (x : R) : IsUnit ((algebraMap R S) x) ↔ x ∈ I.primeCompl :=
  ⟨fun h hx =>
    (isPrime_of_isPrime_disjoint I.primeCompl S I hI disjoint_compl_left).ne_top <|
      (Ideal.map (algebraMap R S) I).eq_top_of_isUnit_mem (Ideal.mem_map_of_mem _ hx) h,
    fun h => map_units S ⟨x, h⟩⟩
    -- Can't use typeclasses to infer the `IsLocalRing` instance, so use an `optParam` instead
    -- (since `IsLocalRing` is a `Prop`, there should be no unification issues.)

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