feat(linear_algebra/finite_dimensional): generalize results to module.finite (#18811)

eric-wieser · eric-wieser · commit e95e4f92c8f8 · 2023-04-14T22:49:11.000Z
This generalize the following from `finite_dimensional` over division rings to `module.finite` over free modules:
* `finite_dimensional.nonempty_linear_equiv_of_finrank_eq` (moved from `nonempty_linear_equiv_of_finrank_eq`)
* `finite_dimensional.nonempty_linear_equiv_iff_finrank_eq` (moved from `nonempty_linear_equiv_iff_finrank_eq`)
* `linear_equiv.of_finrank_eq`
* `module.finite.map` (moved from `finite_dimensional.submodule.map.finite_dimensional`). This is the only lemma moved across the porting tide.
* `submodule.finrank_map_le` (moved from `finite_dimensional.finrank_map_le`)
* `submodule.finrank_map_subtype_eq` (moved from `finite_dimensional.finrank_map_subtype_eq`, needs no finite or free assumptions at all)
* `submodule.finrank_le_finrank_of_le`
diff --git a/src/linear_algebra/bilinear_form.lean b/src/linear_algebra/bilinear_form.lean
@@ -1181,7 +1181,7 @@ lemma finrank_add_finrank_orthogonal
 begin
   rw [← to_lin_restrict_ker_eq_inf_orthogonal _ _ b₁,
       ← to_lin_restrict_range_dual_coannihilator_eq_orthogonal _ _,
-      finrank_map_subtype_eq],
+      submodule.finrank_map_subtype_eq],
   conv_rhs { rw [← @subspace.finrank_add_finrank_dual_coannihilator_eq K V _ _ _ _
                   (B.to_lin.dom_restrict W).range,
                  add_comm, ← add_assoc, add_comm (finrank K ↥((B.to_lin.dom_restrict W).ker)),
diff --git a/src/linear_algebra/finite_dimensional.lean b/src/linear_algebra/finite_dimensional.lean
@@ -358,18 +358,7 @@ span_of_finite K $ s.finite_to_set
 /-- Pushforwards of finite-dimensional submodules are finite-dimensional. -/
 instance (f : V →ₗ[K] V₂) (p : submodule K V) [h : finite_dimensional K p] :
   finite_dimensional K (p.map f) :=
-begin
-  unfreezingI { rw [finite_dimensional, ← iff_fg, is_noetherian.iff_rank_lt_aleph_0] at h ⊢ },
-  rw [← cardinal.lift_lt.{v' v}],
-  rw [← cardinal.lift_lt.{v v'}] at h,
-  rw [cardinal.lift_aleph_0] at h ⊢,
-  exact (lift_rank_map_le f p).trans_lt h
-end
-
-/-- Pushforwards of finite-dimensional submodules have a smaller finrank. -/
-lemma finrank_map_le (f : V →ₗ[K] V₂) (p : submodule K V) [finite_dimensional K p] :
-  finrank K (p.map f) ≤ finrank K p :=
-by simpa [← finrank_eq_rank', -finrank_eq_rank] using lift_rank_map_le f p
+module.finite.map _ _
 
 variable {K}
 
@@ -781,32 +770,6 @@ section division_ring
 variables [division_ring K] [add_comm_group V] [module K V]
 {V₂ : Type v'} [add_comm_group V₂] [module K V₂]
 
-/--
-Two finite-dimensional vector spaces are isomorphic if they have the same (finite) dimension.
--/
-theorem nonempty_linear_equiv_of_finrank_eq [finite_dimensional K V] [finite_dimensional K V₂]
-  (cond : finrank K V = finrank K V₂) : nonempty (V ≃ₗ[K] V₂) :=
-nonempty_linear_equiv_of_lift_rank_eq $ by simp only [← finrank_eq_rank, cond, lift_nat_cast]
-
-/--
-Two finite-dimensional vector spaces are isomorphic if and only if they have the same (finite)
-dimension.
--/
-theorem nonempty_linear_equiv_iff_finrank_eq [finite_dimensional K V] [finite_dimensional K V₂] :
-  nonempty (V ≃ₗ[K] V₂) ↔ finrank K V = finrank K V₂ :=
-⟨λ ⟨h⟩, h.finrank_eq, λ h, nonempty_linear_equiv_of_finrank_eq h⟩
-
-variables (V V₂)
-
-/--
-Two finite-dimensional vector spaces are isomorphic if they have the same (finite) dimension.
--/
-noncomputable def linear_equiv.of_finrank_eq [finite_dimensional K V] [finite_dimensional K V₂]
-  (cond : finrank K V = finrank K V₂) : V ≃ₗ[K] V₂ :=
-classical.choice $ nonempty_linear_equiv_of_finrank_eq cond
-
-variables {V}
-
 lemma eq_of_le_of_finrank_le {S₁ S₂ : submodule K V} [finite_dimensional K S₂] (hle : S₁ ≤ S₂)
   (hd : finrank K S₂ ≤ finrank K S₁) : S₁ = S₂ :=
 begin
@@ -821,12 +784,7 @@ lemma eq_of_le_of_finrank_eq {S₁ S₂ : submodule K V} [finite_dimensional K S
   (hd : finrank K S₁ = finrank K S₂) : S₁ = S₂ :=
 eq_of_le_of_finrank_le hle hd.ge
 
-@[simp]
-lemma finrank_map_subtype_eq (p : submodule K V) (q : submodule K p) :
-  finite_dimensional.finrank K (q.map p.subtype) = finite_dimensional.finrank K q :=
-(submodule.equiv_subtype_map p q).symm.finrank_eq
-
-variables {V₂} [finite_dimensional K V] [finite_dimensional K V₂]
+variables [finite_dimensional K V] [finite_dimensional K V₂]
 
 /-- Given isomorphic subspaces `p q` of vector spaces `V` and `V₁` respectively,
   `p.quotient` is isomorphic to `q.quotient`. -/
@@ -1054,11 +1012,6 @@ lemma eq_top_of_finrank_eq [finite_dimensional K V] {S : submodule K V}
   (h : finrank K S = finrank K V) :
   S = ⊤ := finite_dimensional.eq_of_le_of_finrank_eq le_top (by simp [h, finrank_top])
 
-lemma finrank_le_finrank_of_le {s t : submodule K V} [finite_dimensional K t]
-  (hst : s ≤ t) : finrank K s ≤ finrank K t :=
-calc  finrank K s = finrank K (comap t.subtype s) : (comap_subtype_equiv_of_le hst).finrank_eq.symm
-... ≤ finrank K t : finrank_le _
-
 lemma finrank_mono [finite_dimensional K V] :
   monotone (λ (s : submodule K V), finrank K s) :=
 λ s t, finrank_le_finrank_of_le
diff --git a/src/linear_algebra/free_module/finite/rank.lean b/src/linear_algebra/free_module/finite/rank.lean
@@ -30,6 +30,18 @@ namespace finite_dimensional
 open module.free
 
 section ring
+variables [ring R]
+variables [add_comm_group M] [module R M]
+variables [add_comm_group N] [module R N]
+
+@[simp]
+lemma submodule.finrank_map_subtype_eq (p : submodule R M) (q : submodule R p) :
+  finrank R (q.map p.subtype) = finrank R q :=
+(submodule.equiv_subtype_map p q).symm.finrank_eq
+
+end ring
+
+section ring_finite
 
 variables [ring R] [strong_rank_condition R]
 variables [add_comm_group M] [module R M] [module.finite R M]
@@ -49,7 +61,7 @@ end
 @[simp] lemma finrank_eq_rank : ↑(finrank R M) = module.rank R M :=
 by { rw [finrank, cast_to_nat_of_lt_aleph_0 (rank_lt_aleph_0 R M)] }
 
-end ring
+end ring_finite
 
 section ring_free
 
@@ -104,6 +116,25 @@ lemma finrank_matrix (m n : Type*) [fintype m] [fintype n] :
   finrank R (matrix m n R) = (card m) * (card n) :=
 by { simp [finrank] }
 
+variables {R M N}
+
+/-- Two finite and free modules are isomorphic if they have the same (finite) rank. -/
+theorem nonempty_linear_equiv_of_finrank_eq
+  (cond : finrank R M = finrank R N) : nonempty (M ≃ₗ[R] N) :=
+nonempty_linear_equiv_of_lift_rank_eq $ by simp only [← finrank_eq_rank, cond, lift_nat_cast]
+
+/-- Two finite and free modules are isomorphic if and only if they have the same (finite) rank. -/
+theorem nonempty_linear_equiv_iff_finrank_eq :
+  nonempty (M ≃ₗ[R] N) ↔ finrank R M = finrank R N :=
+⟨λ ⟨h⟩, h.finrank_eq, λ h, nonempty_linear_equiv_of_finrank_eq h⟩
+
+variables (M N)
+
+/-- Two finite and free modules are isomorphic if they have the same (finite) rank. -/
+noncomputable def _root_.linear_equiv.of_finrank_eq (cond : finrank R M = finrank R N) :
+  M ≃ₗ[R] N :=
+classical.choice $ nonempty_linear_equiv_of_finrank_eq cond
+
 end ring_free
 
 section comm_ring
@@ -115,7 +146,7 @@ variables [add_comm_group N] [module R N] [module.free R N] [module.finite R N]
 /-- The finrank of `M ⊗[R] N` is `(finrank R M) * (finrank R N)`. -/
 @[simp] lemma finrank_tensor_product (M : Type v) (N : Type w) [add_comm_group M] [module R M]
   [module.free R M] [add_comm_group N] [module R N] [module.free R N] :
-finrank R (M ⊗[R] N) = (finrank R M) * (finrank R N) :=
+  finrank R (M ⊗[R] N) = (finrank R M) * (finrank R N) :=
 by { simp [finrank] }
 
 end comm_ring
@@ -151,4 +182,15 @@ lemma submodule.finrank_quotient_le [module.finite R M] (s : submodule R M) :
 by simpa only [cardinal.to_nat_lift] using to_nat_le_of_le_of_lt_aleph_0
   (rank_lt_aleph_0 _ _) ((submodule.mkq s).rank_le_of_surjective (surjective_quot_mk _))
 
+/-- Pushforwards of finite submodules have a smaller finrank. -/
+lemma submodule.finrank_map_le (f : M →ₗ[R] N) (p : submodule R M) [module.finite R p] :
+  finrank R (p.map f) ≤ finrank R p :=
+finrank_le_finrank_of_rank_le_rank (lift_rank_map_le _ _) (rank_lt_aleph_0 _ _)
+
+lemma submodule.finrank_le_finrank_of_le {s t : submodule R M} [module.finite R t]
+  (hst : s ≤ t) : finrank R s ≤ finrank R t :=
+calc finrank R s = finrank R (s.comap t.subtype)
+      : (submodule.comap_subtype_equiv_of_le hst).finrank_eq.symm
+... ≤ finrank R t : submodule.finrank_le _
+
 end
diff --git a/src/ring_theory/finiteness.lean b/src/ring_theory/finiteness.lean
@@ -479,6 +479,10 @@ end⟩
 instance range [finite R M] (f : M →ₗ[R] N) : finite R f.range :=
 of_surjective f.range_restrict $ λ ⟨x, y, hy⟩, ⟨y, subtype.ext hy⟩
 
+/-- Pushforwards of finite submodules are finite. -/
+instance map (p : submodule R M) [finite R p] (f : M →ₗ[R] N) : finite R (p.map f) :=
+of_surjective (f.restrict $ λ _, mem_map_of_mem) $ λ ⟨x, y, hy, hy'⟩, ⟨⟨_, hy⟩, subtype.ext hy'⟩
+
 variables (R)
 
 instance self : finite R R :=
