The direct-sum algebra of a graded quasicoherent algebra

A graded quasicoherent algebra A = (Aₙ)ₙ on a scheme X has an underlying quasicoherent commutative 𝒪_X-algebra ⨁ₙ Aₙ: its underlying module is the direct sum (coproduct) of the homogeneous components, the product of homogeneous sections of degrees i and j is their homogeneous product in degree i + j, and the unit is the unit of A₀. A graded algebra morphism induces the direct sum of its components. This forgets the grading, and it is the algebra whose relative spectrum is the scheme affine over X attached to a graded quasicoherent algebra, for instance the linear scheme of a quasicoherent sheaf.

The construction is the image of A under the lax braided monoidal functor CategoryTheory.GradedObject.total, which sends a graded object to the coproduct of its components, on commutative monoid objects (CategoryTheory.Functor.mapCommMon); the direct sum is quasicoherent because coproducts of quasicoherent sheaves are.

Main declarations

• TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.toQuasicoherentAlgebra: the functor A ↦ ⨁ₙ Aₙ from graded quasicoherent algebras to quasicoherent algebras;
• TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.ιTotal: the inclusion of a homogeneous summand in the underlying direct sum;
• TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.isColimitιTotal and TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.toQuasicoherentAlgebra_hom_ext: these inclusions exhibit the underlying module as the coproduct of the homogeneous components;
• TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.toQuasicoherentAlgebra_tensor_hom_ext: morphisms out of the tensor square of the underlying module are determined on the summands Aᵢ ⊗ Aⱼ;
• TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.ιTotal_tensorHom_ιTotal_mul and TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.one_toQuasicoherentAlgebra: its multiplication restricts to the homogeneous multiplication on Aᵢ ⊗ Aⱼ, and its unit is the unit of A₀;
• TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.mul_ιTotal_comp and TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.one_ιTotal_comp: hence an algebra morphism out of ⨁ₙ Aₙ is multiplicative and unital on the homogeneous summands (mul_ιTotal and one_ιTotal for the identity);
• TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.ιTotal_toQuasicoherentAlgebra_map: the algebra morphism induced by a graded algebra morphism is its degree-n component on the summand Aₙ.

noncomputable def TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.toQuasicoherentAlgebra {X : AlgebraicGeometry.Scheme} : CategoryTheory.Functor (GradedQuasicoherentAlgebra X) (QuasicoherentAlgebra X)

The direct-sum algebra ⨁ₙ Aₙ underlying a graded quasicoherent algebra A, as a functor to quasicoherent algebras: the image of A under the lax braided total-object functor GradedObject.total, which is quasicoherent because each Aₙ is.

@[simp]

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.toQuasicoherentAlgebra_obj_obj_X {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) : (toQuasicoherentAlgebra.obj A).obj.X = (CategoryTheory.GradedObject.total ℕ X.Modules).obj A.obj.X

The underlying module of the direct-sum algebra is the direct sum of the homogeneous components.

noncomputable def TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.ιTotal {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) (n : ℕ) : A.obj.X n ⟶ (toQuasicoherentAlgebra.obj A).obj.X

The inclusion of the degree-n homogeneous component into the direct-sum algebra.

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.ιTotal_def {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) (n : ℕ) : A.ιTotal n = CategoryTheory.CategoryStruct.comp (A.obj.X.ιTotal n) (CategoryTheory.eqToHom ⋯)

The inclusion of the degree-n summand is the coprojection GradedObject.ιTotal into the total object, transported along the identification of the direct-sum algebra's underlying module with the total object.

noncomputable def TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.isColimitιTotal {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (toQuasicoherentAlgebra.obj A).obj.X A.ιTotal)

The underlying module of the direct-sum algebra is the coproduct of the homogeneous components, with coprojections ιTotal.

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.toQuasicoherentAlgebra_hom_ext {X : AlgebraicGeometry.Scheme} {A : GradedQuasicoherentAlgebra X} {M : X.Modules} {f g : (toQuasicoherentAlgebra.obj A).obj.X ⟶ M} (h : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (A.ιTotal n) f = CategoryTheory.CategoryStruct.comp (A.ιTotal n) g) : f = g

Morphisms out of the direct-sum algebra agree as soon as they agree on every homogeneous summand.

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.toQuasicoherentAlgebra_hom_ext_iff {X : AlgebraicGeometry.Scheme} {A : GradedQuasicoherentAlgebra X} {M : X.Modules} {f g : (toQuasicoherentAlgebra.obj A).obj.X ⟶ M} : f = g ↔ ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (A.ιTotal n) f = CategoryTheory.CategoryStruct.comp (A.ιTotal n) g

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.toQuasicoherentAlgebra_tensor_hom_ext {X : AlgebraicGeometry.Scheme} {A : GradedQuasicoherentAlgebra X} {M : X.Modules} {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj (toQuasicoherentAlgebra.obj A).obj.X (toQuasicoherentAlgebra.obj A).obj.X ⟶ M} (h : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (A.ιTotal i) (A.ιTotal j)) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (A.ιTotal i) (A.ιTotal j)) g) : f = g

Morphisms out of the tensor square of the direct-sum algebra agree as soon as they agree on every summand Aᵢ ⊗ Aⱼ.

@[simp]

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.ιTotal_tensorHom_ιTotal_mul {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) (i j : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (A.ιTotal i) (A.ιTotal j)) CategoryTheory.MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj A.obj.X A.obj.X i j (i + j) ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonObj.mul (i + j)) (A.ιTotal (i + j)))

On the summand Aᵢ ⊗ Aⱼ, the multiplication of the direct-sum algebra is the homogeneous multiplication Aᵢ ⊗ Aⱼ ⟶ Aᵢ₊ⱼ followed by the inclusion of the summand of degree i + j.

@[simp]

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.ιTotal_tensorHom_ιTotal_mul_assoc {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) (i j : ℕ) {Z : X.Modules} (h : (toQuasicoherentAlgebra.obj A).obj.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (A.ιTotal i) (A.ιTotal j)) (CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj A.obj.X A.obj.X i j (i + j) ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonObj.mul (i + j)) (CategoryTheory.CategoryStruct.comp (A.ιTotal (i + j)) h))

On the summand Aᵢ ⊗ Aⱼ, the multiplication of the direct-sum algebra is the homogeneous multiplication Aᵢ ⊗ Aⱼ ⟶ Aᵢ₊ⱼ followed by the inclusion of the summand of degree i + j.

@[simp]

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.one_toQuasicoherentAlgebra {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) : CategoryTheory.MonObj.one = CategoryTheory.CategoryStruct.comp CategoryTheory.GradedObject.Monoidal.tensorUnit₀.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonObj.one 0) (A.ιTotal 0))

The unit of the direct-sum algebra is the unit of A₀ followed by the inclusion of the summand of degree 0.

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.one_toQuasicoherentAlgebra_assoc {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) {Z : X.Modules} (h : (toQuasicoherentAlgebra.obj A).obj.X ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h = CategoryTheory.CategoryStruct.comp CategoryTheory.GradedObject.Monoidal.tensorUnit₀.inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonObj.one 0) (CategoryTheory.CategoryStruct.comp (A.ιTotal 0) h))

The unit of the direct-sum algebra is the unit of A₀ followed by the inclusion of the summand of degree 0.

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.mul_ιTotal {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) (i j : ℕ) : CategoryTheory.CategoryStruct.comp (A.obj.toMon.mul i j) (A.ιTotal (i + j)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (A.ιTotal i) (A.ιTotal j)) CategoryTheory.MonObj.mul

The homogeneous multiplication Aᵢ ⊗ Aⱼ ⟶ Aᵢ₊ⱼ followed by the inclusion of the summand Aᵢ₊ⱼ is the multiplication of the direct-sum algebra on the summand Aᵢ ⊗ Aⱼ.

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.mul_ιTotal_assoc {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) (i j : ℕ) {Z : X.Modules} (h : (toQuasicoherentAlgebra.obj A).obj.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (A.obj.toMon.mul i j) (A.ιTotal (i + j))) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (A.ιTotal i) (A.ιTotal j)) CategoryTheory.MonObj.mul) h

The homogeneous multiplication Aᵢ ⊗ Aⱼ ⟶ Aᵢ₊ⱼ followed by the inclusion of the summand Aᵢ₊ⱼ is the multiplication of the direct-sum algebra on the summand Aᵢ ⊗ Aⱼ.

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.one_ιTotal {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) : CategoryTheory.CategoryStruct.comp A.obj.toMon.one (A.ιTotal 0) = CategoryTheory.MonObj.one

The unit of A₀ followed by the inclusion of the summand A₀ is the unit of the direct-sum algebra.

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.one_ιTotal_assoc {X : AlgebraicGeometry.Scheme} (A : GradedQuasicoherentAlgebra X) {Z : X.Modules} (h : (toQuasicoherentAlgebra.obj A).obj.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp A.obj.toMon.one (A.ιTotal 0)) h = CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h

The unit of A₀ followed by the inclusion of the summand A₀ is the unit of the direct-sum algebra.

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.mul_ιTotal_comp {X : AlgebraicGeometry.Scheme} {B : CategoryTheory.CommMon X.Modules} (A : GradedQuasicoherentAlgebra X) (k : (toQuasicoherentAlgebra.obj A).obj ⟶ B) (i j : ℕ) : CategoryTheory.CategoryStruct.comp (A.obj.toMon.mul i j) (CategoryTheory.CategoryStruct.comp (A.ιTotal (i + j)) k.hom.hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp (A.ιTotal i) k.hom.hom) (CategoryTheory.CategoryStruct.comp (A.ιTotal j) k.hom.hom)) CategoryTheory.MonObj.mul

A morphism of commutative algebras k out of the direct-sum algebra ⨁ₙ Aₙ sends the homogeneous multiplication Aᵢ ⊗ Aⱼ ⟶ Aᵢ₊ⱼ to the product of its restrictions to Aᵢ and Aⱼ.

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.mul_ιTotal_comp_assoc {X : AlgebraicGeometry.Scheme} {B : CategoryTheory.CommMon X.Modules} (A : GradedQuasicoherentAlgebra X) (k : (toQuasicoherentAlgebra.obj A).obj ⟶ B) (i j : ℕ) {Z : X.Modules} (h : B.toMon.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (A.obj.toMon.mul i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (A.ιTotal (i + j)) k.hom.hom) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp (A.ιTotal i) k.hom.hom) (CategoryTheory.CategoryStruct.comp (A.ιTotal j) k.hom.hom)) CategoryTheory.MonObj.mul) h

A morphism of commutative algebras k out of the direct-sum algebra ⨁ₙ Aₙ sends the homogeneous multiplication Aᵢ ⊗ Aⱼ ⟶ Aᵢ₊ⱼ to the product of its restrictions to Aᵢ and Aⱼ.

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.one_ιTotal_comp {X : AlgebraicGeometry.Scheme} {B : CategoryTheory.CommMon X.Modules} (A : GradedQuasicoherentAlgebra X) (k : (toQuasicoherentAlgebra.obj A).obj ⟶ B) : CategoryTheory.CategoryStruct.comp A.obj.toMon.one (CategoryTheory.CategoryStruct.comp (A.ιTotal 0) k.hom.hom) = CategoryTheory.MonObj.one

A morphism of commutative algebras k out of the direct-sum algebra ⨁ₙ Aₙ sends the unit of A₀ to the unit of its target.

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.one_ιTotal_comp_assoc {X : AlgebraicGeometry.Scheme} {B : CategoryTheory.CommMon X.Modules} (A : GradedQuasicoherentAlgebra X) (k : (toQuasicoherentAlgebra.obj A).obj ⟶ B) {Z : X.Modules} (h : B.toMon.X ⟶ Z) : CategoryTheory.CategoryStruct.comp A.obj.toMon.one (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (A.ιTotal 0) k.hom.hom) h) = CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one h

A morphism of commutative algebras k out of the direct-sum algebra ⨁ₙ Aₙ sends the unit of A₀ to the unit of its target.

@[simp]

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.ιTotal_toQuasicoherentAlgebra_map {X : AlgebraicGeometry.Scheme} {A B : GradedQuasicoherentAlgebra X} (f : A ⟶ B) (n : ℕ) : CategoryTheory.CategoryStruct.comp (A.ιTotal n) (toQuasicoherentAlgebra.map f).hom.hom.hom = CategoryTheory.CategoryStruct.comp (f.hom.hom.hom n) (B.ιTotal n)

On the summand Aₙ, the algebra morphism induced by a graded algebra morphism f is the degree-n component of f.

theorem TauCeti.AlgebraicGeometry.GradedQuasicoherentAlgebra.ιTotal_toQuasicoherentAlgebra_map_assoc {X : AlgebraicGeometry.Scheme} {A B : GradedQuasicoherentAlgebra X} (f : A ⟶ B) (n : ℕ) {Z : X.Modules} (h : (toQuasicoherentAlgebra.obj B).obj.toMon.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (A.ιTotal n) (toQuasicoherentAlgebra.map f).hom.hom.hom) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (f.hom.hom.hom n) (B.ιTotal n)) h

On the summand Aₙ, the algebra morphism induced by a graded algebra morphism f is the degree-n component of f.