[Merged by Bors] - feat(topology/category/Profinite): Profinite_to_Top creates limits. #7070

adamtopaz · 2021-04-06T21:56:27Z

This PR adds a proof that Profinite has limits by showing that the forgetful functor to Top creates limits.

semorrison · 2021-04-06T23:21:59Z

src/topology/category/Top/limits.lean

+Generally you should just use `limit.cone F`, unless you need the actual definition
+(which is in terms of `types.limit_cone`).
+This differs from `limit_cone` only in the definition of the topology itself,
+which is defined as a subspace topology as opposed to an infemum as in limit_cone.


Suggested change

which is defined as a subspace topology as opposed to an infemum as in limit_cone.

which is defined as a subspace topology as opposed to an infimum as in `limit_cone`.

semorrison · 2021-04-06T23:28:45Z

src/topology/category/Profinite.lean

+{ X :=
+  { to_Top := (Top.limit_cone' $ F ⋙ Profinite_to_Top).X,
+    is_compact := begin
+      erw ← compact_iff_compact_space,


If you don't like the erw then apply compact_iff_compact_space.mp, suffices here.

semorrison · 2021-04-06T23:29:16Z

src/topology/category/Profinite.lean

+      apply is_closed_Inter,
+      intros a,
+      apply is_closed_Inter,
+      intros b,
+      apply is_closed_Inter,
+      intros f,


Perhaps

Suggested change

apply is_closed_Inter,

intros a,

apply is_closed_Inter,

intros b,

apply is_closed_Inter,

intros f,

refine is_closed_Inter (λ a, is_closed_Inter (λ b, is_closed_Inter (λ f, _))),

b-mehta · 2021-04-06T23:31:22Z

Since we already have that the functor Profinite_to_CompHaus is reflective, and CompHaus_to_Top is reflective, they both create limits (and Profinite has limits from there), which would be a much shorter proof than this one.

semorrison · 2021-04-06T23:31:36Z

src/topology/category/Profinite.lean

+      refine is_closed.preimage (continuous.prod_mk (continuous_apply _) (continuous_apply _)) _,
+      refine is_closed_eq _ continuous_snd,
+      continuity,


Suggested change

refine is_closed.preimage (continuous.prod_mk (continuous_apply _) (continuous_apply _)) _,

refine is_closed_eq _ continuous_snd,

continuity,

exact is_closed.preimage (by continuity) (is_closed_eq (by continuity) continuous_snd),

It's interesting that by continuity can't solve continuous_snd here, even though continuous_snd has the attribute. I don't see what's going on. continuity! does work, however, so another possibility here is

refine is_closed.preimage _ (is_closed_eq _ _); continuity!

semorrison · 2021-04-06T23:38:04Z

src/topology/category/Profinite.lean

+    valid_lift := let I := limit_cone_to_Top F in I ≪≫ limits.is_limit.unique_up_to_iso
+      (Top.limit_cone'_is_limit _) hA } }


Suggested change

valid_lift := let I := limit_cone_to_Top F in I ≪≫ limits.is_limit.unique_up_to_iso

(Top.limit_cone'_is_limit _) hA } }

valid_lift := let I := limit_cone_to_Top F in

I ≪≫ limits.is_limit.unique_up_to_iso (Top.limit_cone'_is_limit _) hA } }

semorrison

LGTM

semorrison · 2021-04-06T23:38:25Z

src/topology/category/Profinite.lean

+      refine is_closed.preimage (continuous.prod_mk (continuous_apply _) (continuous_apply _)) _,
+      refine is_closed_eq _ continuous_snd,
+      continuity,


It's interesting that by continuity can't solve continuous_snd here, even though continuous_snd has the attribute. I don't see what's going on. continuity! does work, however, so another possibility here is

refine is_closed.preimage _ (is_closed_eq _ _); continuity!

semorrison · 2021-04-06T23:39:37Z

Don't mind whether or not you take the suggestions, they're all just minor stylistic points.

bors d+

bors · 2021-04-06T23:39:38Z

✌️ adamtopaz can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

b-mehta · 2021-04-06T23:56:56Z

@semorrison I don't think this is ready to merge yet, since this is virtually all work essentially already in mathlib - we're basically five lines from having the result that Profinite has limits from things already in mathlib master, like I mentioned in my comment earlier.

adamtopaz · 2021-04-07T00:14:12Z

@semorrison I don't think this is ready to merge yet, since this is virtually all work essentially already in mathlib - we're basically five lines from having the result that Profinite has limits from things already in mathlib master, like I mentioned in my comment earlier.

Good point! I'll try to make it work with the reflectors.

adamtopaz · 2021-04-07T00:52:02Z

Thanks @b-mehta ! That was much easier (modulo some small universe annoyances).

b-mehta

LGTM, modulo minor comment.

src/topology/category/Profinite.lean

b-mehta · 2021-04-07T16:41:48Z

Thanks!

bors merge

…7070) This PR adds a proof that `Profinite` has limits by showing that the forgetful functor to `Top` creates limits.

bors · 2021-04-07T22:32:13Z

Pull request successfully merged into master.

Build succeeded:

Add files

927d7b6

adamtopaz requested review from kbuzzard and b-mehta April 6, 2021 21:56

adamtopaz added the awaiting-review The author would like community review of the PR label Apr 6, 2021

semorrison reviewed Apr 6, 2021

View reviewed changes

semorrison approved these changes Apr 6, 2021

View reviewed changes

reflective

c21c314

b-mehta approved these changes Apr 7, 2021

View reviewed changes

src/topology/category/Profinite.lean Show resolved Hide resolved

Add instances

8638e1d

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Apr 7, 2021

bors bot pushed a commit that referenced this pull request Apr 7, 2021

feat(topology/category/Profinite): Profinite_to_Top creates limits. (#…

68bd325

…7070) This PR adds a proof that `Profinite` has limits by showing that the forgetful functor to `Top` creates limits.

bors bot changed the title ~~feat(topology/category/Profinite): Profinite_to_Top creates limits.~~ [Merged by Bors] - feat(topology/category/Profinite): Profinite_to_Top creates limits. Apr 7, 2021

bors bot closed this Apr 7, 2021

bors bot deleted the profinite_has_limits branch April 7, 2021 22:32

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(topology/category/Profinite): Profinite_to_Top creates limits. #7070

[Merged by Bors] - feat(topology/category/Profinite): Profinite_to_Top creates limits. #7070

adamtopaz commented Apr 6, 2021

semorrison Apr 6, 2021 •

edited

Loading

semorrison Apr 6, 2021

semorrison Apr 6, 2021

b-mehta commented Apr 6, 2021

semorrison Apr 6, 2021

semorrison Apr 6, 2021

semorrison Apr 6, 2021

semorrison left a comment

semorrison Apr 6, 2021

semorrison commented Apr 6, 2021

bors bot commented Apr 6, 2021

b-mehta commented Apr 6, 2021

adamtopaz commented Apr 7, 2021

adamtopaz commented Apr 7, 2021

b-mehta left a comment

b-mehta commented Apr 7, 2021

bors bot commented Apr 7, 2021

	which is defined as a subspace topology as opposed to an infemum as in limit_cone.
	which is defined as a subspace topology as opposed to an infimum as in `limit_cone`.

		valid_lift := let I := limit_cone_to_Top F in I ≪≫ limits.is_limit.unique_up_to_iso
		(Top.limit_cone'_is_limit _) hA } }

[Merged by Bors] - feat(topology/category/Profinite): Profinite_to_Top creates limits. #7070

[Merged by Bors] - feat(topology/category/Profinite): Profinite_to_Top creates limits. #7070

Conversation

adamtopaz commented Apr 6, 2021

semorrison Apr 6, 2021 • edited Loading

Choose a reason for hiding this comment

semorrison Apr 6, 2021

Choose a reason for hiding this comment

semorrison Apr 6, 2021

Choose a reason for hiding this comment

b-mehta commented Apr 6, 2021

semorrison Apr 6, 2021

Choose a reason for hiding this comment

semorrison Apr 6, 2021

Choose a reason for hiding this comment

semorrison Apr 6, 2021

Choose a reason for hiding this comment

semorrison left a comment

Choose a reason for hiding this comment

semorrison Apr 6, 2021

Choose a reason for hiding this comment

semorrison commented Apr 6, 2021

bors bot commented Apr 6, 2021

b-mehta commented Apr 6, 2021

adamtopaz commented Apr 7, 2021

adamtopaz commented Apr 7, 2021

b-mehta left a comment

Choose a reason for hiding this comment

b-mehta commented Apr 7, 2021

bors bot commented Apr 7, 2021

semorrison Apr 6, 2021 •

edited

Loading