Commit 2024-08-01 04:29 c96401c7

View on Github →

refactor(Topology/Category): use CompHausLike API for limits in Profinite and Stonean (#15363)

Estimated changes

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

deleted theorem Profinite.Sigma.ι_comp_toFiniteCoproduct

deleted def Profinite.coproductHomeoCoproduct

deleted def Profinite.coproductIsoCoproduct

deleted def Profinite.finiteCoproduct.desc

deleted theorem Profinite.finiteCoproduct.hom_ext

deleted def Profinite.finiteCoproduct.isColimit

deleted def Profinite.finiteCoproduct.ι

deleted theorem Profinite.finiteCoproduct.ι_desc

deleted theorem Profinite.finiteCoproduct.ι_desc_apply

deleted theorem Profinite.finiteCoproduct.ι_injective

deleted theorem Profinite.finiteCoproduct.ι_jointly_surjective

deleted def Profinite.finiteCoproduct

deleted theorem Profinite.pullback.condition

deleted def Profinite.pullback.cone

deleted def Profinite.pullback.fst

deleted theorem Profinite.pullback.hom_ext

deleted def Profinite.pullback.isLimit

deleted def Profinite.pullback.lift

deleted theorem Profinite.pullback.lift_fst

deleted theorem Profinite.pullback.lift_snd

deleted def Profinite.pullback.snd

deleted def Profinite.pullback

deleted def Profinite.pullbackHomeoPullback

deleted def Profinite.pullbackIsoPullback

deleted theorem Profinite.pullback_fst_eq

deleted theorem Profinite.pullback_snd_eq

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

deleted theorem Stonean.HasPullbackOpenEmbedding

deleted theorem Stonean.Sigma.openEmbedding_ι

deleted def Stonean.coproductIsoCoproduct

deleted def Stonean.createsPullbacksOfOpenEmbedding

added theorem Stonean.extremallyDisconnected_preimage

added theorem Stonean.extremallyDisconnected_pullback

deleted def Stonean.finiteCoproduct.desc

deleted theorem Stonean.finiteCoproduct.hom_ext

deleted def Stonean.finiteCoproduct.isColimit

deleted theorem Stonean.finiteCoproduct.openEmbedding_ι

deleted def Stonean.finiteCoproduct.ι

deleted theorem Stonean.finiteCoproduct.ι_desc

deleted def Stonean.finiteCoproduct

deleted theorem Stonean.pullback.condition

deleted def Stonean.pullback.cone

deleted def Stonean.pullback.fst

deleted theorem Stonean.pullback.hom_ext

deleted def Stonean.pullback.isLimit

deleted def Stonean.pullback.lift

deleted theorem Stonean.pullback.lift_fst

deleted theorem Stonean.pullback.lift_snd

deleted def Stonean.pullback.snd

deleted def Stonean.pullback

deleted def Stonean.pullbackIsoPullback