Rational_variety

Reference: Wikipedia

class NoetherProblem.IsRationalExtension (K : Type u_1) (L : Type u_2) (ι : Type u_3) [Field K] [Field L] [Algebra K L] : Prop

A rational field extension is a field extension L/K isomorphic to a field of rational functions (in some arbitrary number of indeterminates.)

• pure_transcendental : Nonempty (L ≃ₐ[K] FractionRing (MvPolynomial ι K))

theorem NoetherProblem.rationalExtension_empty_index (K : Type u_1) (L : Type u_2) (ι : Type u_3) [Field K] [Field L] [Algebra K L] [IsEmpty ι] [IsRationalExtension K L ι] : Nonempty (L ≃ₐ[K] K)

If the index set ι is empty, then IsRationalExtension K L ι means that K, L are isomorphic as K algebras.

def NoetherProblem.HasNoetherProperty (K L ι : Type) [Field K] [Field L] [Fintype ι] [Algebra K L] [IsRationalExtension K L ι] : Prop

We say that a rational extension L of K has the Noether Property if for any finite subgroup H of the Galois group of L, the fixed field L^H is also a rational extension.

Equations

• NoetherProblem.HasNoetherProperty K L ι = ∀ (H : Subgroup (L ≃ₐ[K] L)), Finite ↥H → ∃ (ι' : Type), NoetherProblem.IsRationalExtension K (↥(IntermediateField.fixedField H)) ι'

theorem NoetherProblem.noether_problem : (∀ (K L ι : Type), Type → ∀ [inst : Field K] [inst_1 : Field L] [inst_2 : Fintype ι] [inst_3 : Algebra K L] [inst_4 : IsRationalExtension K L ι], HasNoetherProperty K L ι) ↔ False

The Noether Problem: let L be the field of rational functions in n indeterminates over K. Is it true that L/K has the Noether property?

Solution: False.

theorem NoetherProblem.noether_problem.variants.two {K L ι G : Type} [Field K] [Field L] [Fintype ι] [Algebra K L] [IsRationalExtension K L ι] (hι : Fintype.card ι = 2) : HasNoetherProperty K L ι

The Noether problem has a positive solution in the two indeterminate case.

theorem NoetherProblem.noether_problem.variants.three {K L ι G : Type} [Field K] [Field L] [Fintype ι] [Algebra K L] [IsRationalExtension K L ι] (hι : Fintype.card ι = 3) : HasNoetherProperty K L ι

The Noether problem has a positive solution in the three indeterminate case.

theorem NoetherProblem.noether_problem.variants.four {K L ι G : Type} [Field K] [Field L] [Fintype ι] [Algebra K L] [IsRationalExtension K L ι] (hι : Fintype.card ι = 4) : HasNoetherProperty K L ι

The Noether problem has a positive solution in the four indeterminate case.

theorem NoetherProblem.noether_problem.variants.forty_seven : ∃ (K : Type) (L : Type) (ι : Type) (G : Type) (x : Field K) (x_1 : Field L) (x_2 : Fintype ι) (x_3 : Algebra K L) (x_4 : IsRationalExtension K L ι), Fintype.card ι = 47 ∧ ¬HasNoetherProperty K L ι

One can find a counterexample to the Noether Problem's claim by considering a rational function field in 47 indeterminates.