stalkMap_toStalk — Mathlib

English

A simp lemma asserting the equality of stalk maps through the equivalence of categories; a simplification step.

Русский

Упрощенное лемма равенства stalk maps через эквивалентность категорий.

LaTeX

$$$\text{stalkMap\_simp\_1}$$$

Lean4

@[elementwise]
theorem stalkMap_toStalk {R S : CommRingCat.{u}} (f : R ⟶ S) (p : PrimeSpectrum S) :
    toStalk R (PrimeSpectrum.comap f.hom p) ≫ (Spec.sheafedSpaceMap f).stalkMap p = f ≫ toStalk S p :=
  by
  rw [← toOpen_germ S ⊤ p trivial, ← toOpen_germ R ⊤ (PrimeSpectrum.comap f.hom p) trivial, Category.assoc]
  erw [PresheafedSpace.stalkMap_germ (Spec.sheafedSpaceMap f) ⊤ p trivial]
  rw [Spec.sheafedSpaceMap_c_app]
  erw [toOpen_comp_comap_assoc]
  rfl

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