Module

GenericFiber.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.BaseChange.GenericFiber

8 declarations indexed from sourceView source ↗

Module documentation

Selected generic components after finite-etale base change

This file packages the generic-fibre bookkeeping needed after a finite-etale base change. The generic fibre of B ⊗[A] T over a fraction field K of B is canonically K ⊗[A] T. A surjective map from that tensor product to a field selects a maximal component by its kernel. The normalization of the selected field is finite etale over B.

The final theorem specializes the target field to an actual compositum in a fixed ambient field, using the product-map API from ClassFieldTheory.

Imports3

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.Compositum
Mathlib.RingTheory.TensorProduct.Finite
Nyll.EtaleFundamentalGroups.FiniteEtale.GenericFiber.Component

Imported by6

def

baseChangeGenericFiberEquiv

L36 ↗

EtaleFundamentalGroups.baseChangeGenericFiberEquiv

Documentation

Reassociate the generic fibre of a base-changed algebra: (B ⊗[A] T) ⊗[B] K ≃ K ⊗[A] T.

The source uses the right K-algebra structure.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uA uB uT uK uF uE uΩ

Lean source · full declaration

def baseChangeGenericFiberEquiv
    (A : Type uA) (B : Type uB) (T : Type uT) (K : Type uK)
    [CommRing A] [CommRing B] [CommRing T] [CommRing K]
    [Algebra A B] [Algebra A T] [Algebra B K]
    [Algebra A K] [IsScalarTower A B K] :
    letI : Algebra K ((B ⊗[A] T) ⊗[B] K) :=
      Algebra.TensorProduct.rightAlgebra
    ((B ⊗[A] T) ⊗[B] K) ≃ₐ[K] (K ⊗[A] T) := by
  letI : Algebra K ((B ⊗[A] T) ⊗[B] K) :=
    Algebra.TensorProduct.rightAlgebra
  exact
    (Algebra.TensorProduct.commRight B K (B ⊗[A] T)).symm.trans
      (Algebra.TensorProduct.cancelBaseChange A B K K T)

def

iteratedGenericFiberEquiv

L53 ↗

EtaleFundamentalGroups.iteratedGenericFiberEquiv

Documentation

If the generic fibre of T / A is identified with E / F, extending the fraction field from F to K identifies K ⊗[A] T with K ⊗[F] E.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uA uB uT uK uF uE uΩ

Lean source · statement

def iteratedGenericFiberEquiv
    (A : Type uA) (F : Type uF) (K : Type uK)
    (T : Type uT) (E : Type uE)
    [CommRing A] [CommRing F] [CommRing K] [CommRing T] [CommRing E]
    [Algebra A F] [Algebra A K] [Algebra F K] [IsScalarTower A F K]
    [Algebra A T] [Algebra F E]
    (e : (F ⊗[A] T) ≃ₐ[F] E) :
    (K ⊗[A] T) ≃ₐ[K] (K ⊗[F] E)

abbrev

selectedGenericFiberIdeal

L65 ↗

EtaleFundamentalGroups.selectedGenericFiberIdeal

Documentation

The kernel of a map from a generic fibre to a specified field.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uA uB uT uK uF uE uΩ

Lean source · statement

abbrev selectedGenericFiberIdeal
    {R : Type uA} {T : Type uT} {K : Type uK} {Ω : Type uΩ}
    [CommRing R] [CommRing T] [Algebra R T]
    [CommRing K] [Algebra R K]
    [CommRing Ω] [Algebra R Ω]
    (f : (T ⊗[R] K) →ₐ[R] Ω) : Ideal (T ⊗[R] K)

theorem

selectedGenericFiberIdeal_isMaximal

L74 ↗

EtaleFundamentalGroups.selectedGenericFiberIdeal_isMaximal

Documentation

A surjective generic-fibre map to a field selects a maximal ideal.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uA uB uT uK uF uE uΩ

Lean source · statement

theorem selectedGenericFiberIdeal_isMaximal
    {R : Type uA} {T : Type uT} {K : Type uK} {Ω : Type uΩ}
    [CommRing R] [CommRing T] [Algebra R T]
    [CommRing K] [Algebra R K]
    [Field Ω] [Algebra R Ω]
    (f : (T ⊗[R] K) →ₐ[R] Ω) (hf : Function.Surjective f) :
    (selectedGenericFiberIdeal f).IsMaximal

def

selectedGenericFiberComponentEquiv

L85 ↗

EtaleFundamentalGroups.selectedGenericFiberComponentEquiv

Documentation

The component selected by a surjective generic-fibre map is the target field itself.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uA uB uT uK uF uE uΩ

Lean source · statement

def selectedGenericFiberComponentEquiv
    {R : Type uA} {T : Type uT} {K : Type uK} {Ω : Type uΩ}
    [CommRing R] [CommRing T] [Algebra R T]
    [CommRing K] [Algebra R K]
    [Field Ω] [Algebra R Ω]
    (f : (T ⊗[R] K) →ₐ[R] Ω) (hf : Function.Surjective f) :
    ((T ⊗[R] K) ⧸ selectedGenericFiberIdeal f) ≃ₐ[R] Ω

theorem

integralClosure_etale_of_surjective_genericFiber

L97 ↗

EtaleFundamentalGroups.integralClosure_etale_of_surjective_genericFiber

Documentation

A specified field quotient of the generic fibre of a finite-etale algebra has finite-etale normalization over a normal base.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uA uB uT uK uF uE uΩ

Lean source · statement

theorem integralClosure_etale_of_surjective_genericFiber
    {R : Type uA} {T : Type uT} {K : Type uK} {Ω : Type uΩ}
    [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    [CommRing T] [Algebra R T] [Module.Finite R T] [Algebra.Etale R T]
    [Field K] [Algebra R K] [IsFractionRing R K]
    [Field Ω] [Algebra R Ω]
    (f : (T ⊗[R] K) →ₐ[R] Ω) (hf : Function.Surjective f) :
    Algebra.Etale R (integralClosure R Ω)

theorem

integralClosure_etale_of_surjective_reassociatedGenericFiber

L120 ↗

EtaleFundamentalGroups.integralClosure_etale_of_surjective_reassociatedGenericFiber

Documentation

Reassociated form of integralClosure_etale_of_surjective_genericFiber.

It is enough to give a surjective K-algebra map K ⊗[A] T → Ω; the finite-etale algebra over B and its generic component are constructed in the proof.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uA uB uT uK uF uE uΩ

Lean source · statement

theorem integralClosure_etale_of_surjective_reassociatedGenericFiber
    {A : Type uA} {B : Type uB} {T : Type uT}
    {K : Type uK} {Ω : Type uΩ}
    [CommRing A] [CommRing B] [Algebra A B]
    [CommRing T] [Algebra A T] [Module.Finite A T] [Algebra.Etale A T]
    [IsDomain B] [IsIntegrallyClosed B]
    [Field K] [Algebra B K] [IsFractionRing B K]
    [Algebra A K] [IsScalarTower A B K]
    [Field Ω] [Algebra K Ω] [Algebra B Ω] [IsScalarTower B K Ω]
    (f : (K ⊗[A] T) →ₐ[K] Ω) (hf : Function.Surjective f) :
    Algebra.Etale B (integralClosure B Ω)

theorem

integralClosure_compositum_etale_of_finiteEtale_baseChange

L154 ↗

EtaleFundamentalGroups.integralClosure_compositum_etale_of_finiteEtale_baseChange

Documentation

Actual-compositum endpoint.

Assume the generic fibre F ⊗[A] T is a field E inside a common ambient field and that K' is the fraction field of the new normal base B. Then the integral closure of B in the actual compositum E ⊔ K' is finite etale over B.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uA uB uT uK uF uE uΩ
open DiscreteValuationField.FieldCompositum

Lean source · full declaration

theorem integralClosure_compositum_etale_of_finiteEtale_baseChange
    {A : Type uA} {B : Type uB} {T : Type uT}
    {F : Type uF} {Ω : Type uΩ}
    [CommRing A] [CommRing B] [Algebra A B]
    [CommRing T] [Algebra A T] [Module.Finite A T] [Algebra.Etale A T]
    [IsDomain B] [IsIntegrallyClosed B]
    [Field F] [Algebra A F]
    [Field Ω] [Algebra F Ω]
    (E K' : IntermediateField F Ω)
    [Algebra B K'] [IsFractionRing B K']
    [Algebra A K'] [IsScalarTower A B K'] [IsScalarTower A F K']
    [FiniteDimensional F E]
    (eGeneric : (F ⊗[A] T) ≃ₐ[F] E) :
    let M := E ⊔ K'
    letI : Algebra B M :=
      ((algebraMap K' M).comp (algebraMap B K')).toAlgebra
    Algebra.Etale B (integralClosure B M) := by
  let M := E ⊔ K'
  let : Algebra B M :=
    ((algebraMap K' M).comp (algebraMap B K')).toAlgebra
  let : IsScalarTower B K' M := IsScalarTower.of_algebraMap_eq' rfl
  let eFactor : (K' ⊗[A] T) ≃ₐ[K'] (K' ⊗[F] E) :=
    iteratedGenericFiberEquiv A F K' T E eGeneric
  let product : (K' ⊗[F] E) →ₐ[K'] M :=
    supFlipProductMapRightAlgHom E K'
  let f : (K' ⊗[A] T) →ₐ[K'] M := product.comp eFactor.toAlgHom
  apply integralClosure_etale_of_surjective_reassociatedGenericFiber
    (A := A) (B := B) (T := T) (K := K') f
  exact (supFlipProductMapRightAlgHom_surjective E K').comp
    eFactor.surjective

Module documentation

Selected generic components after finite-etale base change

Declarations