Commit 2023-08-23 08:35 23e7b3db

View on Github →

feat: Stonean is precoherent (#6725)

depends on: #5808
We give a characterisation of effective epimorphic families in Stonean and deduce that Stonean is a precoherent category. This work was done during the 2023 Copenhagen masterclass on formalisation of condensed mathematics. Numerous participants contributed.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Category/Stonean/EffectiveEpi.lean

added theorem CategoryTheory.EffectiveEpiFamily.toCompHaus

added theorem Stonean.EffectiveEpiFamily.lift_desc_condition

added def Stonean.EffectiveEpiFamily.struct

added theorem Stonean.effectiveEpiFamily_of_jointly_surjective

added theorem Stonean.effectiveEpiFamily_tfae

added theorem Stonean.epi_iff_surjective

added def Stonean.two

Modified Mathlib/Topology/Category/Stonean/Limits.lean

added def Stonean.coproductIsoCoproduct

added def Stonean.finiteCoproduct.explicitCocone

added def Stonean.finiteCoproduct.isColimit'