preservesInitial_of_isIso — Mathlib

English

Let C and D be categories with initial objects and G : C ⥤ D a functor. If there exists an isomorphism f : ⊥_D → G(⊥_C), then G preserves the initial object; equivalently G preserves the colimit of the empty diagram.

Русский

Пусть C и D — категории с начальными объектами, а G : C → D — функтор. Если существует изоморфизм f : ⊥_D → G(⊥_C), то G сохраняет начальный объект; эквивалентно тому, что G сохраняет предел пустой диаграммы.

LaTeX

$$$(\exists f : \bot_D \to G(\bot_C))\; \mathrm{IsIso}(f) \Rightarrow \PreservesColimit(\mathrm{Functor.empty}\, C)\ G$$$

Lean4

/-- If there is any isomorphism `⊥ ⟶ G.obj ⊥`, then `G` preserves initial objects. -/
theorem preservesInitial_of_isIso (f : ⊥_ D ⟶ G.obj (⊥_ C)) [i : IsIso f] : PreservesColimit (Functor.empty.{0} C) G :=
  by
  rw [Subsingleton.elim f (initialComparison G)] at i
  exact PreservesInitial.of_iso_comparison G

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