Commit 2024-05-28 19:29 de3c257c

View on Github →

feat: morphisms of presheaves that are locally injective for a Grothendieck topology (#11719) This PR creates the file CategoryTheory.Sites.LocallyInjective which develops the basic API of locally injective morphisms of presheaves. The file CategoryTheory.Sites.Surjective is renamed CategoryTheory.Sites.LocallySurjective and shall be expanded in a future PR.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/ConcreteCategory/Basic.lean

added theorem CategoryTheory.NatTrans.naturality_apply

Modified Mathlib/CategoryTheory/Sites/LeftExact.lean

added theorem CategoryTheory.toSheafify_plusPlusIsoSheafify_hom

Created Mathlib/CategoryTheory/Sites/LocallyInjective.lean

added def CategoryTheory.Presheaf.equalizerSieve

added theorem CategoryTheory.Presheaf.equalizerSieve_eq_top_iff

added theorem CategoryTheory.Presheaf.equalizerSieve_mem

added theorem CategoryTheory.Presheaf.equalizerSieve_mem_of_equalizerSieve_app_mem

added theorem CategoryTheory.Presheaf.equalizerSieve_self_eq_top

added theorem CategoryTheory.Presheaf.isLocallyInjective_comp_iff

added theorem CategoryTheory.Presheaf.isLocallyInjective_forget_iff

added theorem CategoryTheory.Presheaf.isLocallyInjective_iff_equalizerSieve_mem_imp

added theorem CategoryTheory.Presheaf.isLocallyInjective_iff_injective_of_separated

added theorem CategoryTheory.Presheaf.isLocallyInjective_iff_of_fac

added theorem CategoryTheory.Presheaf.isLocallyInjective_of_injective

added theorem CategoryTheory.Presheaf.isLocallyInjective_of_isLocallyInjective

added theorem CategoryTheory.Presheaf.isLocallyInjective_of_isLocallyInjective_fac

added theorem CategoryTheory.Sheaf.isLocallyInjective_iff_injective

Renamed Mathlib/CategoryTheory/Sites/Surjective.lean to Mathlib/CategoryTheory/Sites/LocallySurjective.lean

Modified Mathlib/Topology/Sheaves/LocallySurjective.lean