isLocalHom_stalkClosedPointTo' — Mathlib

English

A variant stating that for Spec (.of R) → X, the induced stalk map to X is a local homomorphism.

Русский

Вариант утверждает, что для Spec(.of R) → X индуцированная стоячая карта в X есть локальный гомоморфизм.

LaTeX

$$$\\text{IsLocalHom}\\big(\\operatorname{stalkClosedPointTo} f\\big).hom$$$

Lean4

/-- Copy of `isLocalHom_stalkClosedPointTo` which unbundles the comm ring.

Useful for use in combination with `CommRingCat.of K` for a field `K`.
-/
instance isLocalHom_stalkClosedPointTo' {R : Type u} [CommRing R] [IsLocalRing R] (f : Spec (.of R) ⟶ X) :
    IsLocalHom (stalkClosedPointTo f).hom :=
  isLocalHom_stalkClosedPointTo f

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