sheafedSpaceMap_comp — Mathlib

English

For morphisms of rings, the map on the associated sheafed spaces (via Spec) respects composition: Spec.sheafedSpaceMap(f ≫ g) equals Spec.sheafedSpaceMap(g) ∘ Spec.sheafedSpaceMap(f).

Русский

Для морфизмов колец отображение между связанных пространствами сохраняет компоновку: Spec.sheafedSpaceMap( f ≫ g ) = Spec.sheafedSpaceMap(g) ∘ Spec.sheafedSpaceMap(f).

LaTeX

$$$\\mathrm{Spec.sheafedSpaceMap}(f \\circ g) = \\mathrm{Spec.sheafedSpaceMap}(g) \\circ \\mathrm{Spec.sheafedSpaceMap}(f)$$$

Lean4

theorem sheafedSpaceMap_comp {R S T : CommRingCat.{u}} (f : R ⟶ S) (g : S ⟶ T) :
    Spec.sheafedSpaceMap (f ≫ g) = Spec.sheafedSpaceMap g ≫ Spec.sheafedSpaceMap f :=
  AlgebraicGeometry.PresheafedSpace.Hom.ext _ _ (Spec.topMap_comp f g) <|
    by
    ext
      -- Porting note: was one liner
          -- `dsimp, rw category_theory.functor.map_id, rw category.comp_id, erw comap_comp f g, refl`

    rw [NatTrans.comp_app, sheafedSpaceMap_c_app, Functor.whiskerRight_app, eqToHom_refl]
    erw [(sheafedSpaceObj T).presheaf.map_id]
    dsimp only [CommRingCat.hom_comp, RingHom.coe_comp, Function.comp_apply]
    rw [comap_comp]
    rfl

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