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.

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