Instances for Dedekind domains

This file contains various instances to work with localization of a ring extension.

A very common situation in number theory is to have an extension of (say) Dedekind domains R and S, and to prove a property of this extension it is useful to consider the localization Rₚ of R at P, a prime ideal of R. One also works with the corresponding localization Sₚ of S and the fraction fields K and L of R and S. In this situation there are many compatible algebra structures and various properties of the rings involved. Another situation is when we have a tower extension R ⊆ S ⊆ T and thus we work with Rₚ ⊆ Sₚ ⊆ Tₚ where Tₚ is the localization of T at P. This file contains a collection of such instances.

Implementation details

In general one wants all the results below for any algebra satisfying IsLocalization, but those cannot be instances (since Lean has no way of guessing the submonoid). Having the instances in the special case of the localization at a prime ideal is useful in working with Dedekind domains.

theorem algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul {A : Type u_4} (B : Type u_5) [CommSemiring A] [CommSemiring B] [Algebra A B] [NoZeroDivisors B] [FaithfulSMul A B] {S : Submonoid A} (hS : S ≤ nonZeroDivisors A) : Algebra.algebraMapSubmonoid B S ≤ nonZeroDivisors B

theorem FractionRing.isSeparable_of_isLocalization {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] (Rₘ : Type u_4) (Sₘ : Type u_5) [CommRing Rₘ] [CommRing Sₘ] [Algebra R Rₘ] [NoZeroSMulDivisors R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)] {M : Submonoid R} [IsLocalization M Rₘ] [Algebra Rₘ Sₘ] [Algebra S Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] [IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] [Algebra (FractionRing Rₘ) (FractionRing Sₘ)] [IsScalarTower Rₘ (FractionRing Rₘ) (FractionRing Sₘ)] (hM : M ≤ nonZeroDivisors R) : Algebra.IsSeparable (FractionRing Rₘ) (FractionRing Sₘ)

instance instNoZeroSMulDivisorsLocalizationAlgebraMapSubmonoidPrimeCompl {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] {P : Ideal R} [P.IsPrime] [FaithfulSMul R S] : NoZeroSMulDivisors S (Localization (Algebra.algebraMapSubmonoid S P.primeCompl))

instance instNoZeroSMulDivisorsLocalizationAlgebraMapSubmonoidPrimeCompl_1 {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] {P : Ideal R} [P.IsPrime] [FaithfulSMul R S] : NoZeroSMulDivisors R (Localization (Algebra.algebraMapSubmonoid S P.primeCompl))

@[reducible, inline]

noncomputable abbrev Localization.AtPrime.liftAlgebra {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] {P : Ideal R} [P.IsPrime] [FaithfulSMul R S] : Algebra (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) (FractionRing S)

This is not an instance because it creates a diamond with OreLocalization.instAlgebra.

Equations

• Localization.AtPrime.liftAlgebra S = (IsLocalization.map (FractionRing S) (RingHom.id S) ⋯).toAlgebra

instance instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeComplFractionRing {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] {P : Ideal R} [P.IsPrime] [FaithfulSMul R S] : IsScalarTower S (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) (FractionRing S)

instance instIsFractionRingAtPrimeFractionRing {R : Type u_1} [CommRing R] [IsDomain R] {P : Ideal R} [P.IsPrime] : IsFractionRing (Localization.AtPrime P) (FractionRing R)

instance instIsFractionRingLocalizationAlgebraMapSubmonoidPrimeComplFractionRing {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] {P : Ideal R} [P.IsPrime] [FaithfulSMul R S] : IsFractionRing (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) (FractionRing S)

noncomputable instance instAlgebraAtPrimeFractionRing {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [IsDomain S] [Algebra R S] {P : Ideal R} [P.IsPrime] [FaithfulSMul R S] : Algebra (Localization.AtPrime P) (FractionRing S)

Equations

• instAlgebraAtPrimeFractionRing S = (IsLocalization.lift ⋯).toAlgebra

instance instIsScalarTowerAtPrimeFractionRing {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] {P : Ideal R} [P.IsPrime] [FaithfulSMul R S] : IsScalarTower (Localization.AtPrime P) (FractionRing R) (FractionRing S)

instance instIsScalarTowerAtPrimeFractionRing_1 {R : Type u_1} [CommRing R] [IsDomain R] {P : Ideal R} [P.IsPrime] : IsScalarTower R (Localization.AtPrime P) (FractionRing R)

instance instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeComplFractionRing {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] {P : Ideal R} [P.IsPrime] [FaithfulSMul R S] : IsScalarTower (Localization.AtPrime P) (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) (FractionRing S)

instance instIsDedekindDomainLocalizationAlgebraMapSubmonoidPrimeCompl {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] {P : Ideal R} [P.IsPrime] [FaithfulSMul R S] [IsDedekindDomain S] : IsDedekindDomain (Localization (Algebra.algebraMapSubmonoid S P.primeCompl))

instance instIsPrincipalIdealRingLocalizationAlgebraMapSubmonoidPrimeComplOfIsDedekindDomainOfFiniteOfNeZeroIdeal {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] {P : Ideal R} [P.IsPrime] [FaithfulSMul R S] [IsDedekindDomain R] [IsDedekindDomain S] [Module.Finite R S] [hP : NeZero P] : IsPrincipalIdealRing (Localization (Algebra.algebraMapSubmonoid S P.primeCompl))

instance instIsSeparableFractionRingAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl {R : Type u_1} (S : Type u_2) [CommRing R] [CommRing S] [IsDomain R] [IsDomain S] [Algebra R S] {P : Ideal R} [P.IsPrime] [FaithfulSMul R S] [Algebra.IsSeparable (FractionRing R) (FractionRing S)] : Algebra.IsSeparable (FractionRing (Localization.AtPrime P)) (FractionRing (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)))

instance instIsLocalizationAlgebraMapSubmonoidPrimeComplLocalization {R : Type u_1} (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] {P : Ideal R} [P.IsPrime] [Algebra S T] [Algebra R T] [IsScalarTower R S T] : IsLocalization (Algebra.algebraMapSubmonoid T (Algebra.algebraMapSubmonoid S P.primeCompl)) (Localization (Algebra.algebraMapSubmonoid T P.primeCompl))

@[reducible, inline]

noncomputable abbrev Localization.AtPrime.algebra_localization_localization {R : Type u_1} (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] {P : Ideal R} [P.IsPrime] [Algebra S T] [Algebra R T] [IsScalarTower R S T] : Algebra (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) (Localization (Algebra.algebraMapSubmonoid T P.primeCompl))

Let R ⊆ S ⊆ T be a tower of rings. Let Sₚ and Tₚ denote the localizations of S and T at the prime ideal P of R. Then Tₚ is a Sₚ-algebra. This cannot be an instance since it creates a diamond when S = T.

Equations

• Localization.AtPrime.algebra_localization_localization S T = localizationAlgebra (Algebra.algebraMapSubmonoid S P.primeCompl) T

instance instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl {R : Type u_1} (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] {P : Ideal R} [P.IsPrime] [Algebra S T] [Algebra R T] [IsScalarTower R S T] : IsScalarTower S (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) (Localization (Algebra.algebraMapSubmonoid T P.primeCompl))

instance instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl_1 {R : Type u_1} (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] {P : Ideal R} [P.IsPrime] [Algebra S T] [Algebra R T] [IsScalarTower R S T] : IsScalarTower R (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) (Localization (Algebra.algebraMapSubmonoid T P.primeCompl))

instance instFiniteLocalizationAlgebraMapSubmonoidPrimeCompl {R : Type u_1} (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [CommRing T] [Algebra R S] {P : Ideal R} [P.IsPrime] [Algebra S T] [Algebra R T] [IsScalarTower R S T] [Module.Finite S T] : Module.Finite (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) (Localization (Algebra.algebraMapSubmonoid T P.primeCompl))

instance instNoZeroSMulDivisorsLocalizationAlgebraMapSubmonoidPrimeCompl_2 {R : Type u_1} (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [CommRing T] [IsDomain R] [IsDomain S] [IsDomain T] [Algebra R S] {P : Ideal R} [P.IsPrime] [FaithfulSMul R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T] [NoZeroSMulDivisors S T] : NoZeroSMulDivisors (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) (Localization (Algebra.algebraMapSubmonoid T P.primeCompl))

instance instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl {R : Type u_1} (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [CommRing T] [IsDomain R] [IsDomain T] [Algebra R S] {P : Ideal R} [P.IsPrime] [Algebra S T] [Algebra R T] [IsScalarTower R S T] [NoZeroSMulDivisors R T] : IsScalarTower (Localization.AtPrime P) (Localization (Algebra.algebraMapSubmonoid S P.primeCompl)) (Localization (Algebra.algebraMapSubmonoid T P.primeCompl))

instance instIsSeparableFractionRingLocalizationAlgebraMapSubmonoidPrimeCompl {R : Type u_1} (S : Type u_2) (T : Type u_3) [CommRing R] [CommRing S] [CommRing T] [IsDomain R] [IsDomain S] [IsDomain T] [Algebra R S] {P : Ideal R} [P.IsPrime] [FaithfulSMul R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T] [NoZeroSMulDivisors R T] [NoZeroSMulDivisors S T] [Algebra.IsSeparable (FractionRing S) (FractionRing T)] : Algebra.IsSeparable (FractionRing (Localization (Algebra.algebraMapSubmonoid S P.primeCompl))) (FractionRing (Localization (Algebra.algebraMapSubmonoid T P.primeCompl)))