Commit 2023-06-05 13:56 33b0b066

View on Github →

feat: port CategoryTheory.Sites.Canonical (#3936)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Sites/Canonical.lean

added theorem CategoryTheory.Sheaf.Subcanonical.isSheaf_of_representable

added theorem CategoryTheory.Sheaf.Subcanonical.of_yoneda_isSheaf

added def CategoryTheory.Sheaf.Subcanonical

added def CategoryTheory.Sheaf.canonicalTopology

added def CategoryTheory.Sheaf.finestTopology

added def CategoryTheory.Sheaf.finestTopologySingle

added theorem CategoryTheory.Sheaf.isSheafFor_bind

added theorem CategoryTheory.Sheaf.isSheafFor_trans

added theorem CategoryTheory.Sheaf.isSheaf_of_representable

added theorem CategoryTheory.Sheaf.isSheaf_yoneda_obj

added theorem CategoryTheory.Sheaf.le_finestTopology

added theorem CategoryTheory.Sheaf.sheaf_for_finestTopology

Modified Mathlib/CategoryTheory/Sites/Sieves.lean