Commit 2023-05-15 06:06 31f0309e

View on Github →

feat: port CategoryTheory.Sites.DenseSubsite (#3985) Mostly straightforward. Had to fight with simp once and the typeclass inference system a couple of times.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Sites/DenseSubsite.lean

added theorem CategoryTheory.CoverDense.Types.appHom_restrict

added theorem CategoryTheory.CoverDense.Types.appHom_valid_glue

added theorem CategoryTheory.CoverDense.Types.pushforwardFamily_apply

added theorem CategoryTheory.CoverDense.Types.pushforwardFamily_compatible

added theorem CategoryTheory.CoverDense.Types.pushforwardFamily_def

added theorem CategoryTheory.CoverDense.compatiblePreserving

added theorem CategoryTheory.CoverDense.ext

added theorem CategoryTheory.CoverDense.functorPullback_pushforward_covering

added def CategoryTheory.CoverDense.homOver

added def CategoryTheory.CoverDense.isoOver

added theorem CategoryTheory.CoverDense.iso_of_restrict_iso

added theorem CategoryTheory.CoverDense.sheafHom_eq

added theorem CategoryTheory.CoverDense.sheafHom_restrict_eq

added theorem CategoryTheory.CoverDense.sheaf_eq_amalgamation

added structure CategoryTheory.CoverDense

added structure CategoryTheory.Presieve.CoverByImageStructure

added def CategoryTheory.Presieve.coverByImage

added theorem CategoryTheory.Presieve.in_coverByImage

added def CategoryTheory.Sieve.coverByImage