tensorObjDesc

Mathlib.CategoryTheory.GradedObject.Monoidal

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GradedObject.Monoidal.tensorObjDesc

Lean4

/-- Constructor for morphisms from a tensor product of two graded objects. -/
noncomputable def tensorObjDesc {A : C} {k : I} (f : ∀ (i₁ i₂ : I) (_ : i₁ + i₂ = k), X₁ i₁ ⊗ X₂ i₂ ⟶ A) :
    tensorObj X₁ X₂ k ⟶ A :=
  mapBifunctorMapObjDesc f

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

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

Разделы

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

Аффилиация

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