Commit 2024-11-07 20:41 8a68a742

View on Github →

feat(CategoryTheory/Sites): chosen finite products on sheaves (#18633) Introduce a ChosenFiniteProduct instance on sheaves on a category C with a Grothendieck topology J whenever the coefficient category A has a ChosenFiniteProduct instance. We also provide some basic simp lemmas to relate this structure to the one on Cᵒᵖ ⥤ A.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Sites/ChosenFiniteProducts.lean

added theorem CategoryTheory.Sheaf.chosenFiniteProducts_fst_val

added theorem CategoryTheory.Sheaf.chosenFiniteProducts_lift_val

added theorem CategoryTheory.Sheaf.chosenFiniteProducts_snd_val

added theorem CategoryTheory.Sheaf.chosenFiniteProducts_whiskerLeft_val

added theorem CategoryTheory.Sheaf.chosenFiniteProducts_whiskerRight_val

added theorem CategoryTheory.Sheaf.tensorProd_isSheaf

added theorem CategoryTheory.Sheaf.tensorUnit_isSheaf