feat(LinearAlgebra): generalize results about Module.rank of `Linea…

…rMap`. (#9677)

**LinearAlgebra/LinearIndependent**: generalize `linearIndependent_algHom_toLinearMap(')` to allow different domain and codomain of the AlgHom.

**LinearAlgebra/Basic**: add `LinearEquiv.congrLeft` that works for two rings with commuting actions on the codomain.

**LinearAlgebra/FreeModule/Finite/Matrix**: generalize `Module.Free.linearMap`, `Module.Finite.linearMap`, and `FiniteDimensional.finrank_linearMap` to work with two different rings that may be noncommutative. Add `FiniteDimensional.rank_linearMap`, `FiniteDimensional.(fin)rank_linearMap_self`, and `card/cardinal_mk_algHom_le_rank`.

**FieldTheory/Tower**: remove the instance `LinearMap.finite_dimensional''` which becomes redundant; mark `finrank_linear_map'` as deprecated (superseded by `finrank_linearMap_self`.



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Mathlib/Algebra/Category/FGModuleCat/Basic.lean

@@ -213,8 +213,8 @@ instance (V W : FGModuleCat K) : Module.Finite K (V ⟶ W) :=
   (by infer_instance : Module.Finite K (V →ₗ[K] W))
 
 instance closedPredicateModuleFinite :
-    MonoidalCategory.ClosedPredicate fun V : ModuleCat.{u} K => Module.Finite K V where
-  prop_ihom := @fun X Y hX hY => @Module.Finite.linearMap K X Y _ _ _ _ _ _ _ hX hY
+    MonoidalCategory.ClosedPredicate fun V : ModuleCat.{u} K ↦ Module.Finite K V where
+  prop_ihom {X Y} _ _ := Module.Finite.linearMap K K X Y
 #align fgModule.closed_predicate_module_finite FGModuleCat.closedPredicateModuleFinite
 
 instance : MonoidalClosed (FGModuleCat K) := by

Mathlib/FieldTheory/Fixed.lean

@@ -320,7 +320,7 @@ theorem linearIndependent_toLinearMap (R : Type u) (A : Type v) (B : Type w) [Co
 #align linear_independent_to_linear_map linearIndependent_toLinearMap
 
 theorem cardinal_mk_algHom (K : Type u) (V : Type v) (W : Type w) [Field K] [Field V] [Algebra K V]
-    [FiniteDimensional K V] [Field W] [Algebra K W] [FiniteDimensional K W] :
+    [FiniteDimensional K V] [Field W] [Algebra K W] :
     Cardinal.mk (V →ₐ[K] W) ≤ finrank W (V →ₗ[K] W) :=
   (linearIndependent_toLinearMap K V W).cardinal_mk_le_finrank
 #align cardinal_mk_alg_hom cardinal_mk_algHom
@@ -345,7 +345,7 @@ theorem finrank_eq_card (G : Type u) (F : Type v) [Group G] [Field F] [Fintype G
       Fintype.card G ≤ Fintype.card (F →ₐ[FixedPoints.subfield G F] F) :=
         Fintype.card_le_of_injective _ (MulSemiringAction.toAlgHom_injective _ F)
       _ ≤ finrank F (F →ₗ[FixedPoints.subfield G F] F) := (finrank_algHom (subfield G F) F)
-      _ = finrank (FixedPoints.subfield G F) F := finrank_linear_map' _ _ _
+      _ = finrank (FixedPoints.subfield G F) F := finrank_linearMap_self _ _ _
 #align fixed_points.finrank_eq_card FixedPoints.finrank_eq_card
 
 /-- `MulSemiringAction.toAlgHom` is bijective. -/
@@ -359,7 +359,7 @@ theorem toAlgHom_bijective (G : Type u) (F : Type v) [Group G] [Field F] [Finite
   · apply le_antisymm
     · exact Fintype.card_le_of_injective _ (MulSemiringAction.toAlgHom_injective _ F)
     · rw [← finrank_eq_card G F]
-      exact LE.le.trans_eq (finrank_algHom _ F) (finrank_linear_map' _ _ _)
+      exact LE.le.trans_eq (finrank_algHom _ F) (finrank_linearMap_self _ _ _)
 #align fixed_points.to_alg_hom_bijective FixedPoints.toAlgHom_bijective
 
 /-- Bijection between G and algebra homomorphisms that fix the fixed points -/

Mathlib/FieldTheory/Minpoly/Field.lean

@@ -279,7 +279,7 @@ lemma minpoly_algEquiv_toLinearMap (σ : L ≃ₐ[K] L) (hσ : IsOfFinOrder σ)
     simp_rw [← AlgEquiv.pow_toLinearMap] at hs
     apply hq.ne_zero
     simpa using Fintype.linearIndependent_iff.mp
-      (((linearIndependent_algHom_toLinearMap' K L).comp _ AlgEquiv.coe_algHom_injective).comp _
+      (((linearIndependent_algHom_toLinearMap' K L L).comp _ AlgEquiv.coe_algHom_injective).comp _
         (Subtype.val_injective.comp ((finEquivPowers σ hσ).injective)))
       (q.coeff ∘ (↑)) hs ⟨_, H⟩
 

Mathlib/FieldTheory/Tower.lean

@@ -87,23 +87,7 @@ theorem Subalgebra.isSimpleOrder_of_finrank_prime (F A) [Field F] [Ring A] [IsDo
 #align finite_dimensional.subalgebra.is_simple_order_of_finrank_prime FiniteDimensional.Subalgebra.isSimpleOrder_of_finrank_prime
 -- TODO: `IntermediateField` version
 
--- TODO: generalize by removing [FiniteDimensional F K]
--- V = ⊕F,
--- (V →ₗ[F] K) = ((⊕F) →ₗ[F] K) = (⊕ (F →ₗ[F] K)) = ⊕K
-instance _root_.LinearMap.finite_dimensional'' (F : Type u) (K : Type v) (V : Type w) [Field F]
-    [Field K] [Algebra F K] [FiniteDimensional F K] [AddCommGroup V] [Module F V]
-    [FiniteDimensional F V] : FiniteDimensional K (V →ₗ[F] K) :=
-  right F _ _
-#align linear_map.finite_dimensional'' LinearMap.finite_dimensional''
-
-theorem finrank_linear_map' (F : Type u) (K : Type v) (V : Type w) [Field F] [Field K] [Algebra F K]
-    [FiniteDimensional F K] [AddCommGroup V] [Module F V] [FiniteDimensional F V] :
-    finrank K (V →ₗ[F] K) = finrank F V :=
-  mul_right_injective₀ finrank_pos.ne' <|
-    calc
-      finrank F K * finrank K (V →ₗ[F] K) = finrank F (V →ₗ[F] K) := finrank_mul_finrank _ _ _
-      _ = finrank F V * finrank F K := (finrank_linearMap F V K)
-      _ = finrank F K * finrank F V := mul_comm _ _
+@[deprecated] alias finrank_linear_map' := FiniteDimensional.finrank_linearMap_self
 #align finite_dimensional.finrank_linear_map' FiniteDimensional.finrank_linear_map'
 
 end FiniteDimensional

Mathlib/LinearAlgebra/Basic.lean

@@ -1346,6 +1346,19 @@ theorem conj_id (e : M ≃ₗ[R] M₂) : e.conj LinearMap.id = LinearMap.id := b
   simp [conj_apply]
 #align linear_equiv.conj_id LinearEquiv.conj_id
 
+variable (M) in
+/-- An `R`-linear isomorphism between two `R`-modules `M₂` and `M₃` induces an `S`-linear
+isomorphism between `M₂ →ₗ[R] M` and `M₃ →ₗ[R] M`, if `M` is both an `R`-module and an
+`S`-module and their actions commute. -/
+def congrLeft {R} (S) [Semiring R] [Semiring S] [Module R M₂] [Module R M₃] [Module R M]
+    [Module S M] [SMulCommClass R S M] (e : M₂ ≃ₗ[R] M₃) : (M₂ →ₗ[R] M) ≃ₗ[S] (M₃ →ₗ[R] M) where
+  toFun f := f.comp e.symm.toLinearMap
+  invFun f := f.comp e.toLinearMap
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
+  left_inv f := by dsimp only; apply FunLike.ext; exact (congr_arg f <| e.left_inv ·)
+  right_inv f := by dsimp only; apply FunLike.ext; exact (congr_arg f <| e.right_inv ·)
+
 end CommSemiring
 
 section Field

Mathlib/LinearAlgebra/FreeModule/Finite/Matrix.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Riccardo Brasca
 -/
 import Mathlib.LinearAlgebra.Dimension.LinearMap
+import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
 
 #align_import linear_algebra.free_module.finite.matrix from "leanprover-community/mathlib"@"b1c23399f01266afe392a0d8f71f599a0dad4f7b"
 
@@ -21,80 +22,97 @@ We provide some instances for finite and free modules involving matrices.
 -/
 
 
-universe u v w
+universe u u' v w
 
-variable (R : Type u) (M : Type v) (N : Type w)
+variable (R : Type u) (S : Type u') (M : Type v) (N : Type w)
 
-open Module.Free (chooseBasis)
+open Module.Free (chooseBasis ChooseBasisIndex)
 
 open FiniteDimensional (finrank)
 
-section CommRing
+section Ring
 
-variable [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M]
+variable [Ring R] [Ring S] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M]
+variable [AddCommGroup N] [Module R N] [Module S N] [SMulCommClass R S N]
 
-variable [AddCommGroup N] [Module R N] [Module.Free R N]
+private noncomputable def linearMapEquivFun : (M →ₗ[R] N) ≃ₗ[S] ChooseBasisIndex R M → N :=
+  (chooseBasis R M).repr.congrLeft N S ≪≫ₗ (Finsupp.lsum S).symm ≪≫ₗ
+    LinearEquiv.piCongrRight fun _ ↦ LinearMap.ringLmapEquivSelf R S N
 
-instance Module.Free.linearMap [Module.Finite R M] [Module.Finite R N] :
-    Module.Free R (M →ₗ[R] N) := by
-  cases subsingleton_or_nontrivial R
-  · apply Module.Free.of_subsingleton'
-  classical exact
-      Module.Free.of_equiv (LinearMap.toMatrix (chooseBasis R M) (chooseBasis R N)).symm
+instance Module.Free.linearMap [Module.Free S N] : Module.Free S (M →ₗ[R] N) :=
+  Module.Free.of_equiv (linearMapEquivFun R S M N).symm
 #align module.free.linear_map Module.Free.linearMap
 
-variable {R}
-
-instance Module.Finite.linearMap [Module.Finite R M] [Module.Finite R N] :
-    Module.Finite R (M →ₗ[R] N) := by
-  cases subsingleton_or_nontrivial R
-  · infer_instance
-  classical
-    have f := (LinearMap.toMatrix (chooseBasis R M) (chooseBasis R N)).symm
-    exact Module.Finite.of_surjective f.toLinearMap (LinearEquiv.surjective f)
+instance Module.Finite.linearMap [Module.Finite S N] : Module.Finite S (M →ₗ[R] N) :=
+  Module.Finite.equiv (linearMapEquivFun R S M N).symm
 #align module.finite.linear_map Module.Finite.linearMap
 
-end CommRing
+variable [StrongRankCondition R] [StrongRankCondition S] [Module.Free S N]
 
-section Integer
+open Cardinal
+theorem FiniteDimensional.rank_linearMap :
+    Module.rank S (M →ₗ[R] N) = lift.{w} (Module.rank R M) * lift.{v} (Module.rank S N) := by
+  rw [(linearMapEquivFun R S M N).rank_eq, rank_fun_eq_lift_mul,
+    ← finrank_eq_card_chooseBasisIndex, ← finrank_eq_rank R, lift_natCast]
 
-variable [AddCommGroup M] [Module.Finite ℤ M] [Module.Free ℤ M]
+/-- The finrank of `M →ₗ[R] N` as an `S`-module is `(finrank R M) * (finrank S N)`. -/
+theorem FiniteDimensional.finrank_linearMap :
+    finrank S (M →ₗ[R] N) = finrank R M * finrank S N := by
+  simp_rw [finrank, rank_linearMap, toNat_mul, toNat_lift]
+#align finite_dimensional.finrank_linear_map FiniteDimensional.finrank_linearMap
 
-variable [AddCommGroup N] [Module.Finite ℤ N] [Module.Free ℤ N]
+variable [Module R S] [SMulCommClass R S S]
 
-instance Module.Finite.addMonoidHom : Module.Finite ℤ (M →+ N) :=
-  Module.Finite.equiv (addMonoidHomLequivInt ℤ).symm
-#align module.finite.add_monoid_hom Module.Finite.addMonoidHom
+theorem FiniteDimensional.rank_linearMap_self :
+    Module.rank S (M →ₗ[R] S) = lift.{u'} (Module.rank R M) := by
+  rw [rank_linearMap, rank_self, lift_one, mul_one]
 
-instance Module.Free.addMonoidHom : Module.Free ℤ (M →+ N) :=
-  letI : Module.Free ℤ (M →ₗ[ℤ] N) := Module.Free.linearMap _ _ _
-  Module.Free.of_equiv (addMonoidHomLequivInt ℤ).symm
-#align module.free.add_monoid_hom Module.Free.addMonoidHom
+theorem FiniteDimensional.finrank_linearMap_self : finrank S (M →ₗ[R] S) = finrank R M := by
+  rw [finrank_linearMap, finrank_self, mul_one]
 
-end Integer
+end Ring
 
-section CommRing
+section AlgHom
 
-variable [CommRing R] [StrongRankCondition R]
+variable (K M : Type*) (L : Type v) [CommRing K] [Ring M] [Algebra K M]
+  [Module.Free K M] [Module.Finite K M] [CommRing L] [IsDomain L] [Algebra K L]
 
-variable [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M]
+instance Finite.algHom : Finite (M →ₐ[K] L) :=
+  (linearIndependent_algHom_toLinearMap K M L).finite
 
-variable [AddCommGroup N] [Module R N] [Module.Free R N] [Module.Finite R N]
+open Cardinal
 
-/-- The finrank of `M →ₗ[R] N` is `(finrank R M) * (finrank R N)`. -/
-theorem FiniteDimensional.finrank_linearMap :
-    finrank R (M →ₗ[R] N) = finrank R M * finrank R N := by
-  classical
-    letI := nontrivial_of_invariantBasisNumber R
-    have h := LinearMap.toMatrix (chooseBasis R M) (chooseBasis R N)
-    simp_rw [h.finrank_eq, FiniteDimensional.finrank_matrix,
-      FiniteDimensional.finrank_eq_card_chooseBasisIndex, mul_comm]
-#align finite_dimensional.finrank_linear_map FiniteDimensional.finrank_linearMap
+theorem cardinal_mk_algHom_le_rank : #(M →ₐ[K] L) ≤ lift.{v} (Module.rank K M) := by
+  convert (linearIndependent_algHom_toLinearMap K M L).cardinal_lift_le_rank
+  · rw [lift_id]
+  · have := Module.nontrivial K L
+    rw [lift_id, FiniteDimensional.rank_linearMap_self]
+
+theorem card_algHom_le_finrank : Nat.card (M →ₐ[K] L) ≤ finrank K M := by
+  convert toNat_le_of_le_of_lt_aleph0 ?_ (cardinal_mk_algHom_le_rank K M L)
+  · rw [toNat_lift, finrank]
+  · rw [lift_lt_aleph0]; have := Module.nontrivial K L; apply rank_lt_aleph0
 
-end CommRing
+end AlgHom
+
+section Integer
+
+variable [AddCommGroup M] [Module.Finite ℤ M] [Module.Free ℤ M] [AddCommGroup N]
+
+instance Module.Finite.addMonoidHom [Module.Finite ℤ N] : Module.Finite ℤ (M →+ N) :=
+  Module.Finite.equiv (addMonoidHomLequivInt ℤ).symm
+#align module.finite.add_monoid_hom Module.Finite.addMonoidHom
+
+instance Module.Free.addMonoidHom [Module.Free ℤ N] : Module.Free ℤ (M →+ N) :=
+  letI : Module.Free ℤ (M →ₗ[ℤ] N) := Module.Free.linearMap _ _ _ _
+  Module.Free.of_equiv (addMonoidHomLequivInt ℤ).symm
+#align module.free.add_monoid_hom Module.Free.addMonoidHom
+
+end Integer
 
-theorem Matrix.rank_vecMulVec {K m n : Type u} [CommRing K] [StrongRankCondition K] [Fintype n]
+theorem Matrix.rank_vecMulVec {K m n : Type u} [CommRing K] [Fintype n]
     [DecidableEq n] (w : m → K) (v : n → K) : (Matrix.vecMulVec w v).toLin'.rank ≤ 1 := by
+  nontriviality K
   rw [Matrix.vecMulVec_eq, Matrix.toLin'_mul]
   refine' le_trans (LinearMap.rank_comp_le_left _ _) _
   refine' (LinearMap.rank_le_domain _).trans_eq _

Mathlib/LinearAlgebra/LinearIndependent.lean

@@ -1199,17 +1199,17 @@ theorem linearIndependent_monoidHom (G : Type*) [Monoid G] (L : Type*) [CommRing
 #align linear_independent_monoid_hom linearIndependent_monoidHom
 
 lemma linearIndependent_algHom_toLinearMap
-    (K L) [CommSemiring K] [CommRing L] [IsDomain L] [Algebra K L] :
-    LinearIndependent L (AlgHom.toLinearMap : (L →ₐ[K] L) → L →ₗ[K] L) := by
-  apply LinearIndependent.of_comp (LinearMap.ltoFun K L L)
-  exact (linearIndependent_monoidHom L L).comp
+    (K M L) [CommSemiring K] [Semiring M] [Algebra K M] [CommRing L] [IsDomain L] [Algebra K L] :
+    LinearIndependent L (AlgHom.toLinearMap : (M →ₐ[K] L) → M →ₗ[K] L) := by
+  apply LinearIndependent.of_comp (LinearMap.ltoFun K M L)
+  exact (linearIndependent_monoidHom M L).comp
     (RingHom.toMonoidHom ∘ AlgHom.toRingHom)
     (fun _ _ e ↦ AlgHom.ext (FunLike.congr_fun e : _))
 
-lemma linearIndependent_algHom_toLinearMap'
-    (K L) [CommRing K] [CommRing L] [IsDomain L] [Algebra K L] [NoZeroSMulDivisors K L] :
-    LinearIndependent K (AlgHom.toLinearMap : (L →ₐ[K] L) → L →ₗ[K] L) := by
-  apply (linearIndependent_algHom_toLinearMap K L).restrict_scalars
+lemma linearIndependent_algHom_toLinearMap' (K M L) [CommRing K]
+    [Semiring M] [Algebra K M] [CommRing L] [IsDomain L] [Algebra K L] [NoZeroSMulDivisors K L] :
+    LinearIndependent K (AlgHom.toLinearMap : (M →ₐ[K] L) → M →ₗ[K] L) := by
+  apply (linearIndependent_algHom_toLinearMap K M L).restrict_scalars
   simp_rw [Algebra.smul_def, mul_one]
   exact NoZeroSMulDivisors.algebraMap_injective K L
 

Mathlib/LinearAlgebra/Matrix/FiniteDimensional.lean

@@ -53,7 +53,7 @@ variable {V : Type*} [AddCommGroup V] [Module K V] [FiniteDimensional K V]
 variable {W : Type*} [AddCommGroup W] [Module K W] [FiniteDimensional K W]
 
 instance finiteDimensional : FiniteDimensional K (V →ₗ[K] W) :=
-  Module.Finite.linearMap _ _
+  Module.Finite.linearMap _ _ _ _
 #align linear_map.finite_dimensional LinearMap.finiteDimensional
 
 variable {A : Type*} [Ring A] [Algebra K A] [Module A V] [IsScalarTower K A V] [Module A W]

Mathlib/LinearAlgebra/Multilinear/FiniteDimensional.lean

@@ -48,7 +48,7 @@ private theorem free_and_finite_fin (n : ℕ) (N : Fin n → Type*) [∀ i, AddC
         ⟨Module.Free.of_equiv (multilinearCurryLeftEquiv R N M₂),
           Module.Finite.equiv (multilinearCurryLeftEquiv R N M₂)⟩
     cases ih fun i => N i.succ
-    exact ⟨Module.Free.linearMap _ _ _, Module.Finite.linearMap _ _⟩
+    exact ⟨Module.Free.linearMap _ _ _ _, Module.Finite.linearMap _ _ _ _⟩
 
 variable [∀ i, AddCommGroup (M₁ i)] [∀ i, Module R (M₁ i)]