Commit 2023-07-29 10:38 61b9a4c7

View on Github →

feat: some API for explicit limits in CompHaus (#5762) Co-authored by:

Riccardo Brasca riccardo.brasca@gmail.com @riccardobrasca
Filippo A. E. Nuccio filippo.nuccio@univ-st-etienne.fr @faenuccio We add some more API for the compatibility of explicit and abstract limits in CompHaus This work was done during the 2023 Copenhagen masterclass on formalisation of condensed mathematics. Numerous participants contributed.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Category/CompHaus/Basic.lean

added def CompHaus.homeoOfIso

added def CompHaus.isoEquivHomeo

added def CompHaus.isoOfHomeo

Modified Mathlib/Topology/Category/CompHaus/EffectiveEpi.lean

Renamed Mathlib/Topology/Category/CompHaus/ExplicitLimits.lean to Mathlib/Topology/Category/CompHaus/Limits.lean

added theorem CompHaus.Sigma.ι_comp_toFiniteCoproduct

added def CompHaus.coproductHomeoCoproduct

added def CompHaus.coproductIsoCoproduct

added theorem CompHaus.finiteCoproduct.ι_desc_apply

added theorem CompHaus.finiteCoproduct.ι_injective

added theorem CompHaus.finiteCoproduct.ι_jointly_surjective

added def CompHaus.pullbackHomeoPullback

added def CompHaus.pullbackIsoPullback

added theorem CompHaus.pullback_fst_eq

added theorem CompHaus.pullback_snd_eq