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.
This is not an instance because it creates a diamond with OreLocalization.instAlgebra
.
Equations
Instances For
Equations
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
.