Effective epimorphisms in Profinite

This file proves that EffectiveEpi, Epi and Surjective are all equivalent in Profinite. As a consequence we deduce from the material in Mathlib.Topology.Category.CompHausLike.EffectiveEpi that Profinite is Preregular and Precoherent.

We also prove that for a finite family of morphisms in Profinite with fixed target, the conditions jointly surjective, jointly epimorphic and effective epimorphic are all equivalent.

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 π