instReflectsEffectiveEpisCompHausProfiniteToCompHaus

English

The profiniteToCompHaus functor reflects effective epimorphisms: if the image is effective epi in CompHaus, the original is effective epi in Profinite.

Русский

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

LaTeX

$$$\\mathrm{instReflectsEffectiveEpis}\\;:\\; \\mathrm{Profinite} \\to \\mathrm{CompHaus}$$$

Lean4

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

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