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_reducible]

noncomputable 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_reducible]

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

Equations

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

@[instance_reducible]

noncomputable 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_reducible]

noncomputable 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_reducible]

noncomputable 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_reducible]

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

Equations

• LightCondensed.instMonoidalClosedLightCondMod R = { closed := fun (X : LightCondMod R) => CategoryTheory.MonoidalClosed.closed X }

@[instance_reducible]

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

Equations

• LightCondensed.instMonoidalFunctorOppositeLightProfiniteModuleCatSheafCoherentTopologyPresheafToSheaf R = inferInstance

@[instance_reducible]

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

Equations

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