Topological reconstruction theorems for varieties | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: János Kollár, Max Lieblich, Martin Olsson, and Will Sawin. The Zariski topology, linear systems, and algebraic varieties.

Informal solution: Unavailable.

theorem declaration uses `sorry`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 : LeanEval.AlgebraicGeometry.TopologicalReconstruction.IsNormalScheme X) (f : X ⟶ Spec (.of K)) (proj_f : LeanEval.AlgebraicGeometry.TopologicalReconstruction.IsProjectiveHom f)
    (norm_Y : LeanEval.AlgebraicGeometry.TopologicalReconstruction.IsNormalScheme Y) (g : Y ⟶ Spec (.of L)) (proj_g : LeanEval.AlgebraicGeometry.TopologicalReconstruction.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 := byX:SchemeY:SchemeK:Type uL:Type uinst✝⁵:Field Kinst✝⁴:Field Linst✝³:CharZero Kinst✝²:CharZero Linst✝¹:IrreducibleSpace ↥Xinst✝:IrreducibleSpace ↥Ynorm_X:IsNormalScheme Xf:X ⟶ Spec ↧Kproj_f:IsProjectiveHom fnorm_Y:IsNormalScheme Yg:Y ⟶ Spec ↧Lproj_g:IsProjectiveHom gh:4 ≤ topologicalKrullDim ↥X ∨
  3 ≤ topologicalKrullDim ↥X ∧ Algebra.EssFiniteType ℚ K ∧ Algebra.EssFiniteType ℚ L ∨
    2 ≤ topologicalKrullDim ↥X ∧ Uncountable K ∧ Uncountable Lhomeo:↥X ≃ₜ ↥Y⊢ ∃ iso, ⇑iso.hom = ⇑homeo
  sorryAll goals completed! 🐙