English
Let f: R → S and g: S → T be ring homomorphisms. Then the morphism on spectra associated to the composition f ∘ g equals the composition of the morphisms associated to g and f, i.e. the map Spec.locallyRingedSpaceMap respects composition in the opposite order.
Русский
Пусть f: R → S и g: S → T — гомоморфизмы колец. Тогда отображение спектра, соответствующее композиции f ∘ g, равняется композиции отображений, соответствующих g и f, то есть карта Spec.locallyRingedSpaceMap хранит композицию в противоположном порядке.
LaTeX
$$$\operatorname{Spec.locallyRingedSpaceMap}(f \circ g) = \operatorname{Spec.locallyRingedSpaceMap}(g) \circ \operatorname{Spec.locallyRingedSpaceMap}(f).$$$
Lean4
theorem locallyRingedSpaceMap_comp {R S T : CommRingCat.{u}} (f : R ⟶ S) (g : S ⟶ T) :
Spec.locallyRingedSpaceMap (f ≫ g) = Spec.locallyRingedSpaceMap g ≫ Spec.locallyRingedSpaceMap f :=
LocallyRingedSpace.Hom.ext' <| by rw [Spec.locallyRingedSpaceMap_toShHom, Spec.sheafedSpaceMap_comp]; rfl
