Commit 2024-10-31 18:38 9c053cf0

View on Github →

chore(CategoryTheory/Sites): make Subcanonical a class (#18186)

Estimated changes

Modified Mathlib/AlgebraicGeometry/Sites/BigZariski.lean

deleted theorem AlgebraicGeometry.Scheme.subcanonical_zariskiTopology

Modified Mathlib/CategoryTheory/Sites/Canonical.lean

added theorem CategoryTheory.GrothendieckTopology.Subcanonical.isSheaf_of_isRepresentable

added theorem CategoryTheory.GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj

added theorem CategoryTheory.GrothendieckTopology.le_canonical

added def CategoryTheory.GrothendieckTopology.yoneda

added def CategoryTheory.GrothendieckTopology.yonedaCompSheafToPresheaf

added def CategoryTheory.GrothendieckTopology.yonedaFullyFaithful

deleted theorem CategoryTheory.Sheaf.Subcanonical.isSheaf_of_isRepresentable

deleted theorem CategoryTheory.Sheaf.Subcanonical.of_yoneda_isSheaf

deleted def CategoryTheory.Sheaf.Subcanonical.yoneda

deleted def CategoryTheory.Sheaf.Subcanonical.yonedaCompSheafToPresheaf

deleted def CategoryTheory.Sheaf.Subcanonical.yonedaFullyFaithful

deleted def CategoryTheory.Sheaf.Subcanonical

Modified Mathlib/CategoryTheory/Sites/Coherent/CoherentSheaves.lean

deleted theorem CategoryTheory.coherentTopology.subcanonical

Modified Mathlib/CategoryTheory/Sites/Coherent/ExtensiveSheaves.lean

deleted theorem CategoryTheory.extensiveTopology.subcanonical

Modified Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean

deleted theorem CategoryTheory.regularTopology.subcanonical

Modified Mathlib/CategoryTheory/Sites/Types.lean

deleted theorem CategoryTheory.subcanonical_typesGrothendieckTopology

Modified Mathlib/Condensed/Functors.lean

Modified Mathlib/Condensed/Light/Functors.lean