[Merged by Bors] - feat: add Algebra.discr_localizationLocalization

Mathlib/LinearAlgebra/Matrix/Trace.lean

@@ -108,6 +108,10 @@ theorem trace_sum (s : Finset ι) (f : ι → Matrix n n R) :
   map_sum (traceAddMonoidHom n R) f s
 #align matrix.trace_sum Matrix.trace_sum
 
+theorem _root_.AddMonoidHom.map_trace [AddCommMonoid S] (f : R →+ S) (A : Matrix n n R) :
+    f (trace A)  = trace (f.mapMatrix A) :=
+  map_sum f (fun i => diag A i) Finset.univ
+
 end AddCommMonoid
 
 section AddCommGroup

Mathlib/RingTheory/Localization/NormTrace.lean

@@ -5,21 +5,27 @@ Authors: Anne Baanen
 -/
 import Mathlib.RingTheory.Localization.Module
 import Mathlib.RingTheory.Norm
+import Mathlib.RingTheory.Discriminant
 
 #align_import ring_theory.localization.norm from "leanprover-community/mathlib"@"2e59a6de168f95d16b16d217b808a36290398c0a"
 
 /-!
 
-# Field/algebra norm and localization
+# Field/algebra norm / trace and localization
 
-This file contains results on the combination of `Algebra.norm` and `IsLocalization`.
+This file contains results on the combination of `Algebra.norm`, `Algebra.trace` and
+`IsLocalization`.
 
 ## 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
+
 ## Tags
 
 field norm, algebra norm, localization
@@ -39,6 +45,16 @@ variable [IsLocalization M Rₘ] [IsLocalization (Algebra.algebraMapSubmonoid S
 
 variable [Algebra Rₘ Sₘ] [Algebra R Sₘ] [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ]
 
+open Algebra
+
+theorem Algebra.map_leftMulMatrix_localization {ι : Type _} [Fintype ι] [DecidableEq ι]
+    (b : Basis ι R S) (a : S) :
+    (algebraMap R Rₘ).mapMatrix (leftMulMatrix b a) =
+    leftMulMatrix (b.localizationLocalization Rₘ M Sₘ) (algebraMap S Sₘ a) := by
+  ext i j
+  simp only [Matrix.map_apply, RingHom.mapMatrix_apply, leftMulMatrix_eq_repr_mul, ← map_mul,
+    Basis.localizationLocalization_apply, Basis.localizationLocalization_repr_algebraMap]
+
 /-- 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.
 -/
@@ -50,10 +66,47 @@ theorem Algebra.norm_localization [Module.Free R S] [Module.Finite R S] (a : S)
   let b := Module.Free.chooseBasis R S
   letI := Classical.decEq (Module.Free.ChooseBasisIndex R S)
   rw [Algebra.norm_eq_matrix_det (b.localizationLocalization Rₘ M Sₘ),
-    Algebra.norm_eq_matrix_det b, RingHom.map_det]
-  congr
-  ext i j
-  simp only [Matrix.map_apply, RingHom.mapMatrix_apply, Algebra.leftMulMatrix_eq_repr_mul,
-    Basis.localizationLocalization_apply, ← _root_.map_mul]
-  apply Basis.localizationLocalization_repr_algebraMap
+    Algebra.norm_eq_matrix_det b, RingHom.map_det, ← Algebra.map_leftMulMatrix_localization]
 #align algebra.norm_localization Algebra.norm_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.
+-/
+theorem Algebra.trace_localization [Module.Free R S] [Module.Finite R S] (a : S) :
+    Algebra.trace Rₘ Sₘ (algebraMap S Sₘ a) = algebraMap R Rₘ (Algebra.trace R S a) := by
+  cases subsingleton_or_nontrivial R
+  · haveI : Subsingleton Rₘ := Module.subsingleton R Rₘ
+    simp
+  let b := Module.Free.chooseBasis R S
+  letI := Classical.decEq (Module.Free.ChooseBasisIndex R S)
+  rw [Algebra.trace_eq_matrix_trace (b.localizationLocalization Rₘ M Sₘ),
+    Algebra.trace_eq_matrix_trace b, ← Algebra.map_leftMulMatrix_localization]
+  exact (AddMonoidHom.map_trace (algebraMap R Rₘ).toAddMonoidHom _).symm
+
+section LocalizationLocalization
+
+variable (Aₘ : Type _) [CommRing Aₘ] [Algebra S Aₘ] [Algebra Rₘ Aₘ] [Algebra R Aₘ]
+
+variable [IsScalarTower R Rₘ Aₘ] [IsScalarTower R S Aₘ]
+
+variable [IsLocalization (Algebra.algebraMapSubmonoid S M) Aₘ]
+
+variable {ι : Type _} [Fintype ι] [DecidableEq ι]
+
+theorem Algebra.traceMatrix_localizationLocalization (b : Basis ι R S) :
+    Algebra.traceMatrix Rₘ (b.localizationLocalization Rₘ M Aₘ) =
+      (algebraMap R Rₘ).mapMatrix (Algebra.traceMatrix R b) := by
+  have : Module.Finite R S := Module.Finite.of_basis b
+  have : Module.Free R S := Module.Free.of_basis b
+  ext i j : 2
+  simp_rw [RingHom.mapMatrix_apply, Matrix.map_apply, traceMatrix_apply, traceForm_apply,
+    Basis.localizationLocalization_apply, ← map_mul]
+  exact Algebra.trace_localization R M _
+
+theorem Algebra.discr_localizationLocalization (b : Basis ι R S) :
+  Algebra.discr Rₘ (b.localizationLocalization Rₘ M Aₘ) =
+    algebraMap R Rₘ (Algebra.discr R b) := by
+  rw [Algebra.discr_def, Algebra.discr_def, RingHom.map_det,
+    Algebra.traceMatrix_localizationLocalization]
+
+end LocalizationLocalization