profiniteToCompHausEffectivePresentation

English

The functor profiniteToCompHaus is effectively enough, i.e., it provides effective presentations compatible with Profinite.

Русский

Функтор profiniteToCompHaus обладают свойством effectively enough: он обеспечивает эффективные представления, согласованные с Profinite.

LaTeX

$$$\\mathrm{instEffectivelyEnough}\\;\\text{(Profinite\\toCompHaus)}$$$

Lean4

/-- An effective presentation of an `X : Profinite` with respect to the inclusion functor from `Stonean`
-/
noncomputable def profiniteToCompHausEffectivePresentation (X : CompHaus) : profiniteToCompHaus.EffectivePresentation X
    where
  p := Stonean.toProfinite.obj X.presentation
  f := CompHaus.presentation.π X
  effectiveEpi := ((CompHaus.effectiveEpi_tfae _).out 0 1).mpr (inferInstance : Epi _)

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