Module

Finite.lean

Nyll.SchemeTheory.RingTheory.GenericFiber.Finite

2 declarations indexed from sourceView source ↗

Module documentation

Generic fibre of a finite domain extension

For a finite extension of domains C / R, extending scalars from R to a fraction field K identifies the generic fibre K ⊗[R] C with a fraction field E of C, provided the two fraction-field embeddings are compatible.

The proof regards both sides as localizations of C at the image of the non-zero elements of R. Finiteness makes C / R algebraic, so every non-zero denominator from C can be cleared by a non-zero element of R.

Imports3

Mathlib.RingTheory.Localization.BaseChange
Mathlib.RingTheory.Localization.Integral
Mathlib.RingTheory.TensorProduct.Finite

Imported by8

def

finiteGenericFiberAlgEquiv

L36 ↗

EtaleFundamentalGroups.finiteGenericFiberAlgEquiv

Documentation

The generic fibre of a finite extension of domains is its fraction field.

The equivalence is the natural product map induced by K → E and C → E. In particular, it preserves the specified embeddings rather than merely producing an abstract field equivalence.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uC uK uE

Lean source · statement

def finiteGenericFiberAlgEquiv
    {R : Type uR} {C : Type uC} {K : Type uK} {E : Type uE}
    [CommRing R] [IsDomain R]
    [CommRing C] [IsDomain C] [Algebra R C] [Module.Finite R C]
    [Field K] [Algebra R K] [IsFractionRing R K]
    [Field E] [Algebra C E] [IsFractionRing C E]
    [Algebra R E] [IsScalarTower R C E]
    [Algebra K E] [IsScalarTower R K E] :
    (K ⊗[R] C) ≃ₐ[K] E

theorem

finiteGenericFiberAlgEquiv_tmul

L119 ↗

EtaleFundamentalGroups.finiteGenericFiberAlgEquiv_tmul