# Documentation

Mathlib.RingTheory.Localization.NormTrace

# 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) :
↑(RingHom.mapMatrix (algebraMap R Rₘ)) (↑() a) = ↑() (↑(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.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) :
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.