English
In LightCondensed, for a coherent setting with a cone indexed by natural numbers, the initial projection π at index 0 is epi provided each component map is epi and the base limit is preserved by forgetful functors.
Русский
В LightCondensed, в когерентной конфигурации, индексируемой натуральными числами, начальная проекция π на индекс 0 является эпиморфизмом, если каждая компонентная карта является эпиморфизмом и базовый предел сохраняется забывающим функтором.
LaTeX
$$$\text{epi}(c.\pi_{0})$$$
Lean4
theorem epi_π_app_zero_of_epi : Epi (c.π.app ⟨0⟩) :=
by
apply Functor.epi_of_epi_map (forget R)
change Epi (((forget R).mapCone c).π.app ⟨0⟩)
apply coherentTopology.epi_π_app_zero_of_epi
· simp only [LightProfinite.effectiveEpi_iff_surjective]
exact fun x h ↦ Concrete.surjective_π_app_zero_of_surjective_map (limit.isLimit x) h
· have := (freeForgetAdjunction R).isRightAdjoint
exact isLimitOfPreserves _ hc
· exact fun _ ↦ (forget R).map_epi _
