Topological reconstruction of varieties

DefinitionStructure morphism of a projective spectrum#✓fully proved

Let \(R\) be a commutative ring and \(A\) a commutative \(R\)-algebra graded by \(R\)-submodules \(\mathcal{A}_0, \mathcal{A}_1, \dots\). The structure morphism \(\operatorname{Proj} \mathcal{A} \to \operatorname{Spec} R\) is the canonical morphism \(\operatorname{Proj} \mathcal{A} \to \operatorname{Spec} \mathcal{A}_0\) followed by the morphism \(\operatorname{Spec} \mathcal{A}_0 \to \operatorname{Spec} R\) induced by the algebra map \(R \to \mathcal{A}_0\).

For a polynomial ring over \(R\) graded by total degree, this is the structure morphism of projective space over \(R\).

noncomputable def projToSpec {R A : Type u} [CommRing R] [CommRing A] [Algebra R A]
    (𝒜 : ℕ → Submodule R A) [GradedAlgebra 𝒜] : Proj 𝒜 ⟶ Spec (.of R) :=
  Proj.toSpecZero 𝒜 ≫ Spec.map (CommRingCat.ofHom (algebraMap ..))

Used by 1

Used byProjective morphism to an affine scheme

DefinitionProjective morphism to an affine scheme#✓fully proved

Let \(R\) be a commutative ring and \(X\) a scheme. A morphism \(f : X \to \operatorname{Spec} R\) is projective if there are \(n \in \mathbb{N}\) and a closed immersion \(i\) of \(X\) into \(\operatorname{Proj} R[x_1, \dots, x_n]\), the polynomial ring graded by total degree, such that \(f\) is \(i\) followed by the structure morphism \(\operatorname{Proj} R[x_1, \dots, x_n] \to \operatorname{Spec} R\).

def IsProjectiveHom {X : Scheme} {R : Type*} [CommRing R] (f : X ⟶ Spec (.of R)) : Prop :=
  let := @MvPolynomial.gradedAlgebra
  ∃ (n : ℕ) (i : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin n) R)),
    IsClosedImmersion i ∧ f = i ≫ projToSpec _

Uses 1 · Used by 1

Statement usesStructure morphism of a projective spectrum

Used byKollár–Lieblich–Olsson–Sawin topological reconstruction theorem

DefinitionNormal scheme#✓fully proved

A scheme \(X\) is normal if for every point \(x \in X\) the local ring \(\mathcal{O}_{X,x}\) is an integrally closed domain.

def IsNormalScheme (X : Scheme) : Prop :=
  ∀ x : X, IsDomain (X.presheaf.stalk x) ∧ IsIntegrallyClosed (X.presheaf.stalk x)

Used by 1

Used byKollár–Lieblich–Olsson–Sawin topological reconstruction theorem

TheoremKollár–Lieblich–Olsson–Sawin topological reconstruction theorem#●ready to prove

Let \(K\) and \(L\) be fields of characteristic zero, and let \(X\) and \(Y\) be irreducible normal schemes with projective morphisms \(f : X \to \operatorname{Spec} K\) and \(g : Y \to \operatorname{Spec} L\). Suppose that the Krull dimension of the underlying topological space of \(X\) is at least \(4\); or it is at least \(3\) and \(K\) and \(L\) are essentially of finite type over \(\mathbb{Q}\); or it is at least \(2\) and \(K\) and \(L\) are uncountable. Then for every homeomorphism \(h : X \to Y\) there is an isomorphism of schemes \(X \cong Y\) whose underlying map is \(h\).

public theorem_wanted kollar_lieblich_olsson_sawin (X Y : Scheme.{u}) (K L : Type u)
    [Field K] [Field L] [CharZero K] [CharZero L] [IrreducibleSpace X] [IrreducibleSpace Y]
    (norm_X : IsNormalScheme X) (f : X ⟶ Spec (.of K)) (proj_f : IsProjectiveHom f)
    (norm_Y : IsNormalScheme Y) (g : Y ⟶ Spec (.of L)) (proj_g : IsProjectiveHom g)
    (h : 4 ≤ topologicalKrullDim X ∨
      (3 ≤ topologicalKrullDim X ∧ Algebra.EssFiniteType ℚ K ∧ Algebra.EssFiniteType ℚ L) ∨
      (2 ≤ topologicalKrullDim X ∧ Uncountable K ∧ Uncountable L))
    (homeo : X ≃ₜ Y) : ∃ iso : X ≅ Y, (iso.hom : X → Y) = homeo

Sources

• János Kollár, Max Lieblich, Martin Olsson, and Will Sawin. The Zariski topology, linear systems, and algebraic varieties. Problem kollar_lieblich_olsson_sawin of the lean-eval benchmark.

Uses 2

Statement usesNormal scheme · Projective morphism to an affine scheme

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.