NYLL
Module

IntegralClosureEtaleOfSplit.lean

Nyll.SchemeTheory.RingTheory.IntegralClosureEtaleOfSplit
3 declarations indexed from sourceView source ↗

Module documentation

Étale normalization after an actual generic splitting

A splitting over a pointed étale neighborhood gives a split product in a localization by non-zero-divisors. Local normality of that étale neighborhood shows it is integrally closed in that localization. Smooth base change of integral closure and the explicit split-product normalization therefore make the original integral closure étale after faithfully flat base change. Étale descent gives the conclusion over the original normal domain.

Imports9
Imported by3

Declarations

theorem

integralClosure_etale_of_split_localization_after_faithfullyFlat_etale

L39 ↗
SchemeTheory.integralClosure_etale_of_split_localization_after_faithfullyFlat_etale
Documentation

A splitting in a genuine localization by non-zero-divisors on a faithfully flat étale neighborhood makes the original integral closure étale.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct nonZeroDivisors
namespace SchemeTheory
universe u v
Lean source · statement
theorem integralClosure_etale_of_split_localization_after_faithfullyFlat_etale
    (R S B T : Type u) (ι : Type v)
    [CommRing R] [CommRing S] [CommRing B] [CommRing T]
    [IsDomain R] [IsIntegrallyClosed R]
    [Algebra R S] [Algebra R B] [Algebra S T]
    [Algebra.Etale R S] [Module.FaithfullyFlat R S] [Finite ι]
    (M : Submonoid S) (hM : M ≤ S⁰) [IsLocalization M T]
    (e : (S ⊗[R] B) ≃ₐ[S] (ι → T)) :
    Algebra.Etale R (integralClosure R B)
theorem

integralClosure_etale_of_split_after_faithfullyFlat_etale

L64 ↗
SchemeTheory.integralClosure_etale_of_split_after_faithfullyFlat_etale
Documentation

A generic splitting on a faithfully flat étale neighborhood forces the actual integral closure to be étale over the original normal domain.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct nonZeroDivisors
namespace SchemeTheory
universe u v
Lean source · statement
theorem integralClosure_etale_of_split_after_faithfullyFlat_etale
    (R S B T : Type u) (ι : Type v)
    [CommRing R] [CommRing S] [CommRing B] [CommRing T]
    [IsDomain R] [IsIntegrallyClosed R]
    [Algebra R S] [Algebra R B] [Algebra S T]
    [Algebra.Etale R S] [Module.FaithfullyFlat R S] [Finite ι]
    (d : R) (hd : d ≠ 0) [IsLocalization.Away (algebraMap R S d) T]
    (e : (S ⊗[R] B) ≃ₐ[S] (ι → T)) :
    Algebra.Etale R (integralClosure R B)
theorem

integralClosure_etale_of_generic_split_after_faithfullyFlat_etale

L88 ↗
SchemeTheory.integralClosure_etale_of_generic_split_after_faithfullyFlat_etale
Documentation

The actual generic-fiber splitting on a faithfully flat étale neighborhood implies étaleness of normalization over an arbitrary integrally closed domain. The generic tensor is its canonical localization; flatness supplies regular images of every original denominator.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct nonZeroDivisors
namespace SchemeTheory
universe u v
Lean source · statement
theorem integralClosure_etale_of_generic_split_after_faithfullyFlat_etale
    (R S B : Type u) (ι : Type v)
    [CommRing R] [CommRing S] [CommRing B] [IsDomain R] [IsIntegrallyClosed R]
    [Algebra R S] [Algebra R B]
    [Algebra.Etale R S] [Module.FaithfullyFlat R S] [Finite ι]
    (e : (S ⊗[R] B) ≃ₐ[S] (ι → (S ⊗[R] FractionRing R))) :
    Algebra.Etale R (integralClosure R B)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.