English
If the projection maps are epi and the cone is limiting, then Profinite.Extend.functorOp is initial.
Русский
Если проекции являются эпиморфизмами, а конус ограничивает, то Profinite.Extend.functorOp является начальником.
LaTeX
$$$\\mathrm{functorOp\\_initial}:\\ \\text{Initial }(\\mathrm{functor\\_Op})$$$
Lean4
/-- If the projection maps in the cone are epimorphic and the cone is limiting, then
`Profinite.Extend.functor` is initial.
TODO: investigate how to weaken the assumption `∀ i, Epi (c.π.app i)` to
`∀ i, ∃ j (_ : j ⟶ i), Epi (c.π.app j)`.
-/
theorem functor_initial (hc : IsLimit c) [∀ i, Epi (c.π.app i)] : Initial (functor c) :=
by
let e : I ≌ ULiftHom.{w} (ULift.{w} I) := ULiftHomULiftCategory.equiv _
suffices (e.inverse ⋙ functor c).Initial from initial_of_equivalence_comp e.inverse (functor c)
rw [initial_iff_of_isCofiltered (F := e.inverse ⋙ functor c)]
constructor
· intro ⟨_, X, (f : c.pt ⟶ _)⟩
obtain ⟨i, g, h⟩ := exists_hom c hc f
exact ⟨⟨i⟩, ⟨StructuredArrow.homMk g h.symm⟩⟩
· intro ⟨_, X, (f : c.pt ⟶ _)⟩ ⟨i⟩ ⟨_, (s : F.obj i ⟶ X), (w : f = c.π.app i ≫ _)⟩
⟨_, (s' : F.obj i ⟶ X), (w' : f = c.π.app i ≫ _)⟩
simp only [StructuredArrow.hom_eq_iff, StructuredArrow.comp_right]
refine ⟨⟨i⟩, 𝟙 _, ?_⟩
simp only [CategoryTheory.Functor.map_id]
rw [w] at w'
exact toProfinite.map_injective <| Epi.left_cancellation _ _ w'
