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)

Equations

• LightCondensed.instMonoidalCategoryLightCondMod R = CategoryTheory.Sheaf.monoidalCategory (CategoryTheory.coherentTopology LightProfinite) (ModuleCat R)

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

Equations

• LightCondensed.instMonoidalCategorySheafLightProfiniteCoherentTopologyModuleCat R = inferInstanceAs (CategoryTheory.MonoidalCategory (LightCondMod R))

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

Equations

• LightCondensed.instSymmetricCategoryLightCondMod R = CategoryTheory.Sheaf.symmetricCategory (CategoryTheory.coherentTopology LightProfinite) (ModuleCat R)

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• LightCondensed.instMonoidalClosedLightCondMod R = inferInstanceAs (CategoryTheory.MonoidalClosed (CategoryTheory.Sheaf (CategoryTheory.coherentTopology LightProfinite) (ModuleCat R)))

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

Equations

• LightCondensed.instMonoidalFunctorOppositeLightProfiniteModuleCatSheafCoherentTopologyPresheafToSheaf R = inferInstance

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

Equations

• One or more equations did not get rendered due to their size.