instPreservesEffectiveEpisStoneanProfiniteToProfinite

English

The functor from Stonean to Profinite preserves effective epimorphisms: effective epis are preserved under the Stonean-to-Profinite translation.

Русский

Функтор Stonean → Profinite сохраняет эффективные эпиморфизмы: эффективные эпиморфизмы сохраняются при переводе Stonean в Profinite.

LaTeX

$$$$\text{StoneanToProfinite} \ \text{preserves effective epis}.$$$$

Lean4

instance : Stonean.toProfinite.PreservesEffectiveEpis where
  preserves f h := ((Profinite.effectiveEpi_tfae _).out 0 2).mpr (((Stonean.effectiveEpi_tfae _).out 0 2).mp h)

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