Commit 2023-07-29 10:38 0df52a83

View on Github →

feat: explicit limits in Profinite (#5763) Co-authored by:

Riccardo Brasca riccardo.brasca@gmail.com @riccardobrasca
Filippo A. E. Nuccio filippo.nuccio@univ-st-etienne.fr @faenuccio Analogue of CompHaus/ExplicitLimits for Profinite. 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/Limits.lean

added theorem Profinite.Sigma.ι_comp_toFiniteCoproduct

added def Profinite.coproductHomeoCoproduct

added def Profinite.coproductIsoCoproduct

added def Profinite.finiteCoproduct.cocone

added def Profinite.finiteCoproduct.desc

added theorem Profinite.finiteCoproduct.hom_ext

added def Profinite.finiteCoproduct.isColimit

added def Profinite.finiteCoproduct.ι

added theorem Profinite.finiteCoproduct.ι_desc

added theorem Profinite.finiteCoproduct.ι_desc_apply

added theorem Profinite.finiteCoproduct.ι_injective

added theorem Profinite.finiteCoproduct.ι_jointly_surjective

added def Profinite.finiteCoproduct

added theorem Profinite.pullback.condition

added def Profinite.pullback.cone

added def Profinite.pullback.fst

added theorem Profinite.pullback.hom_ext

added def Profinite.pullback.isLimit

added def Profinite.pullback.lift

added theorem Profinite.pullback.lift_fst

added theorem Profinite.pullback.lift_snd

added def Profinite.pullback.snd

added def Profinite.pullback

added def Profinite.pullbackHomeoPullback

added def Profinite.pullbackIsoPullback

added theorem Profinite.pullback_fst_eq

added theorem Profinite.pullback_snd_eq