Module

SmoothAtPrimeNormality.lean

Nyll.SchemeTheory.RingTheory.Descent.SmoothAtPrimeNormality

2 declarations indexed from sourceView source ↗

Module documentation

Normality of smooth algebras localized at primes

A smooth algebra localized at a prime over an integrally closed domain is a domain and is integrally closed. The proof first treats polynomial algebras and then the etale local presentation.

Imports5

Nyll.SchemeTheory.RingTheory.Descent.EtaleAtPrimeNormality
Mathlib.Util.WithWeakNamespace
Mathlib.RingTheory.Polynomial.IsIntegral
Mathlib.RingTheory.RingHom.StandardSmooth
Mathlib.RingTheory.Smooth.StandardSmoothOfFree

Imported by3

theorem

isIntegrallyClosed_mvPolynomial_fin

L35 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Algebra_Smooth_isDomain_and_isIntegrallyClosed_of_isIntegrallyClosed_of_isLocalization_atPrime.isIntegrallyClosed_mvPolynomial_fin

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace
  Algebra_Smooth_isDomain_and_isIntegrallyClosed_of_isIntegrallyClosed_of_isLocalization_atPrime
universe u

Lean source · full declaration

theorem isIntegrallyClosed_mvPolynomial_fin (R : Type u) [CommRing R]
    [IsDomain R] [IsIntegrallyClosed R] :
    ∀ n : ℕ, IsIntegrallyClosed (MvPolynomial (Fin n) R)
  | 0 => IsIntegrallyClosed.of_equiv (MvPolynomial.isEmptyAlgEquiv R (Fin 0)).symm.toRingEquiv
  | n + 1 => by
      have := isIntegrallyClosed_mvPolynomial_fin R n
      exact IsIntegrallyClosed.of_equiv (MvPolynomial.finSuccEquiv R n).symm.toRingEquiv

theorem

isDomain_and_isIntegrallyClosed_of_isIntegrallyClosed_of_isLocalization_atPrime

L47 ↗

Algebra.Smooth.isDomain_and_isIntegrallyClosed_of_isIntegrallyClosed_of_isLocalization_atPrime

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace
  Algebra_Smooth_isDomain_and_isIntegrallyClosed_of_isIntegrallyClosed_of_isLocalization_atPrime
universe u
with_weak_namespace _root_.AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
open
  Algebra_Smooth_isDomain_and_isIntegrallyClosed_of_isIntegrallyClosed_of_isLocalization_atPrime in
with_weak_namespace _root_.Algebra.Smooth

Lean source · statement

theorem isDomain_and_isIntegrallyClosed_of_isIntegrallyClosed_of_isLocalization_atPrime
    (R : Type u) [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    (S : Type u) [CommRing S] [Algebra R S] [Algebra.Smooth R S]
    (p : Ideal S) [p.IsPrime] (Sₚ : Type u) [CommRing Sₚ]
    [Algebra S Sₚ] [IsLocalization.AtPrime Sₚ p] :
    IsDomain Sₚ ∧ IsIntegrallyClosed Sₚ

Module documentation

Normality of smooth algebras localized at primes

Declarations

isIntegrallyClosed_mvPolynomial_fin

isDomain_and_isIntegrallyClosed_of_isIntegrallyClosed_of_isLocalization_atPrime