Monoid objects in graded objects from homogeneous data #

For a monoidal category C and an additive monoid I, the tensor product of graded objects X ⊗ Y has the coproduct of the X i ⊗ Y j with i + j = n in degree n, and the unit is 𝟙_ C placed in degree 0. A monoid object structure on a graded object X is therefore the same as a family of homogeneous multiplications X i ⊗ X j ⟶ X (i + j) together with a unit 𝟙_ C ⟶ X 0, subject to the graded associativity and unit laws. This file proves the introduction direction of that description: it assembles such homogeneous data into a monoid object, a commutative monoid object when the homogeneous multiplications commute, and recognizes morphisms of monoid objects by their homogeneous components. In the other direction, it extracts the homogeneous unit and multiplications, together with their laws, from a monoid object in graded objects, and their graded commutativity from a commutative one. This is how graded algebras such as symmetric algebras, which are naturally described degree by degree, are given and used as monoid objects in graded objects.

Homogeneous data can be transported along a lax monoidal functor F : C ⥤ D: given identifications e n : Y n ≅ F.obj (X n), the multiplications Y i ⊗ Y j ⟶ F.obj (X i) ⊗ F.obj (X j) ⟶ F.obj (X i ⊗ X j) ⟶ F.obj (X (i + j)) ⟶ Y (i + j) and the unit 𝟙_ D ⟶ F.obj (𝟙_ C) ⟶ F.obj (X 0) ⟶ Y 0 satisfy the graded laws whenever the original data do, and the graded commutativity law too when F is lax braided. This is how a graded algebra described degree by degree on presheaves, such as a sectionwise symmetric algebra, passes to sheaves along sheafification.

Main declarations #

CategoryTheory.GradedObject.Monoidal.mulOfHomogeneous: the morphism X ⊗ X ⟶ X assembled from homogeneous multiplications, characterized by CategoryTheory.GradedObject.Monoidal.ιTensorObj_mulOfHomogeneous;
CategoryTheory.GradedObject.Monoidal.oneOfDegreeZero: the morphism 𝟙_ ⟶ X determined by a morphism 𝟙_ C ⟶ X 0;
CategoryTheory.GradedObject.monObjOfHomogeneous: the monoid object structure defined by homogeneous data satisfying the graded associativity and unit laws;
CategoryTheory.GradedObject.isCommMonObj_monObjOfHomogeneous: commutativity of that monoid object from graded commutativity of the homogeneous multiplications;
CategoryTheory.GradedObject.isMonHom_of_homogeneous: a morphism of graded objects between monoid objects is a monoid morphism once it preserves the unit in degree zero and the multiplication of homogeneous components;
CategoryTheory.Mon.mul and CategoryTheory.Mon.one: the homogeneous multiplication and degree-zero unit extracted from a monoid object in graded objects, together with their associativity, unit, and functoriality laws; CategoryTheory.CommMon.mul_comm is their graded commutativity for a commutative monoid object;
CategoryTheory.Mon.hom_ext_of_epi_mul: morphisms out of an ℕ-graded monoid object generated in degree one, in the sense that its unit and the multiplications A.X n ⊗ A.X 1 ⟶ A.X (n + 1) are epimorphisms, are determined by their degree-one components;
CategoryTheory.GradedObject.mul_assoc_of_laxMonoidal, CategoryTheory.GradedObject.one_mul_of_laxMonoidal, CategoryTheory.GradedObject.mul_one_of_laxMonoidal and CategoryTheory.GradedObject.mul_comm_of_laxBraided: the graded laws of homogeneous data transported along a lax monoidal (resp. lax braided) functor;
CategoryTheory.GradedObject.map_mul_of_laxMonoidal: transported morphisms commute with the transported homogeneous multiplications.