Commit 2024-07-24 09:58 babbbb7c

View on Github →

feat(CategoryTheory/Site): Locally fully-faithful functors into sites. (#15062)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Limits/Presheaf.lean

Created Mathlib/CategoryTheory/Sites/LocallyFullyFaithful.lean

added theorem CategoryTheory.Functor.IsLocallyFaithful.ext

added theorem CategoryTheory.Functor.IsLocallyFull.ext

added theorem CategoryTheory.Functor.functorPushforward_equalizer_mem

added theorem CategoryTheory.Functor.functorPushforward_imageSieve_mem

added def CategoryTheory.Functor.imageSieve

added theorem CategoryTheory.Functor.imageSieve_eq_imageSieve

added theorem CategoryTheory.Functor.imageSieve_map

added def CategoryTheory.Sieve.equalizer

added theorem CategoryTheory.Sieve.equalizer_eq_equalizerSieve

added theorem CategoryTheory.Sieve.equalizer_self

Modified Mathlib/CategoryTheory/Yoneda.lean

modified def CategoryTheory.yonedaMap

Modified docs/references.bib