Graded coefficient inclusion and images of the irrelevant ideal

For a surjective graded ring homomorphism f : 𝒜 →+*ᵍ ℬ, the irrelevant ideal ℬ₊ is contained in the image 𝒜₊.map f of the irrelevant ideal 𝒜₊. This containment is the hypothesis under which f induces AlgebraicGeometry.Proj.map f : Proj ℬ ⟶ Proj 𝒜.

Degreewise rescaling by powers of a unit preserves the condition that a coordinate map sends the irrelevant ideal to the unit ideal, allowing the rescaled coordinates to define a morphism to Proj as well.

Coefficient inclusion also satisfies this containment, although it need not be surjective. TauCeti.GradedAlgebra.baseChangeMap uses the same ring inclusion as Mathlib's GradedAlgHom.includeRight, with the target grading over the extended coefficient ring. This is the form needed for homogeneous localizations and projective coefficient projections.

Main results

• HomogeneousIdeal.irrelevant_le_map_of_surjective: ℬ₊ ≤ 𝒜₊.map f for a surjective f.
• HomogeneousIdeal.irrelevant_le_map_baseChangeMap: the same containment for extension of the coefficient ring.

theorem HomogeneousIdeal.irrelevant_le_map_of_surjective {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_4} {τ : Type u_5} [Semiring A] [Semiring B] [SetLike σ A] [SetLike τ B] [AddSubmonoidClass σ A] [AddSubmonoidClass τ B] [DecidableEq ι] [AddCommMonoid ι] [PartialOrder ι] [CanonicallyOrderedAdd ι] {𝒜 : ι → σ} {ℬ : ι → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : Function.Surjective ⇑f) : irrelevant ℬ ≤ map f (irrelevant 𝒜)

For a surjective graded ring homomorphism f : 𝒜 →+*ᵍ ℬ, the irrelevant ideal ℬ₊ is contained in the image 𝒜₊.map f of the irrelevant ideal 𝒜₊.

theorem TauCeti.HomogeneousIdeal.map_irrelevant_eq_top_of_unit_rescaling {A : Type u_1} {B : Type u_2} {σ : Type u_3} [Semiring A] [CommSemiring B] [SetLike σ A] [AddSubmonoidClass σ A] (𝒜 : ℕ → σ) [GradedRing 𝒜] (f g : A →+* B) (c : Bˣ) (h : ∀ (n : ℕ), 0 < n → ∀ a ∈ 𝒜 n, g a = ↑c ^ n * f a) (hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤) : Ideal.map g (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤

Unit rescaling in positive degrees preserves the condition that the irrelevant ideal maps to the unit ideal.

def TauCeti.GradedAlgebra.baseChangeMap {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Type u_4) [CommSemiring S] [Algebra R S] (𝒜 : ι → Submodule R A) : 𝒜 →+*ᵍ fun (n : ι) => Submodule.baseChange S (𝒜 n)

The coefficient inclusion as a graded ring map, using the grading over the extended coefficient ring rather than its restriction of scalars.

Equations

• TauCeti.GradedAlgebra.baseChangeMap S 𝒜 = { toRingHom := Algebra.TensorProduct.includeRight.toRingHom, map_mem := ⋯ }

@[simp]

theorem TauCeti.GradedAlgebra.baseChangeMap_apply {ι : Type u_1} {R : Type u_2} {A : Type u_3} [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Type u_4) [CommSemiring S] [Algebra R S] (𝒜 : ι → Submodule R A) (a : A) : (baseChangeMap S 𝒜) a = 1 ⊗ₜ[R] a

Coefficient extension sends a homogeneous element to its pure tensor with one.

theorem HomogeneousIdeal.irrelevant_le_map_baseChangeMap {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Algebra R A] (S : Type u_3) [CommSemiring S] [Algebra R S] (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] : (irrelevant fun (n : ℕ) => Submodule.baseChange S (𝒜 n)) ≤ map (TauCeti.GradedAlgebra.baseChangeMap S 𝒜) (irrelevant 𝒜)

The irrelevant ideal after scalar extension lies in the ideal generated by the images of the original positive-degree elements. In particular, coefficient extension defines a morphism of Proj.