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} [CommRing R] [CommRing S] [Algebra R S] {Rₘ : Type u_3} {Sₘ : Type u_4} [CommRing Rₘ] [Algebra R Rₘ] [CommRing Sₘ] [Algebra S Sₘ] (M : Submonoid R) [IsLocalization M Rₘ] [IsLocalization (algebraMapSubmonoid S M) Sₘ] [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] {ι : Type u_5} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι R S) (a : S) : (algebraMap R Rₘ).mapMatrix ((leftMulMatrix b) a) = (leftMulMatrix (Module.Basis.localizationLocalization Rₘ M Sₘ b)) ((algebraMap S Sₘ) a)

theorem Algebra.norm_localization (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {Rₘ : Type u_3} {Sₘ : Type u_4} [CommRing Rₘ] [Algebra R Rₘ] [CommRing Sₘ] [Algebra S Sₘ] (M : Submonoid R) [IsLocalization M Rₘ] [IsLocalization (algebraMapSubmonoid S M) Sₘ] [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] [Module.Free R S] [Module.Finite R S] (a : S) : (norm Rₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((norm 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} [CommRing R] [CommRing S] [Algebra R S] {Rₘ : Type u_3} {Sₘ : Type u_4} [CommRing Rₘ] [Algebra R Rₘ] [CommRing Sₘ] [Algebra S Sₘ] {M : Submonoid R} [IsLocalization M Rₘ] [IsLocalization (algebraMapSubmonoid S M) Sₘ] [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] [Module.Free R S] [Module.Finite R S] {a : S} {b : R} (hM : M ≤ nonZeroDivisors R) : (norm R) a = b ↔ (norm Rₘ) ((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} [CommRing R] [CommRing S] [Algebra R S] {Rₘ : Type u_3} {Sₘ : Type u_4} [CommRing Rₘ] [Algebra R Rₘ] [CommRing Sₘ] [Algebra S Sₘ] (M : Submonoid R) [IsLocalization M Rₘ] [IsLocalization (algebraMapSubmonoid S M) Sₘ] [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] [Module.Free R S] [Module.Finite R S] (a : S) : (trace Rₘ Sₘ) ((algebraMap S Sₘ) a) = (algebraMap R Rₘ) ((trace R S) 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} [CommRing R] [CommRing S] [Algebra R S] {Rₘ : Type u_3} [CommRing Rₘ] [Algebra R Rₘ] (M : Submonoid R) [IsLocalization M Rₘ] (Sₘ : Type u_5) [CommRing Sₘ] [Algebra S Sₘ] [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] [IsLocalization (algebraMapSubmonoid S M) Sₘ] {ι : Type u_6} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι R S) : traceMatrix Rₘ ⇑(Module.Basis.localizationLocalization Rₘ M Sₘ b) = (algebraMap R Rₘ).mapMatrix (traceMatrix R ⇑b)

theorem Algebra.discr_localizationLocalization (R : Type u_1) {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {Rₘ : Type u_3} [CommRing Rₘ] [Algebra R Rₘ] (M : Submonoid R) [IsLocalization M Rₘ] (Sₘ : Type u_5) [CommRing Sₘ] [Algebra S Sₘ] [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] [IsLocalization (algebraMapSubmonoid S M) Sₘ] {ι : Type u_6} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι R S) : discr Rₘ ⇑(Module.Basis.localizationLocalization Rₘ M Sₘ b) = (algebraMap R Rₘ) (discr R ⇑b)

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.