instIsPushout

Mathlib.RingTheory.IsTensorProduct

URI: https://scilib.ai/kg/mathlib#instIsPushout

English

The tensor product over R of S and T serves as the pushout of R → S and R → T.

Русский

Тензорное произведение S ⊗_R T служит пушаутом для стрелок R→S и R→T.

LaTeX

$$Algebra.IsPushout R S T (S ⊗[R] T)$$

Lean4

instance : Algebra.IsPushout R R S S where out := .of_equiv (TensorProduct.lid R S) fun _ ↦ by simp

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

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

Разделы

Аффилиация

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