Graded rings of sections of graded algebras

Let A = ⨁ₙ Aₙ be a graded algebra on a scheme X and let U be an open of X. The sections Γ(Aₙ, U) of the homogeneous components carry a native graded multiplication Γ(Aᵢ, U) × Γ(Aⱼ, U) → Γ(Aᵢ₊ⱼ, U): the homogeneous multiplication Aᵢ ⊗ Aⱼ ⟶ Aᵢ₊ⱼ applied to the image of x ⊗ₜ y in the sections of the tensor product. Together with the unit Γ(X, U) → Γ(A₀, U) this makes the family n ↦ Γ(Aₙ, U) a graded commutative Γ(X, U)-algebra, so that ⨁ n, Γ(Aₙ, U) is a commutative Γ(X, U)-algebra graded by its summands. Over an affine open this is the graded ring whose homogeneous pieces are the modules corresponding to the Aₙ when they are quasicoherent; it is the input of affine-local constructions with graded algebras, such as their relative spectra and relative Proj.

The graded laws are obtained by transporting the homogeneous laws of A along the lax braided sections functor Scheme.Modules.sectionsFunctor U (CategoryTheory.GradedObject.mul_assoc_of_laxMonoidal and its companions), and the graded ring is then assembled by TauCeti.ModuleCat.gCommRingOfHomogeneous.

This is the graded analogue of the ungraded construction of TauCeti/AlgebraicGeometry/Modules/Algebra/Sections.lean, whose CategoryTheory.CommMon.commRingSections, CategoryTheory.CommMon.restrictSections and CategoryTheory.CommMon.toSectionsPresheaf give the sections of a commutative 𝒪_X-algebra their ring structure, restriction maps and structure morphism; the restriction and naturality arguments here follow the proofs there.

Main declarations

• CategoryTheory.CommMon.gCommRingSections and CategoryTheory.CommMon.gAlgebraSections: the graded commutative Γ(X, U)-algebra structure on n ↦ Γ(Aₙ, U), characterized by sections_gMul_def, sections_gOne_def and gAlgebraSections_toFun;
• CategoryTheory.CommMon.gradedSectionsGrading: the grading of ⨁ n, Γ(Aₙ, U) by its summands, as an internally graded algebra in the sense of GradedAlgebra;
• CategoryTheory.CommMon.map_gMul_sections: restriction of sections preserves the homogeneous multiplication;
• CategoryTheory.CommMon.restrictGradedSections: restriction of sections along V ≤ U, a degree-preserving ring homomorphism, assembled into the presheaf of commutative rings gradedSectionsPresheaf under the structure presheaf of X (toGradedSectionsPresheaf); its graded form is CategoryTheory.CommMon.restrictGradedSectionsGradedHom;
• CategoryTheory.CommMon.gradedSectionsMap: the degree-preserving Γ(X, U)-algebra homomorphism induced by a morphism of graded algebras, natural in U (gradedSectionsPresheafMap); its graded form is CategoryTheory.CommMon.gradedSectionsGradedHom, which is surjective onto a homogeneous component over an affine open when the morphism is an epimorphism of quasicoherent sheaves in that degree (grade_subset_range_gradedSectionsGradedHom_of_epi).

@[instance_reducible]

noncomputable instance CategoryTheory.CommMon.gCommRingSections {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) (U : X.Opens) : DirectSum.GCommRing fun (n : ℕ) => ↑((A.X n).presheaf.obj (Opposite.op U))

The sections over U of the homogeneous components of a graded algebra form a graded commutative ring. The product of x : Γ(Aᵢ, U) and y : Γ(Aⱼ, U) is the homogeneous multiplication of A applied to the image of x ⊗ₜ y in the sections of Aᵢ ⊗ Aⱼ (sections_gMul_def).

@[instance_reducible]

noncomputable instance CategoryTheory.CommMon.gAlgebraSections {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) (U : X.Opens) : DirectSum.GAlgebra ↑(X.presheaf.obj (Opposite.op U)) fun (n : ℕ) => ↑((A.X n).presheaf.obj (Opposite.op U))

The sections over U of the homogeneous components of a graded algebra form a graded Γ(X, U)-algebra, whose structure map Γ(X, U) → Γ(A₀, U) is the unit of A (gAlgebraSections_toFun).

@[simp]

theorem CategoryTheory.CommMon.sections_gMul_def {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) (U : X.Opens) {i j : ℕ} (x : ↑((A.X i).presheaf.obj (Opposite.op U))) (y : ↑((A.X j).presheaf.obj (Opposite.op U))) : GradedMonoid.GMul.mul x y = (ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app (A.toMon.mul i j) U)) ((ConcreteCategory.hom (Functor.LaxMonoidal.μ (AlgebraicGeometry.Scheme.Modules.sectionsFunctor U) (A.toMon.X i) (A.toMon.X j))) (x ⊗ₜ[↑(X.presheaf.obj (Opposite.op U))] y))

The product of homogeneous sections x : Γ(Aᵢ, U) and y : Γ(Aⱼ, U) is the homogeneous multiplication of A applied to the image of x ⊗ₜ y under the tensor map of the sections functor.

@[simp]

theorem CategoryTheory.CommMon.sections_gOne_def {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) (U : X.Opens) : GradedMonoid.GOne.one = (ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app A.toMon.one U)) ((ConcreteCategory.hom (Functor.LaxMonoidal.ε (AlgebraicGeometry.Scheme.Modules.sectionsFunctor U))) 1)

The unit of the graded ring of sections is the unit of A applied to 1 : Γ(X, U).

@[simp]

theorem CategoryTheory.CommMon.gAlgebraSections_toFun {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) (U : X.Opens) (r : ↑(X.presheaf.obj (Opposite.op U))) : DirectSum.GAlgebra.toFun r = (ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app A.toMon.one U)) ((ConcreteCategory.hom (Functor.LaxMonoidal.ε (AlgebraicGeometry.Scheme.Modules.sectionsFunctor U))) r)

The structure map Γ(X, U) → Γ(A₀, U) of the graded algebra of sections is the unit of A on sections over U.

theorem CategoryTheory.CommMon.map_gMul_sections {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) {U V : X.Opens} (f : V ⟶ U) {i j : ℕ} (x : ↑((A.X i).presheaf.obj (Opposite.op U))) (y : ↑((A.X j).presheaf.obj (Opposite.op U))) : (ConcreteCategory.hom ((A.X (i + j)).presheaf.map f.op)) (GradedMonoid.GMul.mul x y) = GradedMonoid.GMul.mul ((ConcreteCategory.hom ((A.X i).presheaf.map f.op)) x) ((ConcreteCategory.hom ((A.X j).presheaf.map f.op)) y)

Restriction of sections along V ≤ U preserves the homogeneous multiplication.

noncomputable def CategoryTheory.CommMon.restrictGradedSections {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) {U V : X.Opens} (f : V ⟶ U) : (DirectSum ℕ fun (n : ℕ) => ↑((A.X n).presheaf.obj (Opposite.op U))) →+* DirectSum ℕ fun (n : ℕ) => ↑((A.X n).presheaf.obj (Opposite.op V))

Restriction of sections along an inclusion of opens V ≤ U, as a ring homomorphism between the graded rings of sections. It sends each homogeneous section to its restriction, in the same degree (restrictGradedSections_of).

@[simp]

theorem CategoryTheory.CommMon.restrictGradedSections_of {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) {U V : X.Opens} (f : V ⟶ U) (n : ℕ) (x : ↑((A.X n).presheaf.obj (Opposite.op U))) : (A.restrictGradedSections f) ((DirectSum.of (fun (n : ℕ) => ↑((A.X n).presheaf.obj (Opposite.op U))) n) x) = (DirectSum.of (fun (i : ℕ) => ↑((A.X i).presheaf.obj (Opposite.op V))) n) ((ConcreteCategory.hom ((A.X n).presheaf.map f.op)) x)

Restriction of a homogeneous section is the restriction of the section, in the same degree.

@[simp]

theorem CategoryTheory.CommMon.restrictGradedSections_id {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) (U : X.Opens) : A.restrictGradedSections (CategoryStruct.id U) = RingHom.id (DirectSum ℕ fun (n : ℕ) => ↑((A.X n).presheaf.obj (Opposite.op U)))

Restriction of sections along the identity of an open is the identity.

theorem CategoryTheory.CommMon.restrictGradedSections_comp {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) {U V : X.Opens} (f : V ⟶ U) {W : X.Opens} (g : W ⟶ V) : A.restrictGradedSections (CategoryStruct.comp g f) = (A.restrictGradedSections g).comp (A.restrictGradedSections f)

Restriction of sections along a composite of inclusions of opens is the composite of the restrictions.

@[simp]

theorem CategoryTheory.CommMon.restrictGradedSections_apply {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) {U V : X.Opens} (f : V ⟶ U) (x : DirectSum ℕ fun (n : ℕ) => ↑((A.X n).presheaf.obj (Opposite.op U))) (n : ℕ) : ((A.restrictGradedSections f) x) n = (ConcreteCategory.hom ((A.X n).presheaf.map f.op)) (x n)

Restriction of sections restricts each homogeneous component.

@[simp]

theorem CategoryTheory.CommMon.restrictGradedSections_algebraMap {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) {U V : X.Opens} (f : V ⟶ U) (r : ↑(X.presheaf.obj (Opposite.op U))) : (A.restrictGradedSections f) ((algebraMap (↑(X.presheaf.obj (Opposite.op U))) (DirectSum ℕ fun (n : ℕ) => ↑((A.X n).presheaf.obj (Opposite.op U)))) r) = (algebraMap (↑(X.presheaf.obj (Opposite.op V))) (DirectSum ℕ fun (n : ℕ) => ↑((A.X n).presheaf.obj (Opposite.op V)))) ((ConcreteCategory.hom (X.presheaf.map f.op)) r)

Restriction of sections commutes with the structure maps Γ(X, U) → ⨁ n, Γ(Aₙ, U).

@[reducible, inline]

noncomputable abbrev CategoryTheory.CommMon.gradedSectionsGrading {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) (U : X.Opens) : ℕ → Submodule (↑(X.presheaf.obj (Opposite.op U))) (DirectSum ℕ fun (n : ℕ) => ↑((A.X n).presheaf.obj (Opposite.op U)))

The grading of the ring ⨁ n, Γ(Aₙ, U) of sections of a graded algebra by its summands Γ(Aₙ, U).

theorem CategoryTheory.CommMon.of_mem_gradedSectionsGrading {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) {U : X.Opens} (n : ℕ) (x : ↑((A.X n).presheaf.obj (Opposite.op U))) : (DirectSum.of (fun (i : ℕ) => ↑((A.X i).presheaf.obj (Opposite.op U))) n) x ∈ A.gradedSectionsGrading U n

A homogeneous section of degree n lies in the degree-n summand.

noncomputable def CategoryTheory.CommMon.restrictGradedSectionsGradedHom {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) {U V : X.Opens} (i : V ⟶ U) : A.gradedSectionsGrading U →+*ᵍ A.gradedSectionsGrading V

Restriction of sections along an inclusion of opens V ≤ U, as a graded ring homomorphism between the graded rings of sections. Its underlying ring homomorphism is CategoryTheory.CommMon.restrictGradedSections (CategoryTheory.CommMon.restrictGradedSectionsGradedHom_toRingHom).

@[simp]

theorem CategoryTheory.CommMon.restrictGradedSectionsGradedHom_toRingHom {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) {U V : X.Opens} (i : V ⟶ U) : ↑(A.restrictGradedSectionsGradedHom i) = A.restrictGradedSections i

The underlying ring homomorphism of the graded restriction of sections is the restriction of sections.

@[simp]

theorem CategoryTheory.CommMon.restrictGradedSectionsGradedHom_apply {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) {U V : X.Opens} (i : V ⟶ U) (x : DirectSum ℕ fun (n : ℕ) => ↑((A.X n).presheaf.obj (Opposite.op U))) : (A.restrictGradedSectionsGradedHom i) x = (A.restrictGradedSections i) x

The graded restriction of sections is the restriction of sections.

@[simp]

theorem CategoryTheory.CommMon.restrictGradedSectionsGradedHom_id {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) (U : X.Opens) : A.restrictGradedSectionsGradedHom (CategoryStruct.id U) = GradedRingHom.id (A.gradedSectionsGrading U)

Graded restriction of sections along the identity is the identity.

theorem CategoryTheory.CommMon.restrictGradedSectionsGradedHom_comp {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) {U V W : X.Opens} (i : V ⟶ U) (j : W ⟶ V) : A.restrictGradedSectionsGradedHom (CategoryStruct.comp j i) = (A.restrictGradedSectionsGradedHom j).comp (A.restrictGradedSectionsGradedHom i)

Graded restriction of sections along a composite of inclusions is the composite of the graded restrictions.

noncomputable def CategoryTheory.CommMon.gradedSectionsPresheaf {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) : Functor X.Opensᵒᵖ CommRingCat

The presheaf of graded rings of sections of a graded algebra: it sends an open U to ⨁ n, Γ(Aₙ, U) and an inclusion of opens to restrictGradedSections.

@[simp]

theorem CategoryTheory.CommMon.gradedSectionsPresheaf_obj {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) (U : X.Opensᵒᵖ) : A.gradedSectionsPresheaf.obj U = ↧(DirectSum ℕ fun (n : ℕ) => ↑((A.X n).presheaf.obj (Opposite.op (Opposite.unop U))))

The graded ring of sections over U is the value of gradedSectionsPresheaf at U.

@[simp]

theorem CategoryTheory.CommMon.gradedSectionsPresheaf_map {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) {U V : X.Opensᵒᵖ} (f : U ⟶ V) : A.gradedSectionsPresheaf.map f = CommRingCat.ofHom (A.restrictGradedSections f.unop)

The restriction maps of gradedSectionsPresheaf are restrictGradedSections.

noncomputable def CategoryTheory.CommMon.toGradedSectionsPresheaf {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) : X.presheaf ⟶ A.gradedSectionsPresheaf

The structure morphism from the structure presheaf of X to the presheaf of graded rings of sections, given on each open U by the algebra map Γ(X, U) → ⨁ n, Γ(Aₙ, U) into degree zero.

@[simp]

theorem CategoryTheory.CommMon.toGradedSectionsPresheaf_app {X : AlgebraicGeometry.Scheme} (A : CommMon (GradedObject ℕ X.Modules)) (U : X.Opensᵒᵖ) : A.toGradedSectionsPresheaf.app U = CommRingCat.ofHom (algebraMap (↑(X.presheaf.obj (Opposite.op (Opposite.unop U)))) (DirectSum ℕ fun (n : ℕ) => ↑((A.X n).presheaf.obj (Opposite.op (Opposite.unop U)))))

The structure morphism toGradedSectionsPresheaf is the algebra map on each open.

noncomputable def CategoryTheory.CommMon.gradedSectionsMap {X : AlgebraicGeometry.Scheme} {A B : CommMon (GradedObject ℕ X.Modules)} (φ : A ⟶ B) (U : X.Opens) : (DirectSum ℕ fun (n : ℕ) => ↑((A.X n).presheaf.obj (Opposite.op U))) →ₐ[↑(X.presheaf.obj (Opposite.op U))] DirectSum ℕ fun (n : ℕ) => ↑((B.X n).presheaf.obj (Opposite.op U))

The Γ(X, U)-algebra homomorphism between graded rings of sections induced by a morphism of graded algebras. It applies the morphism degree by degree (gradedSectionsMap_of).

@[simp]

theorem CategoryTheory.CommMon.gradedSectionsMap_of {X : AlgebraicGeometry.Scheme} {A B : CommMon (GradedObject ℕ X.Modules)} (φ : A ⟶ B) (U : X.Opens) (n : ℕ) (x : ↑((A.X n).presheaf.obj (Opposite.op U))) : (gradedSectionsMap φ U) ((DirectSum.of (fun (n : ℕ) => ↑((A.X n).presheaf.obj (Opposite.op U))) n) x) = (DirectSum.of (fun (i : ℕ) => ↑((B.X i).presheaf.obj (Opposite.op U))) n) ((ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app (φ.hom.hom n) U)) x)

The map induced on graded rings of sections applies the morphism to each homogeneous section.

@[simp]

theorem CategoryTheory.CommMon.gradedSectionsMap_apply {X : AlgebraicGeometry.Scheme} {A B : CommMon (GradedObject ℕ X.Modules)} (φ : A ⟶ B) (U : X.Opens) (x : DirectSum ℕ fun (n : ℕ) => ↑((A.X n).presheaf.obj (Opposite.op U))) (i : ℕ) : ((gradedSectionsMap φ U) x) i = (ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app (φ.hom.hom i) U)) (x i)

The map induced on graded rings of sections applies the morphism to each homogeneous component.

@[simp]

theorem CategoryTheory.CommMon.gradedSectionsMap_id {X : AlgebraicGeometry.Scheme} {A : CommMon (GradedObject ℕ X.Modules)} (U : X.Opens) : gradedSectionsMap (CategoryStruct.id A) U = AlgHom.id (↑(X.presheaf.obj (Opposite.op U))) (DirectSum ℕ fun (n : ℕ) => ↑((A.X n).presheaf.obj (Opposite.op U)))

The identity morphism induces the identity on graded rings of sections.

theorem CategoryTheory.CommMon.gradedSectionsMap_comp {X : AlgebraicGeometry.Scheme} {A B C : CommMon (GradedObject ℕ X.Modules)} (φ : A ⟶ B) (ψ : B ⟶ C) (U : X.Opens) : gradedSectionsMap (CategoryStruct.comp φ ψ) U = (gradedSectionsMap ψ U).comp (gradedSectionsMap φ U)

The map induced on graded rings of sections by a composite is the composite of the induced maps.

theorem CategoryTheory.CommMon.gradedSectionsMap_restrictGradedSections {X : AlgebraicGeometry.Scheme} {A B : CommMon (GradedObject ℕ X.Modules)} (φ : A ⟶ B) {U V : X.Opens} (f : V ⟶ U) (x : DirectSum ℕ fun (n : ℕ) => ↑((A.X n).presheaf.obj (Opposite.op U))) : (gradedSectionsMap φ V) ((A.restrictGradedSections f) x) = (B.restrictGradedSections f) ((gradedSectionsMap φ U) x)

The maps induced on graded rings of sections commute with restriction.

noncomputable def CategoryTheory.CommMon.gradedSectionsGradedHom {X : AlgebraicGeometry.Scheme} {A B : CommMon (GradedObject ℕ X.Modules)} (φ : A ⟶ B) (U : X.Opens) : A.gradedSectionsGrading U →+*ᵍ B.gradedSectionsGrading U

The graded ring homomorphism between graded rings of sections induced by a morphism of graded algebras. Its underlying ring homomorphism is CategoryTheory.CommMon.gradedSectionsMap (CategoryTheory.CommMon.gradedSectionsGradedHom_toRingHom).

@[simp]

theorem CategoryTheory.CommMon.gradedSectionsGradedHom_toRingHom {X : AlgebraicGeometry.Scheme} {A B : CommMon (GradedObject ℕ X.Modules)} (φ : A ⟶ B) (U : X.Opens) : ↑(gradedSectionsGradedHom φ U) = (gradedSectionsMap φ U).toRingHom

The underlying ring homomorphism of the graded homomorphism of sections induced by φ is CategoryTheory.CommMon.gradedSectionsMap.

@[simp]

theorem CategoryTheory.CommMon.gradedSectionsGradedHom_apply {X : AlgebraicGeometry.Scheme} {A B : CommMon (GradedObject ℕ X.Modules)} (φ : A ⟶ B) (U : X.Opens) (x : DirectSum ℕ fun (n : ℕ) => ↑((A.X n).presheaf.obj (Opposite.op U))) : (gradedSectionsGradedHom φ U) x = (gradedSectionsMap φ U) x

The graded homomorphism of sections induced by φ applies CategoryTheory.CommMon.gradedSectionsMap.

@[simp]

theorem CategoryTheory.CommMon.gradedSectionsGradedHom_id {X : AlgebraicGeometry.Scheme} {A : CommMon (GradedObject ℕ X.Modules)} (U : X.Opens) : gradedSectionsGradedHom (CategoryStruct.id A) U = GradedRingHom.id (A.gradedSectionsGrading U)

The identity morphism induces the identity graded homomorphism of sections.

theorem CategoryTheory.CommMon.gradedSectionsGradedHom_comp {X : AlgebraicGeometry.Scheme} {A B C : CommMon (GradedObject ℕ X.Modules)} (φ : A ⟶ B) (ψ : B ⟶ C) (U : X.Opens) : gradedSectionsGradedHom (CategoryStruct.comp φ ψ) U = (gradedSectionsGradedHom ψ U).comp (gradedSectionsGradedHom φ U)

The graded homomorphism of sections induced by a composite is the composite of the induced graded homomorphisms.

theorem CategoryTheory.CommMon.gradedSectionsGradedHom_comp_restrictGradedSectionsGradedHom {X : AlgebraicGeometry.Scheme} {A B : CommMon (GradedObject ℕ X.Modules)} (φ : A ⟶ B) {U V : X.Opens} (i : V ⟶ U) : (gradedSectionsGradedHom φ V).comp (A.restrictGradedSectionsGradedHom i) = (B.restrictGradedSectionsGradedHom i).comp (gradedSectionsGradedHom φ U)

The graded homomorphisms of sections induced by φ commute with restriction.

theorem CategoryTheory.CommMon.grade_subset_range_gradedSectionsGradedHom_of_epi {X : AlgebraicGeometry.Scheme} {A B : CommMon (GradedObject ℕ X.Modules)} (φ : A ⟶ B) (U : X.Opens) (hU : AlgebraicGeometry.IsAffineOpen U) (i : ℕ) [hφ : Epi (φ.hom.hom i)] [hA : SheafOfModules.IsQuasicoherent (A.X i)] [hB : SheafOfModules.IsQuasicoherent (B.X i)] : ↑(B.gradedSectionsGrading U i) ⊆ Set.range ⇑(gradedSectionsGradedHom φ U)

Over an affine open, a morphism of graded algebras that is an epimorphism of quasicoherent module sheaves in degree i maps the graded ring of sections onto its homogeneous component of degree i.

noncomputable def CategoryTheory.CommMon.gradedSectionsPresheafMap {X : AlgebraicGeometry.Scheme} {A B : CommMon (GradedObject ℕ X.Modules)} (φ : A ⟶ B) : A.gradedSectionsPresheaf ⟶ B.gradedSectionsPresheaf

The morphism of presheaves of graded rings of sections induced by a morphism of graded algebras: on each open U it is gradedSectionsMap.

@[simp]

theorem CategoryTheory.CommMon.gradedSectionsPresheafMap_app {X : AlgebraicGeometry.Scheme} {A B : CommMon (GradedObject ℕ X.Modules)} (φ : A ⟶ B) (U : X.Opensᵒᵖ) : (gradedSectionsPresheafMap φ).app U = CommRingCat.ofHom (gradedSectionsMap φ (Opposite.unop U)).toRingHom

The components of gradedSectionsPresheafMap φ are the maps gradedSectionsMap φ.

@[simp]

theorem CategoryTheory.CommMon.gradedSectionsPresheafMap_id {X : AlgebraicGeometry.Scheme} {A : CommMon (GradedObject ℕ X.Modules)} : gradedSectionsPresheafMap (CategoryStruct.id A) = CategoryStruct.id A.gradedSectionsPresheaf

The identity morphism induces the identity of the presheaf of graded rings of sections.

theorem CategoryTheory.CommMon.gradedSectionsPresheafMap_comp {X : AlgebraicGeometry.Scheme} {A B C : CommMon (GradedObject ℕ X.Modules)} (φ : A ⟶ B) (ψ : B ⟶ C) : gradedSectionsPresheafMap (CategoryStruct.comp φ ψ) = CategoryStruct.comp (gradedSectionsPresheafMap φ) (gradedSectionsPresheafMap ψ)

The morphism of presheaves induced by a composite is the composite of the induced morphisms.

@[simp]

theorem CategoryTheory.CommMon.toGradedSectionsPresheaf_gradedSectionsPresheafMap {X : AlgebraicGeometry.Scheme} {A B : CommMon (GradedObject ℕ X.Modules)} (φ : A ⟶ B) : CategoryStruct.comp A.toGradedSectionsPresheaf (gradedSectionsPresheafMap φ) = B.toGradedSectionsPresheaf

The morphism of presheaves induced by a morphism of graded algebras is compatible with the structure morphisms from the structure presheaf.

@[simp]

theorem CategoryTheory.CommMon.toGradedSectionsPresheaf_gradedSectionsPresheafMap_assoc {X : AlgebraicGeometry.Scheme} {A B : CommMon (GradedObject ℕ X.Modules)} (φ : A ⟶ B) {Z : TopCat.Presheaf CommRingCat ↑X.toPresheafedSpace} (h : B.gradedSectionsPresheaf ⟶ Z) : CategoryStruct.comp A.toGradedSectionsPresheaf (CategoryStruct.comp (gradedSectionsPresheafMap φ) h) = CategoryStruct.comp B.toGradedSectionsPresheaf h

The morphism of presheaves induced by a morphism of graded algebras is compatible with the structure morphisms from the structure presheaf.