The total object of a graded object is lax monoidal #
For a monoidal category C with coproducts and an additive monoid I, the total object
GradedObject.total I C sends a graded object X to the coproduct ∐ᵢ Xᵢ of its components.
When tensoring on either side preserves coproducts indexed by I, the tensor product
(∐ᵢ Xᵢ) ⊗ (∐ⱼ Yⱼ) is the coproduct of the Xᵢ ⊗ Yⱼ, and sending the summand Xᵢ ⊗ Yⱼ to the
summand of degree i + j of X ⊗ Y makes the total object a lax monoidal functor from graded
objects (with the convolution tensor product) to C; its unit is the inclusion of 𝟙_ C in
degree 0. When C is braided and I is commutative, the functor is lax braided.
Consequently a (commutative) monoid object in graded objects, such as a graded algebra, has a
(commutative) monoid object as its total object, through CategoryTheory.Functor.mapMon and
CategoryTheory.Functor.mapCommMon: this is the direct-sum algebra underlying a graded
algebra.
Main declarations #
CategoryTheory.GradedObject.ιTotal: the inclusion of the summandXᵢinto∐ᵢ Xᵢ;CategoryTheory.GradedObject.descTotal: descent from the total object, characterized byCategoryTheory.GradedObject.ιTotal_descTotal, with extensionality given byCategoryTheory.GradedObject.total_hom_ext;CategoryTheory.GradedObject.totalTensorDesc: the morphism out of(∐ᵢ Xᵢ) ⊗ (∐ⱼ Yⱼ)given on each summandXᵢ ⊗ Yⱼ, with the extensionality lemmaCategoryTheory.GradedObject.total_tensor_hom_ext;CategoryTheory.GradedObject.totalLaxMonoidal: the lax monoidal structure on the total object, characterized byCategoryTheory.GradedObject.ιTotal_tensorHom_ιTotal_total_μandCategoryTheory.GradedObject.total_ε;CategoryTheory.GradedObject.totalLaxBraided: the total object is lax braided.
The inclusion of the summand X i into the total object ∐ᵢ Xᵢ of a graded object. It is
Sigma.ι with its target written as (total I C).obj X, so that it composes with the action of
total I C on morphisms and with its monoidal structure maps.
Instances For
On the summand Xᵢ, the total object of a morphism of graded objects is its component in
degree i.
On the summand Xᵢ, the total object of a morphism of graded objects is its component in
degree i.
A family of morphisms on the graded components descends to the total object.
Instances For
Descent from the total object restricts to the prescribed map on each component.
Descent from the total object restricts to the prescribed map on each component.
Morphisms out of a total object agree if they agree on every graded component.
Morphisms out of A ⊗ (∐ᵢ Xᵢ) agree as soon as they agree on every summand A ⊗ Xᵢ.
Morphisms out of (∐ᵢ Xᵢ) ⊗ A agree as soon as they agree on every summand Xᵢ ⊗ A.
The tensor product (∐ᵢ Xᵢ) ⊗ (∐ⱼ Yⱼ) is the coproduct of the Xᵢ ⊗ Yⱼ: the morphism out
of it given on each summand Xᵢ ⊗ Yⱼ by φ i j.
Instances For
On the summand Xᵢ ⊗ Yⱼ, totalTensorDesc φ is φ i j.
On the summand Xᵢ ⊗ Yⱼ, totalTensorDesc φ is φ i j.
Morphisms out of (∐ᵢ Xᵢ) ⊗ (∐ⱼ Yⱼ) agree as soon as they agree on every summand
Xᵢ ⊗ Yⱼ.
Morphisms out of ((∐ᵢ Xᵢ) ⊗ (∐ⱼ Yⱼ)) ⊗ (∐ₖ Zₖ) agree as soon as they agree on every
summand (Xᵢ ⊗ Yⱼ) ⊗ Zₖ.
The total object X ↦ ∐ᵢ Xᵢ is lax monoidal, when tensoring on either side preserves
coproducts indexed by I. Its tensor map sends the summand Xᵢ ⊗ Yⱼ of (∐ᵢ Xᵢ) ⊗ (∐ⱼ Yⱼ) to
the summand of degree i + j of X ⊗ Y (ιTotal_tensorHom_ιTotal_total_μ), and its unit is
the inclusion of 𝟙_ C in degree 0 (total_ε).
On the summand Xᵢ ⊗ Yⱼ, the tensor map of the total object is the inclusion of Xᵢ ⊗ Yⱼ
into the summand of degree n = i + j of X ⊗ Y.
On the summand Xᵢ ⊗ Yⱼ, the tensor map of the total object is the inclusion of Xᵢ ⊗ Yⱼ
into the summand of degree n = i + j of X ⊗ Y.
The unit of the total object is the inclusion of 𝟙_ C as the summand of degree 0.
The unit of the total object is the inclusion of 𝟙_ C as the summand of degree 0.
When C is braided and I is commutative, the total object is lax braided: on the summand
Xᵢ ⊗ Yⱼ, both composites are the braiding Xᵢ ⊗ Yⱼ ≅ Yⱼ ⊗ Xᵢ followed by the inclusion into
degree i + j.