localRingHom_comp_stalkIso_apply'

English

A variant of the application lemma for localRingHom_comp_stalkIso; expresses the componentwise equality on stalks.

Русский

Вариант утверждения применимости для localRingHom_comp_stalkIso; выражает компонентную равенство на stalk-областях.

LaTeX

$$$\text{localRingHom\_comp\_stalkIso\_apply'}$$$

Lean4

/-- Version of `localRingHom_comp_stalkIso_apply` using `CommRingCat.Hom.hom` -/
theorem localRingHom_comp_stalkIso_apply' {R S : CommRingCat.{u}} (f : R ⟶ S) (p : PrimeSpectrum S) (x) :
    (stalkIso S p).inv
        ((Localization.localRingHom (PrimeSpectrum.comap f.hom p).asIdeal p.asIdeal f.hom rfl)
          ((stalkIso R (PrimeSpectrum.comap f.hom p)).hom x)) =
      (Spec.sheafedSpaceMap f).stalkMap p x :=
  localRingHom_comp_stalkIso_apply _ _ _

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