isoClosure_eq_self

Mathlib.CategoryTheory.MorphismProperty.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.isoClosure_eq_self

English

If P respects isomorphisms, then P is fixed by iso-closure: P.isoClosure = P.

Русский

Если P сохраняет изоморфизм, то изоморфизационная замкнутость не меняет его: P.isoClosure = P.

LaTeX

$$$P.\\mathrm{isoClosure} = P$$$

Lean4

theorem isoClosure_eq_self (P : MorphismProperty C) [P.RespectsIso] : P.isoClosure = P := by rwa [isoClosure_eq_iff]

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

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

Разделы

Аффилиация

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