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