Module

FractionField.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.GenericFiber.FractionField

4 declarations indexed from sourceView source ↗

Module documentation

Fraction fields of finite-etale domains

Let T / R be a finite-etale extension of domains, let K be a fraction field of R, and let L be a fraction field of T. Compatible maps from K and T to L induce a surjection T ⊗[R] K ⟶ L. Consequently the integral closure of R in L is finite etale over R when R is normal.

The last assertion does not assume that T is normal. It follows by selecting the field component L of the generic fibre and using the finite-etale normalization theorem for that component.

Imports1

Nyll.EtaleFundamentalGroups.FiniteEtale.GenericFiber.Component

Imported by4

def

finiteEtaleGenericFiberToFractionField

L38 ↗

EtaleFundamentalGroups.finiteEtaleGenericFiberToFractionField

Documentation

The canonical map from the generic fibre of T / R to a compatible fraction field of T.

Source context 9 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uT uK uL
variable {R : Type uR} {T : Type uT} {K : Type uK} {L : Type uL}
variable [CommRing R] [CommRing T] [Algebra R T]
variable [Field K] [Algebra R K]
variable [Field L] [Algebra R L] [Algebra T L] [Algebra K L]
variable [IsScalarTower R T L] [IsScalarTower R K L]

Lean source · statement

def finiteEtaleGenericFiberToFractionField :
    (T ⊗[R] K) →ₐ[R] L

theorem

finiteEtaleGenericFiberToFractionField_tmul

L46 ↗

EtaleFundamentalGroups.finiteEtaleGenericFiberToFractionField_tmul

Source context 9 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uT uK uL
variable {R : Type uR} {T : Type uT} {K : Type uK} {L : Type uL}
variable [CommRing R] [CommRing T] [Algebra R T]
variable [Field K] [Algebra R K]
variable [Field L] [Algebra R L] [Algebra T L] [Algebra K L]
variable [IsScalarTower R T L] [IsScalarTower R K L]

Lean source · statement

theorem finiteEtaleGenericFiberToFractionField_tmul (x : T) (y : K) :
    finiteEtaleGenericFiberToFractionField (R := R) (T := T) (K := K) (L := L)
        (x ⊗ₜ[R] y) =
      algebraMap T L x * algebraMap K L y

theorem

finiteEtaleGenericFiberToFractionField_surjective

L54 ↗

EtaleFundamentalGroups.finiteEtaleGenericFiberToFractionField_surjective

Documentation

If K and L are fraction fields of R and T, respectively, the canonical generic-fibre map T ⊗[R] K ⟶ L is surjective.

Source context 9 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uT uK uL
variable {R : Type uR} {T : Type uT} {K : Type uK} {L : Type uL}
variable [CommRing R] [CommRing T] [Algebra R T]
variable [Field K] [Algebra R K]
variable [Field L] [Algebra R L] [Algebra T L] [Algebra K L]
variable [IsScalarTower R T L] [IsScalarTower R K L]

Lean source · statement

theorem finiteEtaleGenericFiberToFractionField_surjective
    [IsDomain R] [IsDomain T]
    [Module.Finite R T] [Algebra.Etale R T]
    [IsFractionRing R K] [IsFractionRing T L] :
    Function.Surjective
      (finiteEtaleGenericFiberToFractionField
        (R := R) (T := T) (K := K) (L := L))

theorem

integralClosure_etale_of_finiteEtale_fractionField

L114 ↗

EtaleFundamentalGroups.integralClosure_etale_of_finiteEtale_fractionField

Documentation

The normalization of a normal domain R in the fraction field of a finite-etale R-domain is finite etale over R.

No normality hypothesis on T is needed: L is selected directly as a field quotient of the generic fibre T ⊗[R] K.

Source context 9 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uT uK uL
variable {R : Type uR} {T : Type uT} {K : Type uK} {L : Type uL}
variable [CommRing R] [CommRing T] [Algebra R T]
variable [Field K] [Algebra R K]
variable [Field L] [Algebra R L] [Algebra T L] [Algebra K L]
variable [IsScalarTower R T L] [IsScalarTower R K L]

Lean source · statement

theorem integralClosure_etale_of_finiteEtale_fractionField
    [IsDomain R] [IsIntegrallyClosed R]
    [IsDomain T] [Module.Finite R T] [Algebra.Etale R T]
    [IsFractionRing R K] [IsFractionRing T L] :
    Algebra.Etale R (integralClosure R L)

Module documentation

Fraction fields of finite-etale domains

Declarations

finiteEtaleGenericFiberToFractionField

finiteEtaleGenericFiberToFractionField_tmul

finiteEtaleGenericFiberToFractionField_surjective

integralClosure_etale_of_finiteEtale_fractionField