Effective epimorphisms in LightProfinite

This file proves that EffectiveEpi, Epi and Surjective are all equivalent in LightProfinite. As a consequence we prove that LightProfinite is Preregular. It follows from the constructions in LightProfinite/Limits.lean that LightProfinite is FinitaryExtensive. Together this implies that it is Precoherent.

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

Implementation: if π is a surjective morphism in LightProfinite, then it is an effective epi. The theorem LightProfinite.effectiveEpi_iff_surjective should be used instead.

Equations

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

theorem LightProfinite.effectiveEpi_iff_surjective {X : LightProfinite} {Y : LightProfinite} (f : X ⟶ Y) : CategoryTheory.EffectiveEpi f ↔ Function.Surjective ⇑f

instance LightProfinite.instPreregular : CategoryTheory.Preregular LightProfinite

Equations

• LightProfinite.instPreregular = ⋯

instance LightProfinite.instPrecoherent : CategoryTheory.Precoherent LightProfinite

Equations

• LightProfinite.instPrecoherent = ⋯