Algebra.discr_localizationLocalization
theorem Algebra.discr_localizationLocalization :
∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {Rₘ : Type u_3}
[inst_3 : CommRing Rₘ] [inst_4 : Algebra R Rₘ] (M : Submonoid R) [inst_5 : IsLocalization M Rₘ] (Sₘ : Type u_5)
[inst_6 : CommRing Sₘ] [inst_7 : Algebra S Sₘ] [inst_8 : Algebra Rₘ Sₘ] [inst_9 : Algebra R Sₘ]
[inst_10 : IsScalarTower R Rₘ Sₘ] [inst_11 : IsScalarTower R S Sₘ]
[inst_12 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] {ι : Type u_6} [inst_13 : Fintype ι]
[inst_14 : DecidableEq ι] (b : Basis ι R S),
Algebra.discr Rₘ ⇑(Basis.localizationLocalization Rₘ M Sₘ b) = (algebraMap R Rₘ) (Algebra.discr R ⇑b)
This theorem states that for a given extension `S` of `R` and localizations `Rₘ` and `Sₘ` at `M` of `R` and `S` respectively, and a given `R`-basis `b` of `S`, the discriminant of the `Rₘ`-basis of `Sₘ` induced by `b` is equal to the discriminant of `b` mapped from `R` to `Rₘ`. In other words, the discriminant of the basis after localization is the same as the discriminant of the original basis, after mapping it to the localization. This can be understood as a property of how a basis behaves under localization in the context of ring extensions.
More concisely: The discriminant of an `R`-basis `b` of an extension `S` of `R` remains unchanged when passing to the discriminant of the basis induced by `b` in the localizations `Rₘ` and `Sₘ` at a common multiplicative set `M`.
|
Algebra.trace_localization
theorem Algebra.trace_localization :
∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {Rₘ : Type u_3}
{Sₘ : Type u_4} [inst_3 : CommRing Rₘ] [inst_4 : Algebra R Rₘ] [inst_5 : CommRing Sₘ] [inst_6 : Algebra S Sₘ]
(M : Submonoid R) [inst_7 : IsLocalization M Rₘ] [inst_8 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ]
[inst_9 : Algebra Rₘ Sₘ] [inst_10 : Algebra R Sₘ] [inst_11 : IsScalarTower R Rₘ Sₘ]
[inst_12 : IsScalarTower R S Sₘ] [inst_13 : Module.Free R S] [inst_14 : Module.Finite R S] (a : S),
(Algebra.trace Rₘ Sₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((Algebra.trace R S) a)
In the context of commutative ring theory, the theorem `Algebra.trace_localization` states that given a ring `R` and its extension `S`, and localizations `Rₘ`, `Sₘ` at a submonoid `M` of `R` and `S` respectively, the trace of an element `a` of `Sₘ` over `Rₘ` is equal to the trace of the same element `a` of `S` over `R`, mapped through the respective algebraic structures, under the condition that the ring `S` is a free `R`-module. Here, the trace refers to the trace of `(s * ·)`, as an `R`-linear map. This condition ensures the existence of a basis for `S` over `R`, facilitating the trace calculation. The theorem establishes a relationship between traces in the original rings and their localized versions.
More concisely: Given a free commutative `R`-algebra `S` over a commutative ring `R`, and localizations `Rₘ` and `Sₘ` of `R` and `S` respectively at a submonoid `M`, the trace of an element `a` in `Sₘ` over `Rₘ` equals the trace of `a` in `S` over `R`.
|
Algebra.norm_localization
theorem Algebra.norm_localization :
∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {Rₘ : Type u_3}
{Sₘ : Type u_4} [inst_3 : CommRing Rₘ] [inst_4 : Algebra R Rₘ] [inst_5 : CommRing Sₘ] [inst_6 : Algebra S Sₘ]
(M : Submonoid R) [inst_7 : IsLocalization M Rₘ] [inst_8 : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ]
[inst_9 : Algebra Rₘ Sₘ] [inst_10 : Algebra R Sₘ] [inst_11 : IsScalarTower R Rₘ Sₘ]
[inst_12 : IsScalarTower R S Sₘ] [inst_13 : Module.Free R S] [inst_14 : Module.Finite R S] (a : S),
(Algebra.norm Rₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((Algebra.norm R) a)
This theorem states that let `S` be an extension of a commutative ring `R`, and `Rₘ` and `Sₘ` be localizations of `R` and `S` respectively at a submonoid `M` of `R`. Then, for a given element `a` from `S`, if `S` is a free and finite `R`-module, the norm of `a` computed in the localization `Sₘ` over `Rₘ` is equal to the image under the localization map of the norm of `a` computed in `S` over `R`. Here, the norm of an element of an `R`-algebra is defined as the determinant of the linear map given by multiplication by that element.
More concisely: Let `R` be a commutative ring, `S` an extension of `R`, `M` a submonoid of `R`, and `a` an element of `S` with `S` a free and finite `R`-module. The norm of `a` in the localization `Sₘ` of `S` at `M` equals the norm of its localization in `S` multiplied by the determinant of the localization map from `R` to `S`.
|