Documentation

Mathlib.Topology.Category.LightProfinite.EffectiveEpi

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 Mathlib/Topology/Category/LightProfinite/Limits.lean that LightProfinite is FinitaryExtensive. Together this implies that it is Precoherent.

source
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.
Instances For
    source
    theorem LightProfinite.effectiveEpi_iff_surjective {X : LightProfinite} {Y : LightProfinite} (f : X ⟶ Y) :
    CategoryTheory.EffectiveEpi f ↔ Function.Surjective ⇑f
    source
    instance LightProfinite.instPreregular :
    CategoryTheory.Preregular LightProfinite
    Equations
    source
    instance LightProfinite.instPrecoherent :
    CategoryTheory.Precoherent LightProfinite
    Equations