map_commSq

Mathlib.CategoryTheory.CommSq

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.map_commSq

← MathLib Explorer

English

A functor maps a commutative square to a commutative square.

Русский

Функтор отображает коммутативный квадрат в коммутативный квадрат.

LaTeX

$$$s\,:\, CommSq f g h i \to CommSq (F.map f) (F.map g) (F.map h) (F.map i)$$$

Lean4

theorem map_commSq (s : CommSq f g h i) : CommSq (F.map f) (F.map g) (F.map h) (F.map i) :=
  ⟨by simpa using congr_arg (fun k : W ⟶ Z => F.map k) s.w⟩

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

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

Разделы

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

Аффилиация

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