Commit 2024-07-25 20:13 9a79e43a

View on Github →

refactor(CategoryTheory/Sites): Allow non-fully-faithful dense subsites. (#15056)

Estimated changes

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

Modified Mathlib/CategoryTheory/Sites/DenseSubsite.lean

added theorem CategoryTheory.Functor.IsCoverDense.Types.naturality

added theorem CategoryTheory.Functor.IsCoverDense.Types.naturality_apply

modified theorem CategoryTheory.Functor.IsCoverDense.compatiblePreserving

modified theorem CategoryTheory.Functor.IsCoverDense.functorPullback_pushforward_covering

modified theorem CategoryTheory.Functor.IsCoverDense.isContinuous

added theorem CategoryTheory.Functor.IsDenseSubsite.coverPreserving

added theorem CategoryTheory.Functor.IsDenseSubsite.equalizer_mem

added theorem CategoryTheory.Functor.IsDenseSubsite.imageSieve_mem

added theorem CategoryTheory.Functor.IsDenseSubsite.isCoverDense

added theorem CategoryTheory.Functor.IsDenseSubsite.isIso_ranCounit_app_of_isDenseSubsite

added theorem CategoryTheory.Functor.IsDenseSubsite.isLocallyFaithful

added theorem CategoryTheory.Functor.IsDenseSubsite.isLocallyFull

Modified Mathlib/CategoryTheory/Sites/Discrete.lean

Modified Mathlib/CategoryTheory/Sites/Equivalence.lean

modified theorem CategoryTheory.Equivalence.coverPreserving

modified theorem CategoryTheory.Equivalence.eq_inducedTopology_of_transports

deleted theorem CategoryTheory.Equivalence.locallyCoverDense

Modified Mathlib/CategoryTheory/Sites/InducedTopology.lean

added def CategoryTheory.Functor.inducedTopology

added theorem CategoryTheory.Functor.inducedTopology_coverPreserving

deleted theorem CategoryTheory.Functor.locallyCoverDense_of_isCoverDense

added theorem CategoryTheory.Functor.pushforward_cover_iff_cover_pullback

deleted def CategoryTheory.LocallyCoverDense.inducedTopology

deleted theorem CategoryTheory.LocallyCoverDense.inducedTopology_coverPreserving

deleted theorem CategoryTheory.LocallyCoverDense.inducedTopology_isCocontinuous

deleted theorem CategoryTheory.LocallyCoverDense.pushforward_cover_iff_cover_pullback

deleted def CategoryTheory.LocallyCoverDense

deleted theorem CategoryTheory.over_forget_locallyCoverDense