Commit 2025-01-29 09:23 6dc054c5

View on Github →

feat(CategoryTheory): Subpresheaf is a complete lattice (#20840) The type of subpresheaves of a given presheaf of sets is a complete lattice.

Estimated changes

Modified Mathlib/CategoryTheory/Sites/LocallySurjective.lean

Modified Mathlib/CategoryTheory/Subpresheaf/Basic.lean

added theorem CategoryTheory.Subpresheaf.bot_obj

modified theorem CategoryTheory.Subpresheaf.eq_top_iff_isIso

modified def CategoryTheory.Subpresheaf.homOfLe

modified theorem CategoryTheory.Subpresheaf.homOfLe_ι

added theorem CategoryTheory.Subpresheaf.iInf_obj

added theorem CategoryTheory.Subpresheaf.iSup_min

added theorem CategoryTheory.Subpresheaf.iSup_obj

modified theorem CategoryTheory.Subpresheaf.le_def

added theorem CategoryTheory.Subpresheaf.max_min

added theorem CategoryTheory.Subpresheaf.max_obj

added theorem CategoryTheory.Subpresheaf.min_obj

modified theorem CategoryTheory.Subpresheaf.nat_trans_naturality

added theorem CategoryTheory.Subpresheaf.sInf_obj

added theorem CategoryTheory.Subpresheaf.sSup_obj

modified def CategoryTheory.Subpresheaf.toPresheaf

added theorem CategoryTheory.Subpresheaf.top_obj

modified def CategoryTheory.Subpresheaf.ι

deleted theorem CategoryTheory.top_subpresheaf_obj