of_isIso

Mathlib.CategoryTheory.MorphismProperty.Representable

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

← MathLib Explorer

English

If F is full, then IsPullback (F.map (hf'.fst' g)) (F.map (hf'.snd g)) f' g holds.

Русский

Если F полно, IsPullback (F.map (hf'.fst' g)) (F.map (hf'.snd g)) f' g выполняется.

LaTeX

$$$IsPullback (F.map (hf'.fst' g)) (F.map (hf'.snd g)) f' g$$$

Lean4

theorem of_isIso {X Y : D} (f : X ⟶ Y) [IsIso f] : F.relativelyRepresentable f := fun a g ↦
  ⟨a, 𝟙 a, g ≫ CategoryTheory.inv f, IsPullback.of_vert_isIso ⟨by simp⟩⟩

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

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

Разделы

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

Аффилиация

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