Motivic invariants of birational maps | Lean AI formalization leaderboard

Loading leaderboard data…

Problem statement

Notes: Unavailable.

Source: H.-Y. Lin and E. Shinder, `Motivic invariants of birational maps`, Annals of Math, 199 (1) 2024. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge (v1.0.0, e32eb14), AnnalsChallenge/AnnalsOfMathematics/2024-199-1-MotivicInvariants.lean

Informal solution: Unavailable.

/--
Statement of Theorem 1.2 (1) (a):

When `𝕜` is a number field, `Cr₃(𝕜)` is not generated by pseudo-regularizable elements.
-/
theorem declaration uses `sorry`theorem_1_2_1_a [NumberField 𝕜] :
    ¬ GenByPseudoRegularizable 𝕜 3 := by𝕜:Typeinst✝¹:Field 𝕜inst✝:NumberField 𝕜⊢ ¬GenByPseudoRegularizable 𝕜 3
  sorryAll goals completed! 🐙

/--
Statement of Theorem 1.2 (1) (b):

When `𝕜` is a function field over a number field, `Cr₃(𝕜)` is not generated by pseudo-regularizable
elements.

Here by a function field, we mean a function field of a positive-dimensional `𝔽`-variety.
-/
theorem declaration uses `sorry`theorem_1_2_1_b [NumberField 𝔽] (X : Scheme) [Variety 𝔽 X]
    (hX : 0 < topologicalKrullDim X) :
    ¬ GenByPseudoRegularizable X.functionField 3 := by𝔽:Typeinst✝²:Field 𝔽inst✝¹:NumberField 𝔽X:Schemeinst✝:Variety 𝔽 XhX:0 < topologicalKrullDim ↥X⊢ ¬GenByPseudoRegularizable (↑X.functionField) 3
  sorryAll goals completed! 🐙

/--
Statement of Theorem 1.2 (1) (c):

When `𝕜` is a function field over a finite field, `Cr₃(𝕜)` is not generated by pseudo-regularizable
elements.

Here by a function field, we mean a function field of a positive-dimensional `𝔽`-variety.
-/
theorem declaration uses `sorry`theorem_1_2_1_c [Finite 𝔽] (X : Scheme) [Variety 𝔽 X]
    (hX : 0 < topologicalKrullDim X) :
    ¬ GenByPseudoRegularizable X.functionField 3 := by𝔽:Typeinst✝²:Field 𝔽inst✝¹:Finite 𝔽X:Schemeinst✝:Variety 𝔽 XhX:0 < topologicalKrullDim ↥X⊢ ¬GenByPseudoRegularizable (↑X.functionField) 3
  sorryAll goals completed! 🐙

/--
Statement of Theorem 1.2 (1) (d):

When `𝕜` is a function field over an algebraically closed field, `Cr₃(𝕜)` is not generated by
pseudo-regularizable elements.

Here by a function field, we mean a function field of a positive-dimensional `𝔽`-variety.
-/
theorem declaration uses `sorry`theorem_1_2_1_d [IsAlgClosed 𝔽] (X : Scheme) [Variety 𝔽 X]
    (hX : 0 < topologicalKrullDim X) :
    ¬ GenByPseudoRegularizable X.functionField 3 := by𝔽:Typeinst✝²:Field 𝔽inst✝¹:IsAlgClosed 𝔽X:Schemeinst✝:Variety 𝔽 XhX:0 < topologicalKrullDim ↥X⊢ ¬GenByPseudoRegularizable (↑X.functionField) 3
  sorryAll goals completed! 🐙

/--
Statement of Theorem 1.2 (2):

For subfields `𝕜 ≤ ℂ` and `n ≥ 4`, `Crₙ(𝕜)` is not generated by pseudo-regularizable elements.
-/
theorem declaration uses `sorry`theorem_1_2_2 {n : ℕ} (hn : 4 ≤ n) (𝕜 : Subfield ℂ) :
    ¬ GenByPseudoRegularizable 𝕜 n := byn:ℕhn:4 ≤ n𝕜:Subfield ℂ⊢ ¬GenByPseudoRegularizable (↥𝕜) n
  sorryAll goals completed! 🐙

/--
Statement of Theorem 1.2 (3):

For infinite fields `𝕜` and `n ≥ 5`, `Crₙ(𝕜)` is not generated by pseudo-regularizable elements.
-/
theorem declaration uses `sorry`theorem_1_2_3 {n : ℕ} (hn : 5 ≤ n) [Infinite 𝕜] :
    ¬ GenByPseudoRegularizable 𝕜 n := by𝕜:Typeinst✝¹:Field 𝕜n:ℕhn:5 ≤ ninst✝:Infinite 𝕜⊢ ¬GenByPseudoRegularizable 𝕜 n
  sorryAll goals completed! 🐙