Lean4
/-- Any `CartesianMonoidalCategory` on `A` induce a
`CartesianMonoidalCategory` structure on `A`-valued sheaves. -/
noncomputable instance cartesianMonoidalCategory : CartesianMonoidalCategory (Sheaf J A) :=
.ofChosenFiniteProducts
({
cone := asEmptyCone { val := 𝟙_ (Cᵒᵖ ⥤ A), cond := tensorUnit_isSheaf _ }
isLimit.lift f := ⟨toUnit f.pt.val⟩
isLimit.fac := by rintro _ ⟨⟨⟩⟩
isLimit.uniq x f h := Sheaf.hom_ext _ _ (toUnit_unique f.val _) }) fun X Y ↦
{ cone :=
BinaryFan.mk (P :=
{ val := X.val ⊗ Y.val
cond := tensorProd_isSheaf J X Y }) ⟨(fst _ _)⟩ ⟨(snd _ _)⟩
isLimit.lift f := ⟨lift (BinaryFan.fst f).val (BinaryFan.snd f).val⟩
isLimit.fac := by rintro s ⟨⟨j⟩⟩ <;> apply Sheaf.hom_ext <;> simp
isLimit.uniq x f
h := by
apply Sheaf.hom_ext
apply CartesianMonoidalCategory.hom_ext
· specialize h ⟨.left⟩
rw [Sheaf.hom_ext_iff] at h
simpa using h
· specialize h ⟨.right⟩
rw [Sheaf.hom_ext_iff] at h
simpa using h }
