instIsClosedUnderIsomorphismsFunctorOppositeType

Mathlib.CategoryTheory.Limits.Indization.IndObject

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.IsIndObject.instIsClosedUnderIsomorphismsFunctorOppositeType

English

Ind-objects are closed under isomorphisms: if A is Ind and A ≅ B, then B is Ind.

Русский

Ind-объекты замкнуты по изоморфизмам: если A — Ind-объект и A ≅ B, то B — Ind-объект.

LaTeX

$$$\forall A,B\;\forall i\colon A\cong B,\; \mathrm{IsIndObject}(A)\Rightarrow \mathrm{IsIndObject}(B)$$$

Lean4

instance : ObjectProperty.IsClosedUnderIsomorphisms (IsIndObject (C := C)) where of_iso i h := h.map i.hom

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

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

Разделы

Аффилиация

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