feat(FieldTheory/LinearDisjoint): trace (resp. norm) and algebraMap commutes (leanprover-community#25832)

For  `A` and `B` two linearly disjoint `R`-subalgebras in a commutative algebra `S` and `b` a `R`-basis of `B`, we construct  a `A`-basis of `S = A ⊔ B` from `b` (and a similar construction using a `R`-basis of `A`). Then, we prove in this situation that `trace` commutes with `algebraMap`, that is:
```lean
Algebra.trace A S (algebraMap B S x) = algebraMap R A (Algebra.trace R B x)
```
and a similar result for the norm.

We also add a similar basis construction for `A` and `B` two linearly disjoint intermediate fields with the hypothesis that `A.toSubalgebra ⊔ B.toSubalgebra = ⊤`. This hypothesis is equivalent to `A ⊔ B = ⊤` in many cases (for example, one of the two extensions is algebraic over the base field) but not always.

Author: xroblot

Mathlib/FieldTheory/LinearDisjoint.lean

@@ -3,7 +3,6 @@ Copyright (c) 2024 Jz Pan. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jz Pan
 -/
-import Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
 import Mathlib.RingTheory.AlgebraicIndependent.RankAndCardinality
 import Mathlib.RingTheory.LinearDisjoint
 
@@ -256,6 +255,52 @@ theorem linearIndependent_right (H : A.LinearDisjoint B)
     {ι : Type*} {b : ι → B} (hb : LinearIndependent F b) : LinearIndependent A (B.val ∘ b) :=
   (linearDisjoint_iff'.1 H).linearIndependent_right_of_flat hb
 
+/--
+If `A` and `B` are linearly disjoint and such that `A.toSubalgebra ⊔ B.toSubalgebra = ⊤`,
+then any `F`-basis of `B` is also an `A`-basis of `E`.
+Note that the condition `A.toSubalgebra ⊔ B.toSubalgebra = ⊤` is equivalent to
+`A ⊔ B = ⊤` in many cases, see `IntermediateField.sup_toSubalgebra_of_isAlgebraic_right` and similar
+results.
+-/
+noncomputable def basisOfBasisRight (H : A.LinearDisjoint B)
+    (H' : A.toSubalgebra ⊔ B.toSubalgebra = ⊤) {ι : Type*} (b : Basis ι F B) :
+    Basis ι A E :=
+  (linearDisjoint_iff'.mp H).basisOfBasisRight H' b
+
+@[simp]
+theorem basisOfBasisRight_apply (H : A.LinearDisjoint B) (H' : A.toSubalgebra ⊔ B.toSubalgebra = ⊤)
+    {ι : Type*} (b : Basis ι F B) (i : ι) :
+    H.basisOfBasisRight H' b i = algebraMap B E (b i) :=
+  (linearDisjoint_iff'.mp H).algebraMap_basisOfBasisRight_apply H' b i
+
+theorem algebraMap_basisOfBasisRight_repr_apply (H : A.LinearDisjoint B)
+    (H' : A.toSubalgebra ⊔ B.toSubalgebra = ⊤) {ι : Type*} (b : Basis ι F B) (x : B) (i : ι) :
+    algebraMap A E ((H.basisOfBasisRight H' b).repr x i) = algebraMap F E (b.repr x i) :=
+  (linearDisjoint_iff'.mp H).algebraMap_basisOfBasisRight_repr_apply H' b x i
+
+/--
+If `A` and `B` are linearly disjoint and such that `A.toSubalgebra ⊔ B.toSubalgebra = ⊤`,
+then any `F`-basis of `A` is also a `B`-basis of `E`.
+Note that the condition `A.toSubalgebra ⊔ B.toSubalgebra = ⊤` is equivalent to
+`A ⊔ B = ⊤` in many cases, see `IntermediateField.sup_toSubalgebra_of_isAlgebraic_right` and similar
+results.
+-/
+noncomputable def basisOfBasisLeft (H : A.LinearDisjoint B)
+    (H' : A.toSubalgebra ⊔ B.toSubalgebra = ⊤) {ι : Type*} (b : Basis ι F A) :
+    Basis ι B E :=
+  (linearDisjoint_iff'.mp H).basisOfBasisLeft H' b
+
+@[simp]
+theorem basisOfBasisLeft_apply (H : A.LinearDisjoint B) (H' : A.toSubalgebra ⊔ B.toSubalgebra = ⊤)
+    {ι : Type*} (b : Basis ι F A) (i : ι) :
+    H.basisOfBasisLeft H' b i = algebraMap A E (b i) :=
+  (linearDisjoint_iff'.mp H).basisOfBasisLeft_apply H' b i
+
+theorem basisOfBasisLeft_repr_apply (H : A.LinearDisjoint B)
+    (H' : A.toSubalgebra ⊔ B.toSubalgebra = ⊤) {ι : Type*} (b : Basis ι F A) (x : A) (i : ι) :
+    algebraMap B E ((H.basisOfBasisLeft H' b).repr x i) = algebraMap F E (b.repr x i) :=
+  (linearDisjoint_iff'.mp H).basisOfBasisLeft_repr_apply H' b x i
+
 /-- If there exists an `F`-basis of `B` which remains linearly independent over `A`, then
 `A` and `B` are linearly disjoint. -/
 theorem of_basis_right {ι : Type*} (b : Basis ι F B)
@@ -634,6 +679,26 @@ theorem algEquiv_of_isAlgebraic (H : A.LinearDisjoint L)
   .of_isField ((Algebra.TensorProduct.congr f1 f2).symm.toMulEquiv.isField
     (H.isField_of_isAlgebraic halg))
 
+/--
+If `A` and `B` are linearly disjoint, then `trace` and `algebraMap` commutes.
+-/
+theorem trace_algebraMap [FiniteDimensional F E] (h₁ : A.LinearDisjoint B) (h₂ : A ⊔ B = ⊤)
+    (x : B) :
+    Algebra.trace A E (algebraMap B E x) = algebraMap F A (Algebra.trace F B x) := by
+  rw [linearDisjoint_iff'] at h₁
+  refine h₁.trace_algebraMap ?_ x
+  simpa [sup_toSubalgebra_of_isAlgebraic_right] using congr_arg toSubalgebra h₂
+
+/--
+If `A` and `B` are linearly disjoint, then `norm` and `algebraMap` commutes.
+-/
+theorem norm_algebraMap [FiniteDimensional F E] (h₁ : A.LinearDisjoint B) (h₂ : A ⊔ B = ⊤)
+    (x : B) :
+    Algebra.norm A (algebraMap B E x) = algebraMap F A (Algebra.norm F x) := by
+  rw [linearDisjoint_iff'] at h₁
+  refine h₁.norm_algebraMap ?_  x
+  simpa [sup_toSubalgebra_of_isAlgebraic_right] using congr_arg toSubalgebra h₂
+
 end LinearDisjoint
 
 end IntermediateField

Mathlib/RingTheory/LinearDisjoint.lean

@@ -6,17 +6,15 @@ Authors: Jz Pan
 import Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
 import Mathlib.Algebra.Algebra.Subalgebra.Rank
 import Mathlib.Algebra.Polynomial.Basis
-import Mathlib.LinearAlgebra.Basis.VectorSpace
-import Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
 import Mathlib.LinearAlgebra.LinearDisjoint
 import Mathlib.LinearAlgebra.TensorProduct.Subalgebra
 import Mathlib.RingTheory.Adjoin.Dimension
 import Mathlib.RingTheory.Algebraic.Basic
 import Mathlib.RingTheory.IntegralClosure.Algebra.Defs
 import Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
-import Mathlib.RingTheory.Localization.FractionRing
-import Mathlib.RingTheory.TensorProduct.Finite
+import Mathlib.RingTheory.Norm.Defs
 import Mathlib.RingTheory.TensorProduct.Nontrivial
+import Mathlib.RingTheory.Trace.Defs
 
 /-!
 
@@ -244,6 +242,72 @@ protected def mulMap :=
 @[simp]
 theorem val_mulMap_tmul (a : A) (b : B) : (H.mulMap (a ⊗ₜ[R] b) : S) = a.1 * b.1 := rfl
 
+/--
+If `A` and `B` are linearly disjoint subalgebras in a commutative algebra `S` over `R`
+such that `A ⊔ B = S`, then this is the natural isomorphism
+`A ⊗[R] B ≃ₐ[A] S` induced by multiplication in `S`.
+-/
+noncomputable def mulMapLeftOfSupEqTop (H' : A ⊔ B = ⊤) :
+    A ⊗[R] B ≃ₐ[A] S :=
+  (AlgEquiv.ofInjective (Algebra.TensorProduct.productLeftAlgHom
+    (Algebra.ofId A S) B.val) H.injective).trans ((Subalgebra.equivOfEq _ _ (by
+      apply Subalgebra.restrictScalars_injective R
+      rw [restrictScalars_top, ← H']
+      exact mulMap_range A B)).trans Subalgebra.topEquiv)
+
+@[simp]
+theorem mulMapLeftOfSupEqTop_tmul (H' : A ⊔ B = ⊤) (a : A) (b : B) :
+    H.mulMapLeftOfSupEqTop H' (a ⊗ₜ[R] b) = (a : S) * (b : S) := rfl
+
+/--
+If `A` and `B` are linearly disjoint subalgebras in a commutative algebra `S` over `R`
+such that `A ⊔ B = S`, then any `R`-basis of `B` is also an `A`-basis of `S`.
+-/
+noncomputable def basisOfBasisRight (H' : A ⊔ B = ⊤) {ι : Type*} (b : Basis ι R B) :
+    Basis ι A S :=
+  (b.baseChange A).map (H.mulMapLeftOfSupEqTop H').toLinearEquiv
+
+@[simp]
+theorem algebraMap_basisOfBasisRight_apply (H' : A ⊔ B = ⊤) {ι : Type*} (b : Basis ι R B) (i : ι) :
+    H.basisOfBasisRight H' b i = algebraMap B S (b i) := by
+  simp [basisOfBasisRight, Subalgebra.algebraMap_def]
+
+@[simp]
+theorem mulMapLeftOfSupEqTop_symm_apply (H' : A ⊔ B = ⊤) (x : B) :
+    (H.mulMapLeftOfSupEqTop H').symm x = 1 ⊗ₜ[R] x :=
+  (H.mulMapLeftOfSupEqTop H').symm_apply_eq.mpr (by simp)
+
+theorem algebraMap_basisOfBasisRight_repr_apply (H' : A ⊔ B = ⊤) {ι : Type*} (b : Basis ι R B)
+    (x : B) (i : ι) :
+    algebraMap A S ((H.basisOfBasisRight H' b).repr x i) = algebraMap R S (b.repr x i) := by
+  simp [basisOfBasisRight, Algebra.algebraMap_eq_smul_one]
+
+theorem leftMulMatrix_basisOfBasisRight_algebraMap (H' : A ⊔ B = ⊤) {ι : Type*} [Fintype ι]
+    [DecidableEq ι] (b : Basis ι R B) (x : B) :
+    Algebra.leftMulMatrix (H.basisOfBasisRight H' b) (algebraMap B S x) =
+      RingHom.mapMatrix (algebraMap R A) (Algebra.leftMulMatrix b x) := by
+  ext
+  simp [Algebra.leftMulMatrix_eq_repr_mul, ← H.algebraMap_basisOfBasisRight_repr_apply H',
+    Subalgebra.algebraMap_def]
+
+/--
+If `A` and `B` are subalgebras in a commutative algebra `S` over `R`, and if they are
+linearly disjoint and such that `A ⊔ B = S`, then any `R`-basis of `A` is also a `B`-basis of `S`.
+-/
+noncomputable def basisOfBasisLeft (H' : A ⊔ B = ⊤) {ι : Type*} (b : Basis ι R A) :
+    Basis ι B S :=
+  (b.baseChange B).map (H.symm.mulMapLeftOfSupEqTop (by rwa [sup_comm])).toLinearEquiv
+
+@[simp]
+theorem basisOfBasisLeft_apply (H' : A ⊔ B = ⊤) {ι : Type*} (b : Basis ι R A) (i : ι) :
+    H.basisOfBasisLeft H' b i = algebraMap A S (b i) :=
+  H.symm.algebraMap_basisOfBasisRight_apply (by rwa [sup_comm]) b i
+
+theorem basisOfBasisLeft_repr_apply (H' : A ⊔ B = ⊤) {ι : Type*} (b : Basis ι R A)
+    (x : A) (i : ι) :
+    algebraMap B S ((H.basisOfBasisLeft H' b).repr x i) = algebraMap R S (b.repr x i) :=
+  H.symm.algebraMap_basisOfBasisRight_repr_apply (by rwa [sup_comm]) b x i
+
 include H in
 /-- If `A` and `B` are subalgebras in a commutative algebra `S` over `R`, and if they are
 linearly disjoint, and if they are free `R`-modules, then `A ⊔ B` is also a free `R`-module. -/
@@ -463,24 +527,45 @@ namespace LinearDisjoint
 
 variable [CommRing R] [CommRing S] [Algebra R S]
 
-variable (A B : Subalgebra R S)
+variable {A B : Subalgebra R S}
+
+/--
+If `A` and `B` are subalgebras in a commutative algebra `S` over `R`, and if they are
+linearly disjoint and such that `A ⊔ B = S`, then `trace` and `algebraMap` commutes.
+-/
+theorem trace_algebraMap (H : A.LinearDisjoint B) (H' : A ⊔ B = ⊤) [Module.Free R B]
+    [Module.Finite R B] (x : B) :
+    Algebra.trace A S (algebraMap B S x) = algebraMap R A (Algebra.trace R B x) := by
+  simp_rw [Algebra.trace_eq_matrix_trace (Module.Free.chooseBasis R B),
+    Algebra.trace_eq_matrix_trace (H.basisOfBasisRight H' (Module.Free.chooseBasis R B)),
+    Matrix.trace, map_sum, leftMulMatrix_basisOfBasisRight_algebraMap, RingHom.mapMatrix_apply,
+    Matrix.diag_apply, Matrix.map_apply]
+
+/--
+If `A` and `B` are subalgebras in a commutative algebra `S` over `R`, and if they are
+linearly disjoint and such that `A ⊔ B = S`, then `norm` and `algebraMap` commutes.
+-/
+theorem norm_algebraMap (H : A.LinearDisjoint B) (H' : A ⊔ B = ⊤) [Module.Free R B]
+    [Module.Finite R B] (x : B) :
+    Algebra.norm A (algebraMap B S x) = algebraMap R A (Algebra.norm R x) := by
+  simp_rw [Algebra.norm_eq_matrix_det (Module.Free.chooseBasis R B),
+    Algebra.norm_eq_matrix_det (H.basisOfBasisRight H' (Module.Free.chooseBasis R B)),
+    leftMulMatrix_basisOfBasisRight_algebraMap, RingHom.map_det]
 
-variable {A B} in
 /-- In a commutative ring, if `A` and `B` are linearly disjoint, if `B` is a flat `R`-module,
 then for any family of `R`-linearly independent elements of `A`,
 they are also `B`-linearly independent. -/
 theorem linearIndependent_left_of_flat (H : A.LinearDisjoint B) [Module.Flat R B]
     {ι : Type*} {a : ι → A} (ha : LinearIndependent R a) : LinearIndependent B (A.val ∘ a) :=
   H.linearIndependent_left_of_flat_of_commute ha fun _ _ ↦ mul_comm _ _
 
+variable (A B) in
 /-- In a commutative ring, if a basis of `A` is also `B`-linearly independent,
 then `A` and `B` are linearly disjoint. -/
 theorem of_basis_left {ι : Type*} (a : Basis ι R A)
     (H : LinearIndependent B (A.val ∘ a)) : A.LinearDisjoint B :=
   of_basis_left_of_commute A B a H fun _ _ ↦ mul_comm _ _
 
-variable {A B}
-
 variable (R) in
 /-- If `A` and `B` are flat algebras over `R`, such that `A ⊗[R] B` is a domain, and such that
 the algebra maps are injective, then there exists an `R`-algebra `K` that is a field that `A`