feat: port LinearAlgebra.FreeModule.Rank (#3377)

This PR also fixes the order of universes in `Cardinal.lift_lift`.



Co-authored-by: Matthew Ballard <matt@mrb.email>
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>

Mathlib.lean

@@ -1284,6 +1284,7 @@ import Mathlib.LinearAlgebra.FinsuppVectorSpace
 import Mathlib.LinearAlgebra.FreeAlgebra
 import Mathlib.LinearAlgebra.FreeModule.Basic
 import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
+import Mathlib.LinearAlgebra.FreeModule.Rank
 import Mathlib.LinearAlgebra.GeneralLinearGroup
 import Mathlib.LinearAlgebra.InvariantBasisNumber
 import Mathlib.LinearAlgebra.Isomorphisms

Mathlib/LinearAlgebra/FreeModule/Rank.lean

@@ -0,0 +1,128 @@
+/-
+Copyright (c) 2021 Riccardo Brasca. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Riccardo Brasca
+
+! This file was ported from Lean 3 source module linear_algebra.free_module.rank
+! leanprover-community/mathlib commit 465d4301d8da5945ef1dc1b29fb34c2f2b315ac4
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.LinearAlgebra.Dimension
+
+/-!
+
+# Extra results about `Module.rank`
+
+This file contains some extra results not in `LinearAlgebra.Dimension`.
+
+-/
+
+
+universe u v w
+
+variable (R : Type u) (M : Type v) (N : Type w)
+
+open TensorProduct DirectSum BigOperators Cardinal
+
+open Cardinal
+
+section Ring
+
+variable [Ring R] [StrongRankCondition R]
+
+variable [AddCommGroup M] [Module R M] [Module.Free R M]
+
+variable [AddCommGroup N] [Module R N] [Module.Free R N]
+
+open Module.Free
+
+@[simp]
+theorem rank_finsupp (ι : Type w) :
+    Module.rank R (ι →₀ M) = Cardinal.lift.{v} (#ι) * Cardinal.lift.{w} (Module.rank R M) := by
+  obtain ⟨⟨_, bs⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
+  rw [← bs.mk_eq_rank'', ← (Finsupp.basis fun _ : ι => bs).mk_eq_rank'', Cardinal.mk_sigma,
+    Cardinal.sum_const]
+#align rank_finsupp rank_finsupp
+
+theorem rank_finsupp' (ι : Type v) : Module.rank R (ι →₀ M) = (#ι) * Module.rank R M := by
+  simp [rank_finsupp]
+#align rank_finsupp' rank_finsupp'
+
+set_option synthInstance.etaExperiment true in -- Porting note: gets around lean4#2074
+/-- The rank of `(ι →₀ R)` is `(# ι).lift`. -/
+@[simp]
+theorem rank_finsupp_self (ι : Type w) : Module.rank R (ι →₀ R) = Cardinal.lift.{u} (#ι) := by
+  simp [rank_finsupp]
+#align rank_finsupp_self rank_finsupp_self
+
+/-- If `R` and `ι` lie in the same universe, the rank of `(ι →₀ R)` is `# ι`. -/
+theorem rank_finsupp_self' {ι : Type u} : Module.rank R (ι →₀ R) = (#ι) := by simp
+#align rank_finsupp_self' rank_finsupp_self'
+
+/-- The rank of the direct sum is the sum of the ranks. -/
+@[simp]
+theorem rank_directSum {ι : Type v} (M : ι → Type w) [∀ i : ι, AddCommGroup (M i)]
+    [∀ i : ι, Module R (M i)] [∀ i : ι, Module.Free R (M i)] :
+    Module.rank R (⨁ i, M i) = Cardinal.sum fun i => Module.rank R (M i) := by
+  let B i := chooseBasis R (M i)
+  let b : Basis _ R (⨁ i, M i) := Dfinsupp.basis fun i => B i
+  simp [← b.mk_eq_rank'', fun i => (B i).mk_eq_rank'']
+#align rank_direct_sum rank_directSum
+
+/-- If `m` and `n` are `Fintype`, the rank of `m × n` matrices is `(# m).lift * (# n).lift`. -/
+@[simp]
+theorem rank_matrix (m : Type v) (n : Type w) [Finite m] [Finite n] :
+    Module.rank R (Matrix m n R) =
+      Cardinal.lift.{max v w u, v} (#m) * Cardinal.lift.{max v w u, w} (#n) := by
+  cases nonempty_fintype m
+  cases nonempty_fintype n
+  have h := (Matrix.stdBasis R m n).mk_eq_rank
+  rw [← lift_lift.{max v w u, max v w}, lift_inj] at h
+  simpa using h.symm
+#align rank_matrix rank_matrix
+
+/-- If `m` and `n` are `Fintype` that lie in the same universe, the rank of `m × n` matrices is
+  `(# n * # m).lift`. -/
+@[simp high]
+theorem rank_matrix' (m n : Type v) [Finite m] [Finite n] :
+    Module.rank R (Matrix m n R) = Cardinal.lift.{u} ((#m) * (#n)) := by
+  rw [rank_matrix, lift_mul, lift_umax.{v, u}]
+#align rank_matrix' rank_matrix'
+
+/-- If `m` and `n` are `Fintype` that lie in the same universe as `R`, the rank of `m × n` matrices
+  is `# m * # n`. -/
+-- @[simp] -- Porting note: simp can prove this
+theorem rank_matrix'' (m n : Type u) [Finite m] [Finite n] :
+    Module.rank R (Matrix m n R) = (#m) * (#n) := by simp
+#align rank_matrix'' rank_matrix''
+
+end Ring
+
+section CommRing
+
+variable [CommRing R] [StrongRankCondition R]
+
+variable [AddCommGroup M] [Module R M] [Module.Free R M]
+
+variable [AddCommGroup N] [Module R N] [Module.Free R N]
+
+open Module.Free
+
+/-- The rank of `M ⊗[R] N` is `(Module.rank R M).lift * (Module.rank R N).lift`. -/
+@[simp]
+theorem rank_tensorProduct :
+    Module.rank R (M ⊗[R] N) =
+      Cardinal.lift.{w, v} (Module.rank R M) * Cardinal.lift.{v, w} (Module.rank R N) := by
+  obtain ⟨⟨_, bM⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
+  obtain ⟨⟨_, bN⟩⟩ := Module.Free.exists_basis (R := R) (M := N)
+  rw [← bM.mk_eq_rank'', ← bN.mk_eq_rank'', ← (bM.tensorProduct bN).mk_eq_rank'', Cardinal.mk_prod]
+#align rank_tensor_product rank_tensorProduct
+
+/-- If `M` and `N` lie in the same universe, the rank of `M ⊗[R] N` is
+  `(Module.rank R M) * (Module.rank R N)`. -/
+theorem rank_tensor_product' (N : Type v) [AddCommGroup N] [Module R N] [Module.Free R N] :
+    Module.rank R (M ⊗[R] N) = Module.rank R M * Module.rank R N := by simp
+#align rank_tensor_product' rank_tensor_product'
+
+end CommRing

Mathlib/SetTheory/Cardinal/Basic.lean

@@ -238,7 +238,7 @@ theorem lift_uzero (a : Cardinal.{u}) : lift.{0} a = a :=
 #align cardinal.lift_uzero Cardinal.lift_uzero
 
 @[simp]
-theorem lift_lift (a : Cardinal) : lift.{w} (lift.{v} a) = lift.{max v w} a :=
+theorem lift_lift.{u_1} (a : Cardinal.{u_1}) : lift.{w} (lift.{v} a) = lift.{max v w} a :=
   inductionOn a fun _ => (Equiv.ulift.trans <| Equiv.ulift.trans Equiv.ulift.symm).cardinal_eq
 #align cardinal.lift_lift Cardinal.lift_lift
 
@@ -1161,7 +1161,7 @@ theorem lift_succ (a) : lift.{v,u} (succ a) = succ (lift.{v,u} a) :=
 @[simp, nolint simpNF]
 theorem lift_umax_eq {a : Cardinal.{u}} {b : Cardinal.{v}} :
     lift.{max v w} a = lift.{max u w} b ↔ lift.{v} a = lift.{u} b := by
-  rw [← lift_lift.{u,v,w}, ← lift_lift.{v,u,w}, lift_inj]
+  rw [← lift_lift.{v, w, u}, ← lift_lift.{u, w, v}, lift_inj]
 #align cardinal.lift_umax_eq Cardinal.lift_umax_eq
 
 -- Porting note: Inserted .{u,v} below

Mathlib/SetTheory/Cardinal/Cofinality.lean

@@ -766,7 +766,7 @@ theorem cof_univ : cof univ.{u, v} = Cardinal.univ.{u, v} :=
       refine' le_of_forall_lt fun c h => _
       rcases lt_univ'.1 h with ⟨c, rfl⟩
       rcases @cof_eq Ordinal.{u} (· < ·) _ with ⟨S, H, Se⟩
-      rw [univ, ← lift_cof, ← Cardinal.lift_lift.{u, u + 1, v}, Cardinal.lift_lt, ← Se]
+      rw [univ, ← lift_cof, ← Cardinal.lift_lift.{u+1, v, u}, Cardinal.lift_lt, ← Se]
       refine' lt_of_not_ge fun h => _
       cases' Cardinal.lift_down h with a e
       refine' Quotient.inductionOn a (fun α e => _) e