The algebra is the actual quotient adjoining an nth root of the Laurent coordinate. Eisenstein irreducibility before localization proves that it is a domain. The monic power basis gives its rank, and the invertible derivative proves etaleness.
The actual algebra adjoining an nth root of the invertible Laurent coordinate.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open Polynomial
namespace AnabelianGeometry.GeometricFundamentalGroup
universe uabbrev LaurentKummerAlgebra (K : Type u) [Field K] (n : ℕ)The Kummer polynomial stays prime on the punctured affine line.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open Polynomial
namespace AnabelianGeometry.GeometricFundamentalGroup
universe utheorem prime_laurentKummerPolynomial (K : Type u) [Field K] {n : ℕ} (hn : 0 < n) :
Prime (X ^ n - C (LaurentPolynomial.T 1 : LaurentPolynomial K))The actual Kummer quotient is an integral domain; no connectedness is assumed.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open Polynomial
namespace AnabelianGeometry.GeometricFundamentalGroup
universe utheorem isDomain_laurentKummerAlgebra (K : Type u) [Field K] {n : ℕ} (hn : 0 < n) :
IsDomain (LaurentKummerAlgebra K n)The monic power basis makes the Kummer algebra finite and free of the stated rank.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open Polynomial
namespace AnabelianGeometry.GeometricFundamentalGroup
universe utheorem finite_free_finrank_laurentKummerAlgebra (K : Type u) [Field K]
{n : ℕ} (hn : 0 < n) :
Module.Finite (LaurentPolynomial K) (LaurentKummerAlgebra K n) ∧
Module.Free (LaurentPolynomial K) (LaurentKummerAlgebra K n) ∧
Module.finrank (LaurentPolynomial K) (LaurentKummerAlgebra K n) = nIn characteristic zero every positive-degree Kummer algebra is etale.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open Polynomial
namespace AnabelianGeometry.GeometricFundamentalGroup
universe utheorem etale_laurentKummerAlgebra (K : Type u) [Field K] [CharZero K]
{n : ℕ} (hn : 0 < n) :
Algebra.Etale (LaurentPolynomial K) (LaurentKummerAlgebra K n)