prodComparisonIso_id

Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

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

English

When F is the identity functor, prodComparisonIso (id C) A B is the identity isomorphism on A × B.

Русский

Если F есть тождественный функтор, то prodComparisonIso (id C) A B — это тождественный изоморфизм на A × B.

LaTeX

$$$$ prodComparisonIso (\mathsf{Id}_C) A B = .refl _ . $$$$

Lean4

@[simp]
theorem prodComparisonIso_id : prodComparisonIso (𝟭 C) A B = .refl _ := by ext <;> simp

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

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

Разделы

Аффилиация

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