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. 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_3} (B : Type u_4) [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_3) (Sₘ : Type u_4) [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ₘ)

noncomputable instance instAlgebraLocalizationAlgebraMapSubmonoidPrimeComplFractionRing {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)

Equations

• instAlgebraLocalizationAlgebraMapSubmonoidPrimeComplFractionRing 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)))