Module

SmoothIntegralClosure.lean

Nyll.SchemeTheory.Normalization.GenericFiber.SmoothIntegralClosure

2 declarations indexed from sourceView source ↗

Module documentation

Integral elements in a smooth generic fibre

Let R be a normal domain with fraction field K, and let S / R be smooth. Every element of S ⊗[R] K which is integral over S already comes from S.

This is the elementwise form of smooth base change for integral closure. It is useful for finite-etale generic fibres: primitive idempotents and elements supported on a selected field component are integral, hence descend to the original finite-etale algebra.

Imports1

Mathlib.RingTheory.Smooth.IntegralClosure

Imported by3

theorem

tensorProduct_integralClosure_eq_tmul_one

L30 ↗

EtaleFundamentalGroups.tensorProduct_integralClosure_eq_tmul_one

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uS uK

Lean source · statement

theorem tensorProduct_integralClosure_eq_tmul_one
    {R : Type uR} {S : Type uS} {K : Type uK}
    [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    [CommRing S] [Algebra R S]
    [Field K] [Algebra R K] [IsFractionRing R K]
    (z : S ⊗[R] integralClosure R K) :
    ∃ s : S, z = s ⊗ₜ[R] (1 : integralClosure R K)

theorem

exists_eq_includeLeft_of_isIntegral_genericFiber_of_smooth

L60 ↗

EtaleFundamentalGroups.exists_eq_includeLeft_of_isIntegral_genericFiber_of_smooth

Documentation

If S / R is smooth and R is normal, every S-integral element of the generic fibre S ⊗[R] K is the image of an element of S.

The preimage is produced by the smooth integral-closure comparison; no normality or component hypothesis on S is assumed.