instIsIsoSymmetryOfFaithful

Mathlib.CategoryTheory.MorphismProperty.Representable

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

English

If C has pullbacks and certain preservation, then F.map f is relatively representable for any f: a ⟶ b.

Русский

Если в C существуют вытяжки и сохраняются пределы, то F.map f относительно представимо для любого f: a ⟶ b.

LaTeX

$$$$ F.relativelyRepresentable (F.map f) $$$$

Lean4

instance [Full F] [Faithful F] : IsIso (hf'.symmetry hg) :=
  (hf'.symmetryIso hg).isIso_hom

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

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

Разделы

Аффилиация

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