prodComparison_id

Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CartesianMonoidalCategory.prodComparison_id

English

If prodComparison F A B is an iso, then inv(prodComparison F A B) ≫ F.map (fst A B) = fst (F.obj A) (F.obj B).

Русский

Если prodComparison F A B изоморфизм, то inv(prodComparison F A B) ∘ F.map(fst(A,B)) = fst(F A, F B).

LaTeX

$$inv (prodComparison F A B) ≫ F.map (fst A B) = fst (F.obj A) (F.obj B)$$

Lean4

@[simp]
theorem prodComparison_id : prodComparison (𝟭 C) A B = 𝟙 (A ⊗ B) :=
  lift_fst_snd

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

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

Разделы

Аффилиация

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