Commit 2024-07-17 17:39 eed648ae

View on Github →

refactor(Topology/Category): refactor Profinite.Basic (#13909) This is the second part of the refactor of CompHaus and friends (refactoring the definition of Profinite in terms of CompHausLike, see #12930 for the end result)

Estimated changes

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

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

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

added def FintypeCat.toProfiniteFullyFaithful

deleted theorem Profinite.coe_comp

deleted theorem Profinite.coe_id

deleted theorem Profinite.forget_ContinuousMap_mk

deleted def Profinite.homeoOfIso

deleted theorem Profinite.isClosedMap

deleted theorem Profinite.isIso_of_bijective

deleted def Profinite.isoEquivHomeo

deleted def Profinite.isoOfHomeo

deleted theorem Profinite.mono_iff_injective

deleted def Profinite.of

deleted def Profinite.toTopCat

deleted theorem Profinite.to_compHausToTopCat

deleted structure Profinite

deleted def profiniteToCompHaus

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

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

modified def Profinite.pullbackHomeoPullback

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

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

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