instReflectsEffectiveEpisStoneanProfiniteToProfinite

English

The Stonean to Profinite functor reflects effective epimorphisms: if its image is an effective epi, then the original morphism is an effective epi.

Русский

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

LaTeX

$$$$\forall f\, (\text{EffectiveEpi}(\mathrm{StoneanToProfinite}(f)) \Rightarrow \text{EffectiveEpi}(f)).$$$$

Lean4

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

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