The monoidal category structure on quadratic R-modules

The monoidal structure is simply the structure on the underlying modules, where the tensor product of two modules is equipped with the form constructed via QuadraticForm.tmul.

As with the monoidal structure on ModuleCat, the universe level of the modules must be at least the universe level of the ring, so that we have a monoidal unit. For now, we simplify by insisting both universe levels are the same.

Implementation notes

This file essentially mirrors Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean.

@[reducible, inline]

noncomputable abbrev QuadraticModuleCat.instMonoidalCategory.tensorObj {R : Type u} [CommRing R] [Invertible 2] (X : QuadraticModuleCat R) (Y : QuadraticModuleCat R) : QuadraticModuleCat R

Auxiliary definition used to build QuadraticModuleCat.instMonoidalCategory.

Equations

• QuadraticModuleCat.instMonoidalCategory.tensorObj X Y = QuadraticModuleCat.of (X.form.tmul Y.form)

@[simp]

theorem QuadraticModuleCat.instMonoidalCategory.tensorObj_form {R : Type u} [CommRing R] [Invertible 2] (X : QuadraticModuleCat R) (Y : QuadraticModuleCat R) : (QuadraticModuleCat.instMonoidalCategory.tensorObj X Y).form = X.form.tmul Y.form

@[reducible, inline]

noncomputable abbrev QuadraticModuleCat.instMonoidalCategory.tensorHom {R : Type u} [CommRing R] [Invertible 2] {W : QuadraticModuleCat R} {X : QuadraticModuleCat R} {Y : QuadraticModuleCat R} {Z : QuadraticModuleCat R} (f : W ⟶ X) (g : Y ⟶ Z) : QuadraticModuleCat.instMonoidalCategory.tensorObj W Y ⟶ QuadraticModuleCat.instMonoidalCategory.tensorObj X Z

Auxiliary definition used to build QuadraticModuleCat.instMonoidalCategory.

We want this up front so that we can re-use it to define whiskerLeft and whiskerRight.

Equations

• QuadraticModuleCat.instMonoidalCategory.tensorHom f g = { toIsometry := f.toIsometry.tmul g.toIsometry }

noncomputable instance QuadraticModuleCat.instMonoidalCategoryStruct {R : Type u} [CommRing R] [Invertible 2] : CategoryTheory.MonoidalCategoryStruct (QuadraticModuleCat R)

Equations

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

@[simp]

theorem QuadraticModuleCat.toModuleCat_tensor {R : Type u} [CommRing R] [Invertible 2] (X : QuadraticModuleCat R) (Y : QuadraticModuleCat R) : (CategoryTheory.MonoidalCategory.tensorObj X Y).toModuleCat = CategoryTheory.MonoidalCategory.tensorObj X.toModuleCat Y.toModuleCat

theorem QuadraticModuleCat.forget₂_map_associator_hom {R : Type u} [CommRing R] [Invertible 2] (X : QuadraticModuleCat R) (Y : QuadraticModuleCat R) (Z : QuadraticModuleCat R) : (CategoryTheory.forget₂ (QuadraticModuleCat R) (ModuleCat R)).map (CategoryTheory.MonoidalCategory.associator X Y Z).hom = (CategoryTheory.MonoidalCategory.associator X.toModuleCat Y.toModuleCat Z.toModuleCat).hom

theorem QuadraticModuleCat.forget₂_map_associator_inv {R : Type u} [CommRing R] [Invertible 2] (X : QuadraticModuleCat R) (Y : QuadraticModuleCat R) (Z : QuadraticModuleCat R) : (CategoryTheory.forget₂ (QuadraticModuleCat R) (ModuleCat R)).map (CategoryTheory.MonoidalCategory.associator X Y Z).inv = (CategoryTheory.MonoidalCategory.associator X.toModuleCat Y.toModuleCat Z.toModuleCat).inv

noncomputable instance QuadraticModuleCat.instMonoidalCategory {R : Type u} [CommRing R] [Invertible 2] : CategoryTheory.MonoidalCategory (QuadraticModuleCat R)

Equations

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

noncomputable def QuadraticModuleCat.toModuleCatMonoidalFunctor (R : Type u) [CommRing R] [Invertible 2] : CategoryTheory.MonoidalFunctor (QuadraticModuleCat R) (ModuleCat R)

forget₂ (QuadraticModuleCat R) (ModuleCat R) as a monoidal functor.

Equations

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

noncomputable instance QuadraticModuleCat.instFaithfulModuleCatToModuleCatMonoidalFunctor {R : Type u} [CommRing R] [Invertible 2] : (QuadraticModuleCat.toModuleCatMonoidalFunctor R).Faithful

Equations

• ⋯ = ⋯