instUniqueHomΩ₀

Mathlib.CategoryTheory.Topos.Classifier

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Classifier.instUniqueHomΩ₀

Lean4

instance {c : Classifier C} : ∀ Y : C, Unique (Y ⟶ c.Ω₀) := fun Y =>
  { default := c.χ₀ Y,
    uniq
      f :=
      have : f ≫ c.truth = c.χ₀ Y ≫ c.truth := by
        calc
          _ = c.χ (𝟙 Y) := c.uniq (𝟙 Y) (of_horiz_isIso_mono { })
          _ = c.χ₀ Y ≫ c.truth := by simp [← (c.isPullback (𝟙 Y)).w]
      Mono.right_cancellation _ _ this }

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

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

Разделы

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

Аффилиация

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