[Merged by Bors] - refactor(topology/discrete_quotient): review API #18401
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
urkud
added
awaiting-review
urkud
commented
Feb 8, 2023
eric-wieser
reviewed
Feb 8, 2023
Comment on lines
77
to
+84
| def of_clopen {A : set X} (h : is_clopen A) : discrete_quotient X := | ||
| { rel := λ x y, x ∈ A ∧ y ∈ A ∨ x ∉ A ∧ y ∉ A, | ||
| equiv := ⟨by tauto!, by tauto!, by tauto!⟩, | ||
| clopen := begin | ||
| intros x, | ||
| by_cases hx : x ∈ A, | ||
| { apply is_clopen.union, | ||
| { convert h, | ||
| ext, | ||
| exact ⟨λ i, i.2, λ i, ⟨hx,i⟩⟩ }, | ||
| { convert is_clopen_empty, | ||
| tidy } }, | ||
| { apply is_clopen.union, | ||
| { convert is_clopen_empty, | ||
| tidy }, | ||
| { convert is_clopen.compl h, | ||
| ext, | ||
| exact ⟨λ i, i.2, λ i, ⟨hx, i⟩⟩ } }, | ||
| end } | ||
|
|
||
| lemma refl : ∀ x : X, S.rel x x := S.equiv.1 | ||
| lemma symm : ∀ x y : X, S.rel x y → S.rel y x := S.equiv.2.1 | ||
| lemma trans : ∀ x y z : X, S.rel x y → S.rel y z → S.rel x z := S.equiv.2.2 | ||
| { to_setoid := ⟨λ x y, x ∈ A ↔ y ∈ A, λ _, iff.rfl, λ _ _, iff.symm, λ _ _ _, iff.trans⟩, | ||
| is_open_set_of_rel := λ x, | ||
| by by_cases hx : x ∈ A; simp [setoid.rel, hx, h.1, h.2, ← compl_set_of] } | ||
|
|
||
| lemma refl : ∀ x, S.rel x x := S.refl' | ||
| lemma symm {x y : X} : S.rel x y → S.rel y x := S.symm' | ||
| lemma trans {x y z} : S.rel x y → S.rel y z → S.rel x z := S.trans' |
eric-wieser
approved these changes
Feb 8, 2023
| @@ -40,7 +40,7 @@ variables (X : Profinite.{u}) | |||
|
|
|||
| /-- The functor `discrete_quotient X ⥤ Fintype` whose limit is isomorphic to `X`. -/ | |||
| def fintype_diagram : discrete_quotient X ⥤ Fintype := | |||
| { obj := λ S, Fintype.of S, | |||
| { obj := λ S, by haveI := fintype.of_finite S; exact Fintype.of S, | |||
There was a problem hiding this comment.
What's the effect of this change?
There was a problem hiding this comment.
I changed an instance from noncomputable .. fintype to finite elsewhere, so I have to use fintype.of_finite here.
|
🚀 Pull request has been placed on the maintainer queue by eric-wieser. |
1 similar comment
|
🚀 Pull request has been placed on the maintainer queue by eric-wieser. |
|
Thanks! bors merge |
github-actions
bot
added
ready-to-merge
eric-wieser
reviewed
Feb 8, 2023
| @@ -26,22 +26,31 @@ quotients as setoids whose equivalence classes are clopen. | |||
| endowed with a `fintype` instance. | |||
There was a problem hiding this comment.
Should this say finite?
Suggested change
| endowed with a `fintype` instance. | |
| endowed with a `finite` instance. |
bors bot
pushed a commit
that referenced
this pull request
Feb 8, 2023
Backport various changes I made to the API while porting to Lean 4 in leanprover-community/mathlib4#2157. * extend `setoid X`; * require only that the fibers are open in the definition, prove that they are clopen; * golf proofs, reuse lattice structure on `setoid`s; * use bundled continuous maps for `comap`; * swap LHS and RHS in some `simp` lemmas; * generalize the `order_bot` instance from a discrete space to a locally connected space; * prove that a discrete topological space is locally connected.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Backport various changes I made to the API while porting to Lean 4 in leanprover-community/mathlib4#2157.
setoid X;setoids;comap;simplemmas;order_botinstance from a discrete space to a locally connected space;