isLocalHom_localRingHom — Mathlib

English

A specialized map from AtPrime to AtPrime is defined by evaluation on a projection.

Русский

Определено отображение mapPiEvalRingHom, полученное по проекции.

LaTeX

$$$\mathrm{mapPiEvalRingHom}: \mathrm{AtPrime} \text{(I)} \to \mathrm{AtPrime} \text{(I)}$.$$

Lean4

@[instance]
theorem isLocalHom_localRingHom (J : Ideal P) [hJ : J.IsPrime] (f : R →+* P) (hIJ : I = J.comap f) :
    IsLocalHom (localRingHom I J f hIJ) :=
  IsLocalHom.mk fun x hx =>
    by
    rcases IsLocalization.mk'_surjective I.primeCompl x with ⟨r, s, rfl⟩
    rw [localRingHom_mk'] at hx
    rw [AtPrime.isUnit_mk'_iff] at hx ⊢
    exact fun hr => hx ((SetLike.ext_iff.mp hIJ r).mp hr)

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