Closed symmetric monoidal structure on light condensed modules

We define a symmetric monoidal structure on light condensed modules by localizing the symmetric monoidal structure on the presheaf category. By Day's reflection theorem, we obtain a closed structure.

instance LightCondensed.instIsMonoidalFunctorOppositeLightProfiniteModuleCatWCoherentTopology (R : Type u) [CommRing R] : (CategoryTheory.coherentTopology LightProfinite).W.IsMonoidal

instance LightCondensed.instMonoidalCategoryLightCondMod (R : Type u) [CommRing R] : CategoryTheory.MonoidalCategory (LightCondMod R)

instance LightCondensed.instMonoidalCategorySheafLightProfiniteCoherentTopologyModuleCat (R : Type u) [CommRing R] : CategoryTheory.MonoidalCategory (CategoryTheory.Sheaf (CategoryTheory.coherentTopology LightProfinite) (ModuleCat R))

instance LightCondensed.instSymmetricCategoryLightCondMod (R : Type u) [CommRing R] : CategoryTheory.SymmetricCategory (LightCondMod R)

instance LightCondensed.instMonoidalClosedFunctorOppositeLightProfiniteModuleCat (R : Type u) [CommRing R] : CategoryTheory.MonoidalClosed (CategoryTheory.Functor LightProfiniteᵒᵖ (ModuleCat R))

instance LightCondensed.instMonoidalClosedSheafLightProfiniteCoherentTopologyModuleCat (R : Type u) [CommRing R] : CategoryTheory.MonoidalClosed (CategoryTheory.Sheaf (CategoryTheory.coherentTopology LightProfinite) (ModuleCat R))

instance LightCondensed.instMonoidalClosedLightCondMod (R : Type u) [CommRing R] : CategoryTheory.MonoidalClosed (LightCondMod R)

instance LightCondensed.instMonoidalFunctorOppositeLightProfiniteModuleCatSheafCoherentTopologyPresheafToSheaf (R : Type u) [CommRing R] : (CategoryTheory.presheafToSheaf (CategoryTheory.coherentTopology LightProfinite) (ModuleCat R)).Monoidal

instance LightCondensed.instMonoidalLightCondSetLightCondModFree (R : Type u) [CommRing R] : (free R).Monoidal