Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Proj.valuativeCriterion_existence_aux

∀ {σ : Type u_1} {A : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {O : Type u_3} [inst_4 : CommRing O] [inst_5 : IsDomain O] [ValuationRing O] {K : Type u_4}
  [inst_7 : Field K] [inst_8 : Algebra O K] [IsFractionRing O K] (φ₀ : ↥(𝒜 0) →+* O) (ι : Type u_5) [Finite ι]
  (x : ι → A),
  Algebra.adjoin (↥(𝒜 0)) (Set.range x) = ⊤ →
    ∀ (j : ι) (φ : HomogeneousLocalization.Away 𝒜 (x j) →+* K),
      (algebraMap O K).comp φ₀ = φ.comp (HomogeneousLocalization.fromZeroRingHom 𝒜 (Submonoid.powers (x j))) →
        ∀ (d : ι → ℕ),
          (∀ (i : ι), 0 < d i) →
            ∀ (hxdi : ∀ (i : ι), x i ∈ 𝒜 (d i)),
              ∃ j₀ φ',
                φ'.comp (HomogeneousLocalization.awayMap 𝒜 ⋯ ⋯) = φ ∧
                  (φ'.comp (HomogeneousLocalization.awayMap 𝒜 ⋯ ⋯)).range ≤ (algebraMap O K).range

Let 𝒜 be a graded ring generated over 𝒜₀ by finitely many homogeneous elements. Suppose we have the following diagram for some homogeneous x with O a valuation ring and K = Frac(O). `` φ K ← 𝒜_{(x)} ↑ ↑ | | | | O ← - 𝒜₀ φ₀ ` Then there exists a lift φₗ : 𝒜_{(x₀)} →+* O for some x₀ such that these two diagrams exist and commute. ` φ' φ' K ← 𝒜_{(x x₀)} K ← 𝒜_{(x x₀)} ↑ ↑ ↖ ↑ | | φ ⟍ | | | ⟍ | O ← - 𝒜_{(x₀)} 𝒜_{(x)} φₗ ` This is the underlying algebraic statement of the valuative criterion for Proj 𝒜`.

Defined in

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper

Cited by

1 results in Mathlib

Foundations

Depth 101 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingSetLikeAddSubgroupClassGradedRingCommRingIsDomainValuationRingFieldAlgebraIsFractionRingFinite