localRingHom_comp_stalkIso — Mathlib

English

A comparison between the composition of localization homs and stalk maps with the stalkIsos; shows a compatibility of local ring homomorphisms with stalks and Spec.sheafedSpaceMap.

Русский

Сопоставление композиции локализационных гомоморфизмов и stalkIsos с stalkMap и Spec.sheafedSpaceMap демонстрирует совместимость локальных кольцевых гомоморфизмов с stalk и Spec.

LaTeX

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

Lean4

/-- Under the isomorphisms `stalkIso`, the map `stalkMap (Spec.sheafedSpaceMap f) p` corresponds
to the induced local ring homomorphism `Localization.localRingHom`.
-/
@[elementwise]
theorem localRingHom_comp_stalkIso {R S : CommRingCat.{u}} (f : R ⟶ S) (p : PrimeSpectrum S) :
    (stalkIso R (PrimeSpectrum.comap f.hom p)).hom ≫
        (CommRingCat.ofHom (Localization.localRingHom (PrimeSpectrum.comap f.hom p).asIdeal p.asIdeal f.hom rfl)) ≫
          (stalkIso S p).inv =
      (Spec.sheafedSpaceMap f).stalkMap p :=
  (stalkIso R (PrimeSpectrum.comap f.hom p)).eq_inv_comp.mp <|
    (stalkIso S p).comp_inv_eq.mpr <|
      CommRingCat.hom_ext <|
        Localization.localRingHom_unique _ _ _ (PrimeSpectrum.comap_asIdeal _ _) fun x => by
          -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644 and https://github.com/leanprover-community/mathlib4/pull/8386

          rw [stalkIso_hom, stalkIso_inv, CommRingCat.comp_apply, CommRingCat.comp_apply, localizationToStalk_of,
            stalkMap_toStalk_apply f p x]
          erw [stalkToFiberRingHom_toStalk]
          rfl

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