chore(CategoryTheory/Sites): make Subcanonical a class

[dagurtomas]

---

[github-actions]

PR summary d039e26c85

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Sheaf.Subcanonical
+ Sheaf.Subcanonical.isSheaf_of_isRepresentable
+ Sheaf.Subcanonical.of_isSheaf_yoneda_obj
+ Sheaf.Subcanonical.yoneda
+ Sheaf.Subcanonical.yonedaCompSheafToPresheaf
+ Sheaf.Subcanonical.yonedaFullyFaithful
+ instance : (J.yoneda).Faithful := (J.yonedaFullyFaithful).faithful
+ instance : (J.yoneda).Full := (J.yonedaFullyFaithful).full
+ instance : (canonicalTopology C).Subcanonical
+ instance : compHausToCondensed.Faithful := inferInstanceAs (_ ⋙ _).Faithful
+ instance : compHausToCondensed.Full := inferInstanceAs (_ ⋙ _).Full
+ le_canonical
+ of_isSheaf_yoneda_obj
++-- subcanonical
- instance : compHausToCondensed.Faithful := show (_ ⋙ _).Faithful from inferInstance
- instance : compHausToCondensed.Full := show (_ ⋙ _).Full from inferInstance
- instance : hJ.yoneda.Faithful := hJ.yonedaFullyFaithful.faithful
- instance : hJ.yoneda.Full := hJ.yonedaFullyFaithful.full
- of_yoneda_isSheaf

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>

The doc-module for script/declarations_diff.sh contains some details about this script.

[dagurtomas]

!bench

[leanprover-bot]

Here are the benchmark results for commit 4693fc8.
There were significant changes against commit f7b57bc:

  Benchmark      Metric                 Change
  =====================================================
- build          .olean serialization    11.2%
- build          import                  11.6%
- build          initialization           9.6%
- open Mathlib   task-clock              18.1% (78.4 σ)

[joelriou]

This lemma could be renamed yoneda_obj_isSheaf.

[dagurtomas]

I renamed it to of_isSheaf_yoneda_obj, which seems to be the most correct

[joelriou]

Here are the benchmark results for commit 4693fc8. There were significant changes against commit f7b57bc:

  Benchmark      Metric                 Change
  =====================================================
- build          .olean serialization    11.2%
- build          import                  11.6%
- build          initialization           9.6%
- open Mathlib   task-clock              18.1% (78.4 σ)

I am completely confused about what this means!

[dagurtomas]

Here are the benchmark results for commit 4693fc8. There were significant changes against commit f7b57bc:

  Benchmark      Metric                 Change
  =====================================================
- build          .olean serialization    11.2%
- build          import                  11.6%
- build          initialization           9.6%
- open Mathlib   task-clock              18.1% (78.4 σ)

I am completely confused about what this means!

So am I... I'll try again

[dagurtomas]

!bench

[leanprover-bot]

Here are the benchmark results for commit ac94109.
There were significant changes against commit f7b57bc:

  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 σ)

[dagurtomas]

!bench

[leanprover-bot]

Here are the benchmark results for commit d039e26.
There were no significant changes against commit 7c7a48f.

[dagurtomas]

Ok, merging master got rid of these weird benchmark results.