pushoutCocone_pt

Mathlib.Algebra.Category.Ring.Constructions

URI: https://scilib.ai/kg/mathlib#CommRingCat.pushoutCocone_pt

English

The apex of the pushout cocone is the base ring corresponding to A ⊗_R B.

Русский

Вершина кокона пуш-аут соответствует кольцу $A\\otimes_R B$.

LaTeX

$$$(pushoutCocone R A B).pt = \\mathrm{of}(A \\otimes_R B)$$

Lean4

@[simp]
theorem pushoutCocone_pt : (pushoutCocone R A B).pt = CommRingCat.of (A ⊗[R] B) :=
  rfl

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

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

Разделы

Аффилиация

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