feat(field_theory/tower): generalize rank_mul_rank to rings (#18885)

eric-wieser · eric-wieser · commit c7bce2818663 · 2023-04-28T14:14:17.000Z
This also renames `rank_mul_rank` to `lift_rank_mul_lift_rank`
diff --git a/src/data/complex/module.lean b/src/data/complex/module.lean
@@ -198,7 +198,7 @@ finite_dimensional.trans ℝ ℂ E
 lemma rank_real_of_complex (E : Type*) [add_comm_group E] [module ℂ E] :
   module.rank ℝ E = 2 * module.rank ℂ E :=
 cardinal.lift_inj.1 $
-  by { rw [← rank_mul_rank' ℝ ℂ E, complex.rank_real_complex], simp [bit0] }
+  by { rw [← lift_rank_mul_lift_rank ℝ ℂ E, complex.rank_real_complex], simp [bit0] }
 
 lemma finrank_real_of_complex (E : Type*) [add_comm_group E] [module ℂ E] :
   finite_dimensional.finrank ℝ E = 2 * finite_dimensional.finrank ℂ E :=
diff --git a/src/field_theory/tower.lean b/src/field_theory/tower.lean
@@ -16,8 +16,8 @@ In this file we prove the tower law for arbitrary extensions and finite extensio
 Suppose `L` is a field extension of `K` and `K` is a field extension of `F`.
 Then `[L:F] = [L:K] [K:F]` where `[E₁:E₂]` means the `E₂`-dimension of `E₁`.
 
-In fact we generalize it to vector spaces, where `L` is not necessarily a field,
-but just a vector space over `K`.
+In fact we generalize it to rings and modules, where `L` is not necessarily a field,
+but just a free module over `K`.
 
 ## Implementation notes
 
@@ -34,31 +34,60 @@ tower law
 universes u v w u₁ v₁ w₁
 open_locale classical big_operators
 
-section field
-
+open finite_dimensional
 open cardinal
 
 variables (F : Type u) (K : Type v) (A : Type w)
-variables [field F] [division_ring K] [add_comm_group A]
+
+section ring
+
+variables [comm_ring F] [ring K] [add_comm_group A]
 variables [algebra F K] [module K A] [module F A] [is_scalar_tower F K A]
+variables [strong_rank_condition F] [strong_rank_condition K] [module.free F K] [module.free K A]
 
-/-- Tower law: if `A` is a `K`-vector space and `K` is a field extension of `F` then
-`dim_F(A) = dim_F(K) * dim_K(A)`. -/
-theorem rank_mul_rank' :
+/-- Tower law: if `A` is a `K`-module and `K` is an extension of `F` then
+$\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$. -/
+theorem lift_rank_mul_lift_rank :
   (cardinal.lift.{w} (module.rank F K) * cardinal.lift.{v} (module.rank K A)) =
   cardinal.lift.{v} (module.rank F A) :=
-let b := basis.of_vector_space F K, c := basis.of_vector_space K A in
-by rw [← (module.rank F K).lift_id, ← b.mk_eq_rank,
-    ← (module.rank K A).lift_id, ← c.mk_eq_rank,
-    ← lift_umax.{w v}, ← (b.smul c).mk_eq_rank, mk_prod, lift_mul,
-    lift_lift, lift_lift, lift_lift, lift_lift, lift_umax]
+begin
+  obtain ⟨_, b⟩ := module.free.exists_basis F K,
+  obtain ⟨_, c⟩ := module.free.exists_basis K A,
+  rw [← (module.rank F K).lift_id, ← b.mk_eq_rank,
+      ← (module.rank K A).lift_id, ← c.mk_eq_rank,
+      ← lift_umax.{w v}, ← (b.smul c).mk_eq_rank, mk_prod, lift_mul,
+      lift_lift, lift_lift, lift_lift, lift_lift, lift_umax]
+end
 
-/-- Tower law: if `A` is a `K`-vector space and `K` is a field extension of `F` then
-`dim_F(A) = dim_F(K) * dim_K(A)`. -/
-theorem rank_mul_rank (F : Type u) (K A : Type v) [field F] [field K] [add_comm_group A]
-  [algebra F K] [module K A] [module F A] [is_scalar_tower F K A] :
+/-- Tower law: if `A` is a `K`-module and `K` is an extension of `F` then
+$\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$.
+
+This is a simpler version of `lift_rank_mul_lift_rank` with `K` and `A` in the same universe. -/
+theorem rank_mul_rank (F : Type u) (K A : Type v)
+  [comm_ring F] [ring K] [add_comm_group A]
+  [algebra F K] [module K A] [module F A] [is_scalar_tower F K A]
+  [strong_rank_condition F] [strong_rank_condition K] [module.free F K] [module.free K A] :
   module.rank F K * module.rank K A = module.rank F A :=
-by convert rank_mul_rank' F K A; rw lift_id
+by convert lift_rank_mul_lift_rank F K A; rw lift_id
+
+/-- Tower law: if `A` is a `K`-module and `K` is an extension of `F` then
+$\operatorname{rank}_F(A) = \operatorname{rank}_F(K) * \operatorname{rank}_K(A)$. -/
+theorem finite_dimensional.finrank_mul_finrank'
+  [nontrivial K] [module.finite F K] [module.finite K A] :
+  finrank F K * finrank K A = finrank F A :=
+begin
+  letI := nontrivial_of_invariant_basis_number F,
+  let b := module.free.choose_basis F K,
+  let c := module.free.choose_basis K A,
+  rw [finrank_eq_card_basis b, finrank_eq_card_basis c, finrank_eq_card_basis (b.smul c),
+    fintype.card_prod],
+end
+
+end ring
+
+section field
+variables [field F] [division_ring K] [add_comm_group A]
+variables [algebra F K] [module K A] [module F A] [is_scalar_tower F K A]
 
 namespace finite_dimensional
 
@@ -85,17 +114,15 @@ let ⟨⟨b, hb⟩⟩ := hf in ⟨⟨b, submodule.restrict_scalars_injective F _
 by { rw [submodule.restrict_scalars_top, eq_top_iff, ← hb, submodule.span_le],
   exact submodule.subset_span }⟩⟩
 
-/-- Tower law: if `A` is a `K`-algebra and `K` is a field extension of `F` then
-`dim_F(A) = dim_F(K) * dim_K(A)`. -/
-theorem finrank_mul_finrank [finite_dimensional F K] :
-  finrank F K * finrank K A = finrank F A :=
+/-- Tower law: if `A` is a `K`-vector space and `K` is a field extension of `F` then
+`dim_F(A) = dim_F(K) * dim_K(A)`.
+
+This is `finite_dimensional.finrank_mul_finrank'` with one fewer finiteness assumption. -/
+theorem finrank_mul_finrank [finite_dimensional F K] : finrank F K * finrank K A = finrank F A :=
 begin
   by_cases hA : finite_dimensional K A,
   { resetI,
-    let b := basis.of_vector_space F K,
-    let c := basis.of_vector_space K A,
-    rw [finrank_eq_card_basis b, finrank_eq_card_basis c,
-      finrank_eq_card_basis (b.smul c), fintype.card_prod] },
+    rw finrank_mul_finrank' },
   { rw [finrank_of_infinite_dimensional hA, mul_zero, finrank_of_infinite_dimensional],
     exact mt (@right F K A _ _ _ _ _ _ _) hA }
 end
