conj_id

Mathlib.CategoryTheory.Conj

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Iso.conj_id

English

Conjugating the identity by α yields the identity in the target: α.conj(id_X) = id_Y.

Русский

Сочетание конъюгации с единицей даёт единицу: α.conj(id_X) = id_Y.

LaTeX

$$$\\alpha.\\mathrm{conj}(\\mathrm{id}_X) = \\mathrm{id}_Y$$$

Lean4

@[simp]
theorem conj_id : α.conj (𝟙 X) = 𝟙 Y :=
  map_one α.conj

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

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

Разделы

Аффилиация

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