# Field/algebra norm / trace and localization #

This file contains results on the combination of IsLocalization and Algebra.norm, Algebra.trace and Algebra.discr.

## Main results #

• Algebra.norm_localization: let S be an extension of R and Rₘ Sₘ be localizations at M of R S respectively. Then the norm of a : Sₘ over Rₘ is the norm of a : S over R if S is free as R-module.

• Algebra.trace_localization: let S be an extension of R and Rₘ Sₘ be localizations at M of R S respectively. Then the trace of a : Sₘ over Rₘ is the trace of a : S over R if S is free as R-module.

• Algebra.discr_localizationLocalization: let S be an extension of R and Rₘ Sₘ be localizations at M of R S respectively. Let b be a R-basis of S. Then discriminant of the Rₘ-basis of Sₘ induced by b is the discriminant of b.

## Tags #

field norm, algebra norm, localization

theorem Algebra.map_leftMulMatrix_localization (R : Type u_1) {S : Type u_2} [] [] [Algebra R S] {Rₘ : Type u_3} {Sₘ : Type u_4} [CommRing Rₘ] [Algebra R Rₘ] [CommRing Sₘ] [Algebra S Sₘ] (M : ) [] [] [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] {ι : Type u_5} [] [] (b : Basis ι R S) (a : S) :
(algebraMap R Rₘ).mapMatrix () = () ((algebraMap S Sₘ) a)
theorem Algebra.norm_localization (R : Type u_1) {S : Type u_2} [] [] [Algebra R S] {Rₘ : Type u_3} {Sₘ : Type u_4} [CommRing Rₘ] [Algebra R Rₘ] [CommRing Sₘ] [Algebra S Sₘ] (M : ) [] [] [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] [] [] (a : S) :
() ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) (() a)

Let S be an extension of R and Rₘ Sₘ be localizations at M of R S respectively. Then the norm of a : Sₘ over Rₘ is the norm of a : S over R if S is free as R-module.

theorem Algebra.norm_eq_iff (R : Type u_1) {S : Type u_2} [] [] [Algebra R S] {Rₘ : Type u_3} {Sₘ : Type u_4} [CommRing Rₘ] [Algebra R Rₘ] [CommRing Sₘ] [Algebra S Sₘ] {M : } [] [] [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] [] [] {a : S} {b : R} (hM : ) :
() a = b () ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) b

The norm of a : S in R can be computed in Sₘ.

theorem Algebra.trace_localization (R : Type u_1) {S : Type u_2} [] [] [Algebra R S] {Rₘ : Type u_3} {Sₘ : Type u_4} [CommRing Rₘ] [Algebra R Rₘ] [CommRing Sₘ] [Algebra S Sₘ] (M : ) [] [] [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] [] [] (a : S) :
(Algebra.trace Rₘ Sₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) (() a)

Let S be an extension of R and Rₘ Sₘ be localizations at M of R S respectively. Then the trace of a : Sₘ over Rₘ is the trace of a : S over R if S is free as R-module.

theorem Algebra.traceMatrix_localizationLocalization (R : Type u_1) {S : Type u_2} [] [] [Algebra R S] {Rₘ : Type u_3} [CommRing Rₘ] [Algebra R Rₘ] (M : ) [] (Sₘ : Type u_5) [CommRing Sₘ] [Algebra S Sₘ] [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] [] {ι : Type u_6} [] [] (b : Basis ι R S) :
Algebra.traceMatrix Rₘ () = (algebraMap R Rₘ).mapMatrix ()
theorem Algebra.discr_localizationLocalization (R : Type u_1) {S : Type u_2} [] [] [Algebra R S] {Rₘ : Type u_3} [CommRing Rₘ] [Algebra R Rₘ] (M : ) [] (Sₘ : Type u_5) [CommRing Sₘ] [Algebra S Sₘ] [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] [] {ι : Type u_6} [] [] (b : Basis ι R S) :
Algebra.discr Rₘ () = (algebraMap R Rₘ) ()

Let S be an extension of R and Rₘ Sₘ be localizations at M of R S respectively. Let b be a R-basis of S. Then discriminant of the Rₘ-basis of Sₘ induced by b is the discriminant of b.