-
Notifications
You must be signed in to change notification settings - Fork 331
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
chore(CategoryTheory/Sites): make Subcanonical
a class
#18186
base: master
Are you sure you want to change the base?
Conversation
dagurtomas
commented
Oct 24, 2024
Subcanonical
a class
PR summary d039e26c85Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
!bench |
Here are the benchmark results for commit 4693fc8. Benchmark Metric Change
=====================================================
- build .olean serialization 11.2%
- build import 11.6%
- build initialization 9.6%
- open Mathlib task-clock 18.1% (78.4 σ) |
Subcanonical.le_canonical | ||
|
||
instance : (canonicalTopology C).Subcanonical where | ||
le_canonical := le_rfl | ||
|
||
namespace Subcanonical | ||
|
||
/-- If every functor `yoneda.obj X` is a `J`-sheaf, then `J` is subcanonical. -/ | ||
theorem of_yoneda_isSheaf (J : GrothendieckTopology C) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This lemma could be renamed yoneda_obj_isSheaf
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I renamed it to of_isSheaf_yoneda_obj
, which seems to be the most correct
I am completely confused about what this means! |
So am I... I'll try again |
!bench |
Here are the benchmark results for commit ac94109. Benchmark Metric Change
=====================================================
- build .olean serialization 11.2%
- build import 11.3%
- build initialization 9.3%
- open Mathlib task-clock 16.3% (11.5 σ)
- open Mathlib wall-clock 14.6% (10.6 σ) |
!bench |
Here are the benchmark results for commit d039e26. |
Ok, merging master got rid of these weird benchmark results. |