[Merged by Bors] - feat(topology/sheaves/*): Notation for restriction of sections. #16088

erdOne · 2022-08-17T03:36:23Z

src/topology/sheaves/presheaf.lean

into restrict_notation

jcommelin · 2022-08-31T13:04:21Z

I think this is helpful. Although I understand @erdOne 's hesitation. @adamtopaz what do you think?

adamtopaz · 2022-08-31T13:17:50Z

To be honest, this notation looks quite awkward. And since it's not too similar (unless you really squint) to what we would write on paper, I'm not sure if it's worth adding this notation right now. Maybe Lean4 would let us introduce better notation? If so, perhaps we should just wait until the port to Lean4?

erdOne · 2022-08-31T13:35:42Z

There are two notations introduced.

x ∣_ₕ e for F.map e.op x
x ∣_ₗ V ⟪e⟫ for F.map (hom_of_le e).op x

Are you referring to both of them?
Although I agree that this is quite awkward, I think we would always need to provide the proof that V ≤ U nonetheless, and I'm not sure (due to the lack of knowledge regarding Lean4) if Lean4 could help the situation.

Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

jcommelin

bors d+

jcommelin · 2022-10-05T12:43:17Z

src/topology/sheaves/presheaf.lean

+infixl ` ∣_ₕ `: 80 := restrict
+
+notation x ` ∣_ₗ `: 80 U ` ⟪` e `⟫ ` := @restrict _ _ _ _ _ _ x U (@hom_of_le (opens _) _ U _ e)


Can you please put this notation in a locale?

bors · 2022-10-05T12:43:27Z

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

erdOne · 2022-10-07T04:02:38Z

bors merge

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

bors · 2022-10-07T06:16:02Z

Build failed (retrying...):

Lint mathlib

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

bors · 2022-10-07T11:25:12Z

Build failed (retrying...):

Run tests

YaelDillies · 2022-10-07T16:07:47Z

I think we would always need to provide the proof that V ≤ U nonetheless

Do you know you can already make the notation infer the proof? Something like

notation ` fin_mk ` k := fin.mk _ ‹k < n›

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

bors · 2022-10-08T00:38:02Z

Build failed (retrying...):

Run tests

erdOne · 2022-10-08T09:03:17Z

Ah I forgot about that. We will probably need a custom tactic instead but this is definitely worth a try.

erdOne · 2022-10-08T09:10:30Z

bors cancel
Let me experiment with that a bit.

bors · 2022-10-08T09:10:32Z

Canceled.

src/algebraic_geometry/Scheme.lean

into restrict_notation

jcommelin

Thanks 🎉

bors merge

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

bors · 2022-10-27T10:46:37Z

Pull request successfully merged into master.

Build succeeded:

first commit

2deb572

alreadydone reviewed Aug 17, 2022

View reviewed changes

src/topology/sheaves/presheaf.lean Outdated Show resolved Hide resolved

src/topology/sheaves/presheaf.lean Outdated Show resolved Hide resolved

erdOne and others added 3 commits August 18, 2022 04:24

Update presheaf.lean

cfbfe01

Merge branch 'master' of https://github.com/leanprover-community/mathlib

5e694ea

into restrict_notation

fix?

80a6ed9

erdOne added the awaiting-review The author would like community review of the PR label Aug 20, 2022

Update src/topology/sheaves/presheaf.lean

349164c

Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

jcommelin reviewed Oct 5, 2022

View reviewed changes

leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Oct 5, 2022

localize notation

aacc7c1

bors bot pushed a commit that referenced this pull request Oct 7, 2022

feat(topology/sheaves/*): Notation for restriction of sections. (#16088)

cd8cecc

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

bors bot pushed a commit that referenced this pull request Oct 7, 2022

feat(topology/sheaves/*): Notation for restriction of sections. (#16088)

f616517

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

bors bot pushed a commit that referenced this pull request Oct 8, 2022

feat(topology/sheaves/*): Notation for restriction of sections. (#16088)

6cc83d9

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

attempt

c192b05

YaelDillies reviewed Oct 9, 2022

View reviewed changes

src/algebraic_geometry/Scheme.lean Outdated Show resolved Hide resolved

erdOne added 2 commits October 10, 2022 08:34

Merge branch 'master' of https://github.com/leanprover-community/mathlib

2ff7b70

into restrict_notation

fix

233cb33

erdOne added awaiting-review The author would like community review of the PR t-algebraic-geometry Algebraic geometry and removed delegated The PR author may merge after reviewing final suggestions. labels Oct 10, 2022

Merge branch 'master' of https://github.com/leanprover-community/mathlib

6f9a11f

into restrict_notation

erdOne requested a review from a team as a code owner October 26, 2022 21:39

jcommelin approved these changes Oct 27, 2022

View reviewed changes

leanprover-community-bot-assistant 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 Oct 27, 2022

bors bot pushed a commit that referenced this pull request Oct 27, 2022

feat(topology/sheaves/*): Notation for restriction of sections. (#16088)

06c75af

Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

bors bot changed the title ~~feat(topology/sheaves/*): Notation for restriction of sections.~~ [Merged by Bors] - feat(topology/sheaves/*): Notation for restriction of sections. Oct 27, 2022

bors bot closed this Oct 27, 2022

bors bot deleted the restrict_notation branch October 27, 2022 10:46

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(topology/sheaves/*): Notation for restriction of sections. #16088

[Merged by Bors] - feat(topology/sheaves/*): Notation for restriction of sections. #16088

erdOne commented Aug 17, 2022

jcommelin commented Aug 31, 2022

adamtopaz commented Aug 31, 2022

erdOne commented Aug 31, 2022 •

edited

Loading

jcommelin left a comment

jcommelin Oct 5, 2022

bors bot commented Oct 5, 2022

erdOne commented Oct 7, 2022

bors bot commented Oct 7, 2022

bors bot commented Oct 7, 2022

YaelDillies commented Oct 7, 2022 •

edited

Loading

bors bot commented Oct 8, 2022

erdOne commented Oct 8, 2022

erdOne commented Oct 8, 2022

bors bot commented Oct 8, 2022

jcommelin left a comment

bors bot commented Oct 27, 2022

		infixl ` ∣_ₕ `: 80 := restrict

		notation x ` ∣_ₗ `: 80 U ` ⟪` e `⟫ ` := @restrict _ _ _ _ _ _ x U (@hom_of_le (opens _) _ U _ e)

[Merged by Bors] - feat(topology/sheaves/*): Notation for restriction of sections. #16088

[Merged by Bors] - feat(topology/sheaves/*): Notation for restriction of sections. #16088

Conversation

erdOne commented Aug 17, 2022

jcommelin commented Aug 31, 2022

adamtopaz commented Aug 31, 2022

erdOne commented Aug 31, 2022 • edited Loading

jcommelin left a comment

Choose a reason for hiding this comment

jcommelin Oct 5, 2022

Choose a reason for hiding this comment

bors bot commented Oct 5, 2022

erdOne commented Oct 7, 2022

bors bot commented Oct 7, 2022

bors bot commented Oct 7, 2022

YaelDillies commented Oct 7, 2022 • edited Loading

bors bot commented Oct 8, 2022

erdOne commented Oct 8, 2022

erdOne commented Oct 8, 2022

bors bot commented Oct 8, 2022

jcommelin left a comment

Choose a reason for hiding this comment

bors bot commented Oct 27, 2022

erdOne commented Aug 31, 2022 •

edited

Loading

YaelDillies commented Oct 7, 2022 •

edited

Loading