cartesianMonoidalCategory

Mathlib.CategoryTheory.Monoidal.Cartesian.Over

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Over.cartesianMonoidalCategory

Lean4

/-- A choice of finite products of `Over X` given by `Limits.pullback`. -/
noncomputable abbrev cartesianMonoidalCategory (X : C) : CartesianMonoidalCategory (Over X) :=
  .ofChosenFiniteProducts
    ⟨asEmptyCone (Over.mk (𝟙 X)),
      IsTerminal.ofUniqueHom (fun Y ↦ Over.homMk Y.hom) fun Y m ↦ Over.OverMorphism.ext (by simpa using m.w)⟩
    fun Y Z ↦
    ⟨pullbackConeEquivBinaryFan.functor.obj (pullback.cone Y.hom Z.hom),
      (pullback.isLimit _ _).pullbackConeEquivBinaryFanFunctor⟩

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

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

Разделы

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

Аффилиация

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