Module

AffineLineEtaleAlgebra.lean

Nyll.AnabelianGeometry.GeometricFundamentalGroup.AffineLineEtaleAlgebra

3 declarations indexed from sourceView source ↗

Module documentation

Finite etale domains over the affine line

An etale normalization of the polynomial ring is unramified away from infinity. Riemann--Hurwitz therefore makes its fraction field trivial in characteristic zero. For a finite etale domain over the polynomial ring, this normalization is constructed from the actual generic fibre. Integral closedness then recovers the original ring.

Imports4

Imported by2

theorem

bijective_algebraMap_of_etale_polynomial_normalization

L32 ↗

AnabelianGeometry.GeometricFundamentalGroup.bijective_algebraMap_of_etale_polynomial_normalization

Documentation

In characteristic zero an etale normalization of the polynomial ring has the original rational function field.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicCurve EtaleFundamentalGroups
open scoped Polynomial TensorProduct
namespace AnabelianGeometry.GeometricFundamentalGroup
universe u

Lean source · statement

theorem bijective_algebraMap_of_etale_polynomial_normalization
    {K E : Type u} [Field K] [IsAlgClosed K] [CharZero K] [Field E]
    [Algebra K E] [Algebra (RatFunc K) E] [IsScalarTower K (RatFunc K) E]
    [Algebra K[X] E] [IsScalarTower K[X] (RatFunc K) E]
    [FiniteDimensional (RatFunc K) E]
    (hEtale : Algebra.Etale K[X] (integralClosure K[X] E)) :
    Function.Bijective (algebraMap (RatFunc K) E)

theorem

bijective_algebraMap_of_finite_etale_polynomial_fractionField

L53 ↗

AnabelianGeometry.GeometricFundamentalGroup.bijective_algebraMap_of_finite_etale_polynomial_fractionField

Documentation

Every finite etale domain over K[X], for K algebraically closed of characteristic zero, is the original polynomial ring via its given algebra map. The auxiliary field is any compatible fraction field of that domain.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicCurve EtaleFundamentalGroups
open scoped Polynomial TensorProduct
namespace AnabelianGeometry.GeometricFundamentalGroup
universe u

Lean source · statement

theorem bijective_algebraMap_of_finite_etale_polynomial_fractionField
    {K T E : Type u} [Field K] [IsAlgClosed K] [CharZero K]
    [CommRing T] [IsDomain T] [Algebra K[X] T]
    [Module.Finite K[X] T] [Algebra.Etale K[X] T]
    [Field E] [Algebra K E] [Algebra K[X] E] [Algebra T E]
    [Algebra (RatFunc K) E] [IsFractionRing T E]
    [IsScalarTower K[X] T E] [IsScalarTower K[X] (RatFunc K) E]
    [IsScalarTower K (RatFunc K) E] :
    Function.Bijective (algebraMap K[X] T)

theorem

bijective_algebraMap_of_finite_etale_polynomial

L108 ↗

AnabelianGeometry.GeometricFundamentalGroup.bijective_algebraMap_of_finite_etale_polynomial

Documentation

A finite etale domain over the polynomial ring of an algebraically closed characteristic-zero field is trivial. The fraction field and all its maps are constructed.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicCurve EtaleFundamentalGroups
open scoped Polynomial TensorProduct
namespace AnabelianGeometry.GeometricFundamentalGroup
universe u

Lean source · statement

theorem bijective_algebraMap_of_finite_etale_polynomial
    {K T : Type u} [Field K] [IsAlgClosed K] [CharZero K]
    [CommRing T] [IsDomain T] [Algebra K[X] T]
    [Module.Finite K[X] T] [Algebra.Etale K[X] T] :
    Function.Bijective (algebraMap K[X] T)

Module documentation

Finite etale domains over the affine line

Declarations

bijective_algebraMap_of_etale_polynomial_normalization

bijective_algebraMap_of_finite_etale_polynomial_fractionField

bijective_algebraMap_of_finite_etale_polynomial