Commit 2024-05-07 21:46 4c7c71d3

View on Github →

feat(LightProfinite): (co)limits (#9513) This PR constructs pullbacks and finite coproducts in LightProfinite.

Estimated changes

Modified Mathlib.lean

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

deleted def CompHaus.finiteCoproduct.cocone

modified def CompHaus.finiteCoproduct.isColimit

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

added def LightProfinite.toTopCat

Created Mathlib/Topology/Category/LightProfinite/Limits.lean

added def LightProfinite.finiteCoproduct.desc

added theorem LightProfinite.finiteCoproduct.hom_ext

added def LightProfinite.finiteCoproduct.isColimit

added def LightProfinite.finiteCoproduct.ι

added theorem LightProfinite.finiteCoproduct.ι_desc

added def LightProfinite.finiteCoproduct

added def LightProfinite.isTerminalPUnit

added theorem LightProfinite.pullback.condition

added def LightProfinite.pullback.fst

added theorem LightProfinite.pullback.hom_ext

added def LightProfinite.pullback.isLimit

added def LightProfinite.pullback.lift

added theorem LightProfinite.pullback.lift_fst

added theorem LightProfinite.pullback.lift_snd

added def LightProfinite.pullback.snd

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

deleted def Profinite.finiteCoproduct.cocone

modified def Profinite.finiteCoproduct.desc

modified theorem Profinite.finiteCoproduct.hom_ext

modified def Profinite.finiteCoproduct.isColimit

modified theorem Profinite.finiteCoproduct.ι_desc

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

deleted def Stonean.finiteCoproduct.cocone

deleted def Stonean.finiteCoproduct.explicitCocone

deleted def Stonean.finiteCoproduct.isColimit'

modified def Stonean.finiteCoproduct.isColimit