instMonoidalCategory — Mathlib

English

The MonoidalCategory structure on QuadraticModuleCat R is defined by inducing the monoidal structure from ModuleCat via forget₂, with the appropriate unit, associator, and tensor product data.

Русский

Структура моноидальной категории для QuadraticModuleCat R определяется как индукция моноидальной структуры от ModuleCat через forget₂, с соответствующей единицей, ассоциатором и тензорной операцией.

LaTeX

$$$ \text{MonoidalCategory}(\text{QuadraticModuleCat}(R)) $$$

Lean4

instance instMonoidalCategory : MonoidalCategory (QuadraticModuleCat.{u} R) :=
  Monoidal.induced (forget₂ (QuadraticModuleCat R) (ModuleCat R))
    { μIso := fun _ _ => Iso.refl _
      εIso := Iso.refl _
      leftUnitor_eq := fun X =>
        by
        simp only [forget₂_obj, forget₂_map, Iso.refl_symm, Iso.trans_assoc, Iso.trans_hom, Iso.refl_hom,
          MonoidalCategory.tensorIso_hom, MonoidalCategory.tensorHom_id]
        dsimp only [toModuleCat_tensor, ModuleCat.of_coe]
        erw [MonoidalCategory.id_whiskerRight]
        simp
        rfl
      rightUnitor_eq := fun X =>
        by
        simp only [forget₂_obj, forget₂_map, Iso.refl_symm, Iso.trans_assoc, Iso.trans_hom, Iso.refl_hom,
          MonoidalCategory.tensorIso_hom, MonoidalCategory.id_tensorHom]
        dsimp only [toModuleCat_tensor, ModuleCat.of_coe]
        erw [MonoidalCategory.whiskerLeft_id]
        simp
        rfl
      associator_eq := fun X Y Z => by
        dsimp only [forget₂_obj, forget₂_map_associator_hom]
        simp only [Iso.refl_symm, Iso.trans_hom, MonoidalCategory.tensorIso_hom, Iso.refl_hom,
          MonoidalCategory.id_tensorHom_id]
        dsimp only [toModuleCat_tensor, ModuleCat.of_coe]
        rw [Category.id_comp, Category.id_comp, Category.comp_id, MonoidalCategory.id_tensorHom_id, Category.id_comp] }

Похожие утверждения