instReflectsEpimorphismsLightCondSetForget

English

The forgetful functor from LightCondensed to LightCondSet reflects epimorphisms: if the underlying morphism is epi, then the original morphism is epi.

Русский

Функтор забывания из LightCondensed в LightCondSet отражает эпиморфизмы: если подлежащий морфизм является эпиморфизмом, то исходный морфизм также является эпиморфизмом.

LaTeX

$$$\text{Forget}(f)\ \text{epi} \Rightarrow f \ \text{epi}.$$$

Lean4

instance : (LightCondensed.forget R).ReflectsEpimorphisms where
  reflects f
    hf := by
    rw [← Sheaf.isLocallySurjective_iff_epi'] at hf ⊢
    exact (Presheaf.isLocallySurjective_iff_whisker_forget _ f.val).mpr hf

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