Commit 2024-08-25 09:29 55eed64a

View on Github →

chore(CategoryTheory/Sites): address a bunch of porting notes (#16092)

Estimated changes

Modified Mathlib/CategoryTheory/Sites/Canonical.lean

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

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

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

Modified Mathlib/CategoryTheory/Sites/CompatibleSheafification.lean

Modified Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean

deleted def CategoryTheory.GrothendieckTopology.sheafificationIsoPresheafToSheafCompSheafToPreasheaf

Modified Mathlib/CategoryTheory/Sites/CoverLifting.lean

Modified Mathlib/CategoryTheory/Sites/Coverage.lean

Modified Mathlib/CategoryTheory/Sites/DenseSubsite.lean

Modified Mathlib/CategoryTheory/Sites/Equivalence.lean

Modified Mathlib/CategoryTheory/Sites/Grothendieck.lean

modified theorem CategoryTheory.GrothendieckTopology.Cover.condition

deleted def CategoryTheory.GrothendieckTopology.Cover.sieve

modified theorem CategoryTheory.GrothendieckTopology.ext

added theorem CategoryTheory.GrothendieckTopology.mem_sieves_iff_coe

Modified Mathlib/CategoryTheory/Sites/InducedTopology.lean

Modified Mathlib/CategoryTheory/Sites/LeftExact.lean

Modified Mathlib/CategoryTheory/Sites/Pullback.lean

Modified Mathlib/CategoryTheory/Sites/Subsheaf.lean

Modified Mathlib/CategoryTheory/Sites/Types.lean