instPreservesEpimorphismsLightCondSetForget

English

The forgetful functor from LightCondensed to LightCondSet preserves epimorphisms: if f is epi in LightCondensed, then forget(f) is epi in LightCondSet.

Русский

Функтор забывания из LightCondensed в LightCondSet сохраняет эпиморфизмы: если f является эпиморфизмом в LightCondensed, то forget(f) — эпиморфизм в LightCondSet.

LaTeX

$$$\forall f:\ X \to Y,\ \text{Epi}(f) \Rightarrow \text{Epi}(\text{forget}(f)).$$$

Lean4

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

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