sheafedSpaceMap

Mathlib.AlgebraicGeometry.Spec

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Spec.sheafedSpaceMap

Lean4

/-- The induced map of a ring homomorphism on the ring spectra, as a morphism of sheafed spaces.
-/
@[simps base c_app]
def sheafedSpaceMap {R S : CommRingCat.{u}} (f : R ⟶ S) : Spec.sheafedSpaceObj S ⟶ Spec.sheafedSpaceObj R
    where
  base := Spec.topMap f
  c :=
    { app := fun U =>
        CommRingCat.ofHom <|
          comap f.hom (unop U) ((TopologicalSpace.Opens.map (Spec.topMap f)).obj (unop U)) fun _ => id
      naturality := fun {_ _} _ => by ext; rfl }

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru