[Merged by Bors] - refactor(Topology/Category): refactor Profinite.Basic#13909
[Merged by Bors] - refactor(Topology/Category): refactor Profinite.Basic#13909dagurtomas wants to merge 20 commits intomasterfrom
Conversation
PR summary 9308991747
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Topology.Category.Profinite.Basic | 1295 | 1293 | -2 (-0.15%) |
| Mathlib.Topology.Category.Profinite.Product | 1296 | 1294 | -2 (-0.15%) |
| Mathlib.Topology.Category.Profinite.AsLimit | 1299 | 1297 | -2 (-0.15%) |
| Mathlib.Topology.Category.Profinite.CofilteredLimit | 1305 | 1303 | -2 (-0.15%) |
| Mathlib.Topology.Category.LightProfinite.Basic | 1326 | 1324 | -2 (-0.15%) |
| Mathlib.Topology.Category.Profinite.Limits | 1338 | 1337 | -1 (-0.07%) |
Import changes for all files
| Files | Import difference |
|---|---|
7 filesMathlib.Topology.Category.Profinite.CofilteredLimit Mathlib.Topology.Category.Profinite.AsLimit Mathlib.Topology.Category.Profinite.Basic Mathlib.Topology.Category.Compactum Mathlib.Topology.Category.LightProfinite.Basic Mathlib.Topology.Category.LightProfinite.Sequence Mathlib.Topology.Category.Profinite.Product |
-2 |
Mathlib.Topology.Category.LightProfinite.Limits Mathlib.Topology.Category.Profinite.Limits |
-1 |
Declarations diff
+ FintypeCat.toProfiniteFullyFaithful
+ instance (X : Type*) [TopologicalSpace X]
+ instance : FintypeCat.toProfinite.Faithful := FintypeCat.toProfiniteFullyFaithful.faithful
+ instance : FintypeCat.toProfinite.Full := FintypeCat.toProfiniteFullyFaithful.full
- Profinite
- Profinite.toTopCat
- Profinite.to_compHausToTopCat
- category
- coe_comp
- coe_id
- concreteCategory
- forget_ContinuousMap_mk
- forget_reflectsIsomorphisms
- hasForget₂
- homeoOfIso
- instance : CoeSort Profinite Type*
- instance : FintypeCat.toProfinite.Faithful
- instance : FintypeCat.toProfinite.Full
- instance : Profinite.toTopCat.Faithful
- instance : Profinite.toTopCat.Full
- instance : profiniteToCompHaus.Faithful
- instance : profiniteToCompHaus.Full
- instance {X : Profinite} : CompactSpace ((forget Profinite).obj X) := by
- instance {X : Profinite} : T2Space ((forget Profinite).obj X) := by
- instance {X : Profinite} : TopologicalSpace ((forget Profinite).obj X) := by
- instance {X Y : Profinite} (f : X ⟶ Y) [@Epi CompHaus _ _ _ f] : Epi f := by
- instance {X Y : Profinite} (f : X ⟶ Y) [Epi f] : @Epi CompHaus _ _ _ f := by
- isClosedMap
- isIso_of_bijective
- isoEquivHomeo
- isoOfBijective
- isoOfHomeo
- mono_iff_injective
- of
- profiniteToCompHaus
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>|
bors merge |
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)
|
Pull request successfully merged into master. Build succeeded: |
This is the second part of the refactor of CompHaus and friends (refactoring the definition of
Profinitein terms ofCompHausLike, see #12930 for the end result)