instPreservesEpimorphismsProfiniteLightToProfinite

English

The induced functor lightToProfinite preserves epis; i.e., epi in LightProfinite maps to epi in Profinite under the forgetful functor.

Русский

Индуцируемый функтор сохраняет эпиморфизмы; эпиморфизм в LightProfinite переходит в эпиморфизм в Profinite через забывающий функтор.

LaTeX

$$$\text{PreservesEpimorphisms} (\text{forget LightProfinite})$$$

Lean4

instance : lightToProfinite.PreservesEpimorphisms where
  preserves f _ := (Profinite.epi_iff_surjective _).mpr ((epi_iff_surjective f).mp inferInstance)

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