coprodSpec_inl

Mathlib.AlgebraicGeometry.Limits

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

English

The composition coprod.inl ≫ coprodSpec R S equals Spec.map of fst.

Русский

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

LaTeX

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

Lean4

@[simp, reassoc]
theorem coprodSpec_inl : coprod.inl ≫ coprodSpec R S = Spec.map (CommRingCat.ofHom <| RingHom.fst R S) :=
  coprod.inl_desc _ _

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

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

Разделы

Аффилиация

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