isLocalHom_toRingHom — Mathlib

English

If a generalized local hom f is given, then its underlying ring hom is local as well.

Русский

Если дан локальный гомоморфизм f в обобщенной форме, то связанный с ним кольцевой гомоморфизм тоже локальный.

LaTeX

$$$\text{IsLocalHom}(f) \Rightarrow \text{IsLocalHom}(f: R \to S)$$$

Lean4

@[instance 100]
theorem isLocalHom_toRingHom {F : Type*} [FunLike F R S] [RingHomClass F R S] (f : F) [IsLocalHom f] :
    IsLocalHom (f : R →+* S) :=
  ⟨IsLocalHom.map_nonunit (f := f)⟩

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