Commit 2023-08-22 14:19 537e7f03

View on Github →

feat: Profinite is precoherent (#5858)

depends on: #5763 We give a characterisation of effective epimorphic families in Profinite and deduce that Profinite 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/Profinite/EffectiveEpi.lean

added def Profinite.EffectiveEpiFamily.QB'

added def Profinite.EffectiveEpiFamily.QB

added def Profinite.EffectiveEpiFamily.relation

added def Profinite.EffectiveEpiFamily.struct

added def Profinite.EffectiveEpiFamily.structAux

added def Profinite.EffectiveEpiFamily.ιFun

added theorem Profinite.EffectiveEpiFamily.ιFun_continuous

added theorem Profinite.EffectiveEpiFamily.ιFun_injective

added def Profinite.EffectiveEpiFamily.ιHom'

added def Profinite.EffectiveEpiFamily.ιHom

added def Profinite.EffectiveEpiFamily.ιIso'

added def Profinite.EffectiveEpiFamily.ιIso

added def Profinite.EffectiveEpiFamily.π'

added theorem Profinite.EffectiveEpiFamily.π'_comp_ι_hom

added theorem Profinite.EffectiveEpiFamily.π_comp_ι_inv

added theorem Profinite.effectiveEpiFamily_of_jointly_surjective

added theorem Profinite.effectiveEpiFamily_tfae