Documentation

Hironaka.Scheme.BlowUp.Rees.Map

The graded Rees algebra along a ring map, and Proj.map over degree zero #

For a ring map φ : R → S and ideals I ⊆ R, J ⊆ S with φ(I) ⊆ J, applying φ to the coefficients sends Rees(I) = ⨁ Iⁿtⁿ into Rees(J) degreewise: the graded ring map reesAlgebra.mapOfLe φ hIJ : grading I →+*ᵍ grading J. These are the transition maps of the relative Proj of the Rees algebra of an ideal sheaf [TSPA, Tags 01OF and 0804]: they are induced by the restriction maps of the structure sheaf, along which I(U) = I(V) Γ(U). When J = I S, the degree-one elements b t, b ∈ J, are S-combinations of the images φ(a) t, a ∈ I, so the irrelevant ideal of Rees(J) lies in the image of that of Rees(I) (reesAlgebra.irrelevant_le_map_mapOfEq, from the generation in degree one of Hironaka.Scheme.BlowUp.Rees.Irrelevant) — the hypothesis under which Mathlib's Proj.map produces Proj Rees(J) ⟶ Proj Rees(I).

Mathlib's Proj.map comes with its chart compatibility awayι_comp_map but not with its compatibility with the structure map toSpecZero; Proj.map_toSpecZero below proves it for any graded ring map, by the affine cover of Proj and awayι_toSpecZero: on Spec (B_{f s})₀ both composites are Spec of the ring map 𝒜₀ → (B_{f s})₀, x ↦ f(x)/1.

Boundary cases #

No hypothesis on φ (it need not be flat or injective); I.map φ ≤ J suffices for the graded map, I.map φ = J for the Proj.map hypothesis. φ = id gives the identity graded map (reesAlgebra.mapOfLe_id) and composites compose (reesAlgebra.mapOfLe_comp).

source
@[simp]
theorem reesAlgebra.coe_mapOfLe_apply {R S : Type u} [CommRing R] [CommRing S] {I : Ideal R} {J : Ideal S} (φ : R →+* S) (hIJ : Ideal.map φ I ≤ J) (p : ↥(reesAlgebra I)) :
↑((mapOfLe φ hIJ) p) = Polynomial.map φ ↑p
source
theorem reesAlgebra.mapOfLe_degreeOne {R S : Type u} [CommRing R] [CommRing S] {I : Ideal R} {J : Ideal S} (φ : R →+* S) (hIJ : Ideal.map φ I ≤ J) (a : ↥I) :
(mapOfLe φ hIJ) ((degreeOne I) a) = (degreeOne J) ⟨φ ↑a, ⋯⟩
source
theorem reesAlgebra.mapOfLe_id {R : Type u} [CommRing R] {I : Ideal R} (h : Ideal.map (RingHom.id R) I ≤ I) :
mapOfLe (RingHom.id R) h = GradedRingHom.id (grading I)
source
theorem reesAlgebra.mapOfLe_comp {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] {I : Ideal R} {J : Ideal S} {K : Ideal T} (φ : R →+* S) (ψ : S →+* T) (hIJ : Ideal.map φ I ≤ J) (hJK : Ideal.map ψ J ≤ K) (hIK : Ideal.map (ψ.comp φ) I ≤ K) :
mapOfLe (ψ.comp φ) hIK = (mapOfLe ψ hJK).comp (mapOfLe φ hIJ)
source
theorem reesAlgebra.coe_mapOfLe_gradingZeroEquiv_symm {R S : Type u} [CommRing R] [CommRing S] {I : Ideal R} {J : Ideal S} (φ : R →+* S) (hIJ : Ideal.map φ I ≤ J) (r : R) :
↑((mapOfLe φ hIJ) ↑((gradingZeroEquiv I).symm r)) = ↑↑((gradingZeroEquiv J).symm (φ r))

The degree-zero restriction of a graded Rees map is the constant map φ, through the identifications grading I 0 ≅ R and grading J 0 ≅ S.

source
theorem reesAlgebra.irrelevant_le_map_mapOfEq {R S : Type u} [CommRing R] [CommRing S] {I : Ideal R} {J : Ideal S} (φ : R →+* S) (hJ : Ideal.map φ I = J) :
HomogeneousIdeal.irrelevant (grading J) ≤ HomogeneousIdeal.map (mapOfLe φ ⋯) (HomogeneousIdeal.irrelevant (grading I))

The Proj.map hypothesis: when J = I S, the irrelevant ideal of Rees(J) lies in the image of that of Rees(I), because Rees(J) is generated in degree one [Hau14, Definition 4.6] and every degree-one element b t, b ∈ J, is an S-combination of the images φ(a) t, a ∈ I.

source
def GradedRingHom.zeroRingHom {A B σ τ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) :
↥(𝒜 0) →+* ↥(ℬ 0)

The degree-zero part of a graded ring map, as a ring map 𝒜 0 →+* ℬ 0.

Equations
  • f.zeroRingHom = { toFun := fun (x : ↥(𝒜 0)) => ⟨f ↑x, ⋯⟩, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
    source
    @[simp]
    theorem GradedRingHom.coe_zeroRingHom_apply {A B σ τ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (x : ↥(𝒜 0)) :
    ↑(f.zeroRingHom x) = f ↑x
    source
    theorem AlgebraicGeometry.Away.map_fromZeroRingHom {A B σ τ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (s : A) (x : ↥(𝒜 0)) :
    (HomogeneousLocalization.Away.map f s) ((HomogeneousLocalization.fromZeroRingHom 𝒜 (Submonoid.powers s)) x) = (HomogeneousLocalization.fromZeroRingHom ℬ (Submonoid.powers (f s))) (f.zeroRingHom x)

    Away.map sends the constants of degree zero to the constants of degree zero.

    source
    theorem AlgebraicGeometry.Proj.awayι_map_toSpecZero {A B σ τ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) (i : ℕ+) (x : ↥(𝒜 ↑i)) :
    CategoryTheory.CategoryStruct.comp (awayι ℬ (f ↑x) ⋯ ⋯) (CategoryTheory.CategoryStruct.comp (map f hf) (toSpecZero 𝒜)) = CategoryTheory.CategoryStruct.comp (awayι ℬ (f ↑x) ⋯ ⋯) (CategoryTheory.CategoryStruct.comp (toSpecZero ℬ) (Spec.map (CommRingCat.ofHom f.zeroRingHom)))

    The chart-by-chart statement of Proj.map_toSpecZero: on the chart D₊(f x) of Proj ℬ both composites are Spec of the ring map 𝒜₀ → (B_{f x})₀, x ↦ f(x)/1.

    source
    theorem AlgebraicGeometry.Proj.map_toSpecZero {A B σ τ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) :
    CategoryTheory.CategoryStruct.comp (map f hf) (toSpecZero 𝒜) = CategoryTheory.CategoryStruct.comp (toSpecZero ℬ) (Spec.map (CommRingCat.ofHom f.zeroRingHom))

    Proj.map over the structure maps to degree zero: for a graded ring map f : 𝒜 → ℬ, the square Proj ℬ → Proj 𝒜 over Spec ℬ₀ → Spec 𝒜₀ commutes (Mathlib has the chart compatibility Proj.awayι_comp_map; this is its consequence for Proj.toSpecZero, by the affine cover of Proj ℬ and Proj.awayι_toSpecZero).

    source
    theorem AlgebraicGeometry.Proj.map_toSpecZero_assoc {A B σ τ : Type u} [CommRing A] [SetLike σ A] [AddSubgroupClass σ A] [CommRing B] [SetLike τ B] [AddSubgroupClass τ B] {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [GradedRing 𝒜] [GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜)) {Z : Scheme} (h : Spec ↧↥(𝒜 0) ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (map f hf) (CategoryTheory.CategoryStruct.comp (toSpecZero 𝒜) h) = CategoryTheory.CategoryStruct.comp (toSpecZero ℬ) (CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom f.zeroRingHom)) h)

    Proj.map over the structure maps to degree zero: for a graded ring map f : 𝒜 → ℬ, the square Proj ℬ → Proj 𝒜 over Spec ℬ₀ → Spec 𝒜₀ commutes (Mathlib has the chart compatibility Proj.awayι_comp_map; this is its consequence for Proj.toSpecZero, by the affine cover of Proj ℬ and Proj.awayι_toSpecZero).