Commit 2023-06-02 11:07 a17426c3

View on Github →

feat: Condensed objects (#4527)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Condensed/Basic.lean

added def Condensed

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

added def CompHaus.EffectiveEpiFamily.QB

added def CompHaus.EffectiveEpiFamily.relation

added def CompHaus.EffectiveEpiFamily.struct

added def CompHaus.EffectiveEpiFamily.structAux

added def CompHaus.EffectiveEpiFamily.ι

added def CompHaus.EffectiveEpiFamily.ιFun

added theorem CompHaus.EffectiveEpiFamily.ιFun_continuous

added theorem CompHaus.EffectiveEpiFamily.ιFun_injective

added def CompHaus.EffectiveEpiFamily.ιHom

added def CompHaus.EffectiveEpiFamily.π'

added theorem CompHaus.EffectiveEpiFamily.π'_comp_ι_hom

added theorem CompHaus.EffectiveEpiFamily.π_comp_ι_inv

added theorem CompHaus.effectiveEpiFamily_of_jointly_surjective

added theorem CompHaus.effectiveEpiFamily_tfae

Created Mathlib/Topology/Category/CompHaus/ExplicitLimits.lean

added def CompHaus.finiteCoproduct.cocone

added def CompHaus.finiteCoproduct.desc

added theorem CompHaus.finiteCoproduct.hom_ext

added def CompHaus.finiteCoproduct.isColimit

added def CompHaus.finiteCoproduct.ι

added theorem CompHaus.finiteCoproduct.ι_desc

added def CompHaus.finiteCoproduct

added theorem CompHaus.pullback.condition

added def CompHaus.pullback.cone

added def CompHaus.pullback.fst

added theorem CompHaus.pullback.hom_ext

added def CompHaus.pullback.isLimit

added def CompHaus.pullback.lift

added theorem CompHaus.pullback.lift_fst

added theorem CompHaus.pullback.lift_snd

added def CompHaus.pullback.snd

added def CompHaus.pullback

Modified docs/references.bib