Effective epimorphisms and finite effective epimorphic families in Profinite

This file proves that Profinite is Preregular. Together with the fact that it is FinitaryPreExtensive, this implies that Profinite is Precoherent.

To do this, we need to characterise effective epimorphisms in Profinite. As a consequence, we also get a characterisation of finite effective epimorphic families.

Main results

• Profinite.effectiveEpi_tfae: For a morphism in Profinite, the conditions surjective, epimorphic, and effective epimorphic are all equivalent.

• Profinite.effectiveEpiFamily_tfae: For a finite family of morphisms in Profinite with fixed target in Profinite, the conditions jointly surjective, jointly epimorphic and effective epimorphic are all equivalent.

As a consequence, we obtain instances that Profinite is precoherent and preregular.

noncomputable def Profinite.struct {B : Profinite} {X : Profinite} (π : X ⟶ B) (hπ : Function.Surjective ⇑π) : CategoryTheory.EffectiveEpiStruct π

Implementation: If π is a surjective morphism in Profinite, then it is an effective epi. The theorem Profinite.effectiveEpi_tfae should be used instead.

Equations

• One or more equations did not get rendered due to their size.

theorem Profinite.effectiveEpi_tfae {B : Profinite} {X : Profinite} (π : X ⟶ B) : [CategoryTheory.EffectiveEpi π, CategoryTheory.Epi π, Function.Surjective ⇑π].TFAE

instance Profinite.instPreservesEffectiveEpisCompHausProfiniteToCompHaus : profiniteToCompHaus.PreservesEffectiveEpis

Equations

• Profinite.instPreservesEffectiveEpisCompHausProfiniteToCompHaus = ⋯

instance Profinite.instReflectsEffectiveEpisCompHausProfiniteToCompHaus : profiniteToCompHaus.ReflectsEffectiveEpis

Equations

• Profinite.instReflectsEffectiveEpisCompHausProfiniteToCompHaus = ⋯

noncomputable def Profinite.profiniteToCompHausEffectivePresentation (X : CompHaus) : profiniteToCompHaus.EffectivePresentation X

An effective presentation of an X : Profinite with respect to the inclusion functor from Stonean

Equations

• Profinite.profiniteToCompHausEffectivePresentation X = { p := Stonean.toProfinite.obj X.presentation, f := CompHaus.presentation.π X, effectiveEpi := ⋯ }

instance Profinite.instEffectivelyEnoughCompHausProfiniteToCompHaus : profiniteToCompHaus.EffectivelyEnough

Equations

• Profinite.instEffectivelyEnoughCompHausProfiniteToCompHaus = ⋯

instance Profinite.instPreregular : CategoryTheory.Preregular Profinite

Equations

• Profinite.instPreregular = ⋯

theorem Profinite.effectiveEpiFamily_tfae {α : Type} [Finite α] {B : Profinite} (X : α → Profinite) (π : (a : α) → X a ⟶ B) : [CategoryTheory.EffectiveEpiFamily X π, CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc π), ∀ (b : ↑B.toTop), ∃ (a : α) (x : ↑(X a).toTop), (π a) x = b].TFAE

theorem Profinite.effectiveEpiFamily_of_jointly_surjective {α : Type} [Finite α] {B : Profinite} (X : α → Profinite) (π : (a : α) → X a ⟶ B) (surj : ∀ (b : ↑B.toTop), ∃ (a : α) (x : ↑(X a).toTop), (π a) x = b) : CategoryTheory.EffectiveEpiFamily X π