Commit 2021-12-02 12:47 68060507

View on Github →

feat(category_theory/sites/adjunction): Adjunctions between categories of sheaves. (#10541) We construct adjunctions between categories of sheaves obtained by composition (and sheafification) with functors which form a given adjunction. Will be used in LTE.

Estimated changes

Created src/category_theory/sites/adjunction.lean

added def category_theory.Sheaf.adjunction

added theorem category_theory.Sheaf.adjunction_counit_app

added theorem category_theory.Sheaf.adjunction_hom_equiv_apply

added theorem category_theory.Sheaf.adjunction_hom_equiv_symm_apply

added def category_theory.Sheaf.adjunction_to_types

added theorem category_theory.Sheaf.adjunction_to_types_counit_app

added theorem category_theory.Sheaf.adjunction_to_types_hom_equiv_apply

added theorem category_theory.Sheaf.adjunction_to_types_hom_equiv_symm_apply'

added theorem category_theory.Sheaf.adjunction_to_types_unit_app

added theorem category_theory.Sheaf.adjunction_unit_app

added def category_theory.Sheaf.compose_and_sheafify

added def category_theory.Sheaf.compose_and_sheafify_from_types

added def category_theory.Sheaf.compose_equiv

added def category_theory.Sheaf_forget