coprodSpec_inr

Mathlib.AlgebraicGeometry.Limits

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.coprodSpec_inr

English

The composition coprod.inr ≫ coprodSpec R S equals Spec.map of snd.

Русский

Компоновка coprod.inr ≫ coprodSpec R S равна Spec.map snd.

LaTeX

$$$coprod.inr \\gg coprodSpec\\; R\\; S = \\Spec.map(\\CommRingCat.ofHom(\\RingHom.snd\\; R\\; S))$$$

Lean4

@[simp, reassoc]
theorem coprodSpec_inr : coprod.inr ≫ coprodSpec R S = Spec.map (CommRingCat.ofHom <| RingHom.snd R S) :=
  coprod.inr_desc _ _

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

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

Разделы

Аффилиация

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