NYLL
Module

EtaleAtPrimeNormality.lean

Nyll.SchemeTheory.RingTheory.Descent.EtaleAtPrimeNormality
7 declarations indexed from sourceView source ↗

Module documentation

Normality of etale algebras localized at primes

Integral elements in the generic fibre of a smooth algebra descend to the original algebra. These comparisons yield the domain and integral-closure properties of an etale algebra localized at a prime.

Imports7
  • Mathlib.RingTheory.Smooth.IntegralClosure
  • Mathlib.RingTheory.Etale.Field
  • Mathlib.RingTheory.Flat.Basic
  • Mathlib.RingTheory.Localization.Integral
  • Mathlib.RingTheory.Localization.AtPrime.Basic
  • Mathlib.Tactic.Push
  • Mathlib.RingTheory.Localization.FractionRing
Imported by10

Declarations

theorem

isIntegral_of_isIdempotentElem

L38 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Algebra_Etale_isDomain_and_isIntegrallyClosed_of_isLocalization_atPrime.EtaleLocNormalAux.isIntegral_of_isIdempotentElem
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Algebra_Etale_isDomain_and_isIntegrallyClosed_of_isLocalization_atPrime
universe u
open scoped TensorProduct
namespace EtaleLocNormalAux
Lean source · statement
theorem isIntegral_of_isIdempotentElem {T B : Type*} [CommRing T] [CommRing B] [Algebra T B]
    {e : B} (he : IsIdempotentElem e) : IsIntegral T e
theorem

tensorMap_integralClosure_mem_bot

L51 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Algebra_Etale_isDomain_and_isIntegrallyClosed_of_isLocalization_atPrime.EtaleLocNormalAux.tensorMap_integralClosure_mem_bot
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Algebra_Etale_isDomain_and_isIntegrallyClosed_of_isLocalization_atPrime
universe u
open scoped TensorProduct
namespace EtaleLocNormalAux
section Core
variable (R K : Type u) [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
  [Field K] [Algebra R K] [IsFractionRing R K]
variable (S : Type u) [CommRing S] [Algebra R S]
omit [IsDomain R] in
Lean source · statement
theorem tensorMap_integralClosure_mem_bot (y : S ⊗[R] (integralClosure R K)) :
    (Algebra.TensorProduct.map (AlgHom.id S S) (integralClosure R K).val) y
      ∈ (⊥ : Subalgebra S (S ⊗[R] K))
theorem

smooth_integrallyClosed_in_genericFibre

L72 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Algebra_Etale_isDomain_and_isIntegrallyClosed_of_isLocalization_atPrime.EtaleLocNormalAux.smooth_integrallyClosed_in_genericFibre
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Algebra_Etale_isDomain_and_isIntegrallyClosed_of_isLocalization_atPrime
universe u
open scoped TensorProduct
namespace EtaleLocNormalAux
section Core
variable (R K : Type u) [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
  [Field K] [Algebra R K] [IsFractionRing R K]
variable (S : Type u) [CommRing S] [Algebra R S]
omit [IsDomain R] in
Lean source · statement
theorem smooth_integrallyClosed_in_genericFibre [Algebra.Smooth R S] :
    integralClosure S (S ⊗[R] K) = ⊥
theorem

exists_algebraMap_eq_of_isIntegral_genericFibre

L85 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Algebra_Etale_isDomain_and_isIntegrallyClosed_of_isLocalization_atPrime.EtaleLocNormalAux.exists_algebraMap_eq_of_isIntegral_genericFibre
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Algebra_Etale_isDomain_and_isIntegrallyClosed_of_isLocalization_atPrime
universe u
open scoped TensorProduct
namespace EtaleLocNormalAux
section Core
variable (R K : Type u) [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
  [Field K] [Algebra R K] [IsFractionRing R K]
variable (S : Type u) [CommRing S] [Algebra R S]
omit [IsDomain R] in
Lean source · statement
theorem exists_algebraMap_eq_of_isIntegral_genericFibre [Algebra.Smooth R S]
    {x : S ⊗[R] K} (hx : IsIntegral S x) : ∃ s : S, algebraMap S (S ⊗[R] K) s = x
theorem

algebraMap_genericFibre_injective

L92 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Algebra_Etale_isDomain_and_isIntegrallyClosed_of_isLocalization_atPrime.EtaleLocNormalAux.algebraMap_genericFibre_injective
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Algebra_Etale_isDomain_and_isIntegrallyClosed_of_isLocalization_atPrime
universe u
open scoped TensorProduct
namespace EtaleLocNormalAux
section Core
variable (R K : Type u) [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
  [Field K] [Algebra R K] [IsFractionRing R K]
variable (S : Type u) [CommRing S] [Algebra R S]
omit [IsDomain R] [IsIntegrallyClosed R] in
Lean source · statement
theorem algebraMap_genericFibre_injective [Module.Flat R S] :
    Function.Injective (algebraMap S (S ⊗[R] K))
theorem

isIntegrallyClosed_of_integralClosure_eq_bot

L102 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Algebra_Etale_isDomain_and_isIntegrallyClosed_of_isLocalization_atPrime.EtaleLocNormalAux.isIntegrallyClosed_of_integralClosure_eq_bot
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Algebra_Etale_isDomain_and_isIntegrallyClosed_of_isLocalization_atPrime
universe u
open scoped TensorProduct
namespace EtaleLocNormalAux
Lean source · statement
theorem isIntegrallyClosed_of_integralClosure_eq_bot (T A : Type*) [CommRing T]
    [IsDomain T] [CommRing A] [IsDomain A] [Algebra T A] [FaithfulSMul T A]
    [IsIntegrallyClosed A] (h : integralClosure T A = ⊥) :
    IsIntegrallyClosed T
theorem

isDomain_and_isIntegrallyClosed_of_isLocalization_atPrime

L137 ↗
Algebra.Etale.isDomain_and_isIntegrallyClosed_of_isLocalization_atPrime
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Algebra_Etale_isDomain_and_isIntegrallyClosed_of_isLocalization_atPrime
universe u
open scoped TensorProduct
open EtaleLocNormalAux in
Lean source · statement
theorem _root_.Algebra.Etale.isDomain_and_isIntegrallyClosed_of_isLocalization_atPrime
    (P : Type u) [CommRing P] [IsDomain P] [IsIntegrallyClosed P]
    (A : Type u) [CommRing A] [Algebra P A] [Algebra.Etale P A]
    (q : Ideal A) [q.IsPrime] (A_q : Type u) [CommRing A_q]
    [Algebra A A_q] [IsLocalization.AtPrime A_q q] :
    IsDomain A_q ∧ IsIntegrallyClosed A_q

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