Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 5aa3c1d

Browse files
eric-wiesereric-wieser
committed
chore(linear_algebra/dimension): deduplicate lemmas (#18743)
We have some lemmas in the `module.free` namespace which duplicate lemmas in the root namespace. This moves all the remaining `rank` lemmas in this namespace into the root namespace, and cleans up the overlapping lemmas this creates. The changes are: * `module.free.rank_eq_card_choose_basis_index`: unchanged but moved to an earlier file * `rank_prod` → `rank_prod'` (the non-universe polymorphic version) * `module.free.rank_prod` → `rank_prod` * none → `rank_finsupp` (new lemma) * `finsupp.rank_eq` → `rank_finsupp'` (the non-universe polymorphic version) * `module.free.rank_finsupp` → `rank_finsupp_self` * `module.free.rank_finsupp'` → `rank_finsupp_self'` (the non-universe polymorphic version) * `module.free.rank_pi_finite` → `rank_pi` (these were duplicates) * For everything else, `module.free.rank_*` → `rank_*`
1 parent 75be6b6 commit 5aa3c1d

4 files changed

Lines changed: 53 additions & 66 deletions

File tree

‎src/field_theory/finite/polynomial.lean‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -182,8 +182,7 @@ calc module.rank K (R σ K) =
182182
module.rank K (↥{s : σ →₀ ℕ | ∀ (n : σ), s n ≤ fintype.card K - 1} →₀ K) :
183183
linear_equiv.rank_eq
184184
(finsupp.supported_equiv_finsupp {s : σ →₀ ℕ | ∀n:σ, s n ≤ fintype.card K - 1 })
185-
... = #{s : σ →₀ ℕ | ∀ (n : σ), s n ≤ fintype.card K - 1} :
186-
by rw [finsupp.rank_eq, rank_self, mul_one]
185+
... = #{s : σ →₀ ℕ | ∀ (n : σ), s n ≤ fintype.card K - 1} : by rw [rank_finsupp_self']
187186
... = #{s : σ → ℕ | ∀ (n : σ), s n < fintype.card K } :
188187
begin
189188
refine quotient.sound ⟨equiv.subtype_equiv finsupp.equiv_fun_on_finite $ assume f, _⟩,

‎src/linear_algebra/dimension.lean‎

Lines changed: 31 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -942,6 +942,19 @@ variables [add_comm_group V'] [module K V'] [module.free K V']
942942
variables [add_comm_group V₁] [module K V₁] [module.free K V₁]
943943
variables {K V}
944944

945+
946+
namespace module.free
947+
variables (K V)
948+
949+
/-- The rank of a free module `M` over `R` is the cardinality of `choose_basis_index R M`. -/
950+
lemma rank_eq_card_choose_basis_index : module.rank K V = #(choose_basis_index K V) :=
951+
(choose_basis K V).mk_eq_rank''.symm
952+
953+
end module.free
954+
955+
open module.free
956+
open cardinal
957+
945958
/-- Two vector spaces are isomorphic if they have the same dimension. -/
946959
theorem nonempty_linear_equiv_of_lift_rank_eq
947960
(cond : cardinal.lift.{v'} (module.rank K V) = cardinal.lift.{v} (module.rank K V')) :
@@ -987,35 +1000,31 @@ theorem linear_equiv.nonempty_equiv_iff_rank_eq :
9871000
nonempty (V ≃ₗ[K] V₁) ↔ module.rank K V = module.rank K V₁ :=
9881001
⟨λ ⟨h⟩, linear_equiv.rank_eq h, λ h, nonempty_linear_equiv_of_rank_eq h⟩
9891002

990-
theorem rank_prod : module.rank K (V × V₁) = module.rank K V + module.rank K V₁ :=
991-
begin
992-
obtain ⟨⟨_, b⟩⟩ := module.free.exists_basis K V,
993-
obtain ⟨⟨_, c⟩⟩ := module.free.exists_basis K V₁,
994-
rw [← cardinal.lift_inj,
995-
← (basis.prod b c).mk_eq_rank,
996-
cardinal.lift_add, ← cardinal.mk_ulift,
997-
← b.mk_eq_rank, ← c.mk_eq_rank,
998-
← cardinal.mk_ulift, ← cardinal.mk_ulift,
999-
cardinal.add_def (ulift _)],
1000-
exact cardinal.lift_inj.1 (cardinal.lift_mk_eq.2
1001-
⟨equiv.ulift.trans (equiv.sum_congr equiv.ulift equiv.ulift).symm ⟩),
1002-
end
1003+
/-- The rank of `M × N` is `(module.rank R M).lift + (module.rank R N).lift`. -/
1004+
@[simp] lemma rank_prod :
1005+
module.rank K (V × V') =
1006+
cardinal.lift.{v'} (module.rank K V) + cardinal.lift.{v v'} (module.rank K V') :=
1007+
by simpa [rank_eq_card_choose_basis_index K V, rank_eq_card_choose_basis_index K V',
1008+
lift_umax, lift_umax'] using ((choose_basis K V).prod (choose_basis K V')).mk_eq_rank.symm
1009+
1010+
/-- If `M` and `N` lie in the same universe, the rank of `M × N` is
1011+
`(module.rank R M) + (module.rank R N)`. -/
1012+
theorem rank_prod' : module.rank K (V × V₁) = module.rank K V + module.rank K V₁ :=
1013+
by simp
10031014

10041015
section fintype
10051016
variables [∀i, add_comm_group (φ i)] [∀i, module K (φ i)] [∀i, module.free K (φ i)]
10061017

10071018
open linear_map
10081019

1009-
lemma rank_pi [finite η] :
1020+
/-- The rank of a finite product is the sum of the ranks. -/
1021+
@[simp] lemma rank_pi [finite η] :
10101022
module.rank K (Πi, φ i) = cardinal.sum (λi, module.rank K (φ i)) :=
10111023
begin
1012-
haveI := nontrivial_of_invariant_basis_number K,
10131024
casesI nonempty_fintype η,
1014-
let b := λ i, (module.free.exists_basis K (φ i)).some.2,
1015-
let this : basis (Σ j, _) K (Π j, φ j) := pi.basis b,
1016-
rw [← cardinal.lift_inj, ← this.mk_eq_rank],
1017-
simp_rw [cardinal.mk_sigma, cardinal.lift_sum, ←(b _).mk_range_eq_rank,
1018-
cardinal.mk_range_eq _ (b _).injective],
1025+
let B := λ i, choose_basis K (φ i),
1026+
let b : basis _ K (Π i, φ i) := pi.basis (λ i, B i),
1027+
simp [← b.mk_eq_rank'', λ i, (B i).mk_eq_rank''],
10191028
end
10201029

10211030
variable [fintype η]
@@ -1038,13 +1047,6 @@ by simp [rank_fun']
10381047

10391048
end fintype
10401049

1041-
lemma finsupp.rank_eq {ι : Type v} : module.rank K (ι →₀ V) = #ι * module.rank K V :=
1042-
begin
1043-
obtain ⟨⟨_, bs⟩⟩ := module.free.exists_basis K V,
1044-
rw [← bs.mk_eq_rank'', ← (finsupp.basis (λa:ι, bs)).mk_eq_rank'',
1045-
cardinal.mk_sigma, cardinal.sum_const']
1046-
end
1047-
10481050
-- TODO: merge with the `finrank` content
10491051
/-- An `n`-dimensional `K`-vector space is equivalent to `fin n → K`. -/
10501052
def fin_dim_vectorspace_equiv (n : ℕ)
@@ -1092,7 +1094,7 @@ calc module.rank K (span K (↑s : set V)) ≤ #(↑s : set V) : rank_span_le
10921094

10931095
theorem rank_quotient_add_rank (p : submodule K V) :
10941096
module.rank K (V ⧸ p) + module.rank K p = module.rank K V :=
1095-
by classical; exact let ⟨f⟩ := quotient_prod_linear_equiv p in rank_prod.symm.trans f.rank_eq
1097+
by classical; exact let ⟨f⟩ := quotient_prod_linear_equiv p in rank_prod'.symm.trans f.rank_eq
10961098

10971099
/-- rank-nullity theorem -/
10981100
theorem rank_range_add_rank_ker (f : V →ₗ[K] V₁) :
@@ -1122,7 +1124,7 @@ lemma rank_add_rank_split
11221124
have hf : surjective (coprod db eb),
11231125
by rwa [←range_eq_top, range_coprod, eq_top_iff],
11241126
begin
1125-
conv {to_rhs, rw [← rank_prod, rank_eq_of_surjective _ hf] },
1127+
conv {to_rhs, rw [← rank_prod', rank_eq_of_surjective _ hf] },
11261128
congr' 1,
11271129
apply linear_equiv.rank_eq,
11281130
refine linear_equiv.of_bijective _ ⟨_, _⟩,

‎src/linear_algebra/free_module/finite/rank.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -57,7 +57,7 @@ end
5757

5858
/-- The finrank of `(ι →₀ R)` is `fintype.card ι`. -/
5959
@[simp] lemma finrank_finsupp {ι : Type v} [fintype ι] : finrank R (ι →₀ R) = card ι :=
60-
by { rw [finrank, rank_finsupp, ← mk_to_nat_eq_card, to_nat_lift] }
60+
by { rw [finrank, rank_finsupp_self, ← mk_to_nat_eq_card, to_nat_lift] }
6161

6262
/-- The finrank of `(ι → R)` is `fintype.card ι`. -/
6363
lemma finrank_pi {ι : Type v} [fintype ι] : finrank R (ι → R) = card ι :=
@@ -84,7 +84,7 @@ lemma finrank_pi_fintype {ι : Type v} [fintype ι] {M : ι → Type w}
8484
[Π (i : ι), module.finite R (M i)] : finrank R (Π i, M i) = ∑ i, finrank R (M i) :=
8585
begin
8686
letI := nontrivial_of_invariant_basis_number R,
87-
simp only [finrank, λ i, rank_eq_card_choose_basis_index R (M i), rank_pi_finite,
87+
simp only [finrank, λ i, rank_eq_card_choose_basis_index R (M i), rank_pi,
8888
← mk_sigma, mk_to_nat_eq_card, card_sigma],
8989
end
9090

‎src/linear_algebra/free_module/rank.lean‎

Lines changed: 19 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -5,14 +5,12 @@ Authors: Riccardo Brasca
55
-/
66

77
import linear_algebra.dimension
8-
import linear_algebra.free_module.basic
9-
import linear_algebra.invariant_basis_number
108

119
/-!
1210
13-
# Rank of free modules
11+
# Extra results about `module.rank`
1412
15-
This is a basic API for the rank of free modules.
13+
This file contains some extra results not in `linear_algebra.dimension`.
1614
1715
-/
1816

@@ -24,36 +22,31 @@ open_locale tensor_product direct_sum big_operators cardinal
2422

2523
open cardinal
2624

27-
namespace module.free
28-
2925
section ring
3026

3127
variables [ring R] [strong_rank_condition R]
3228
variables [add_comm_group M] [module R M] [module.free R M]
3329
variables [add_comm_group N] [module R N] [module.free R N]
3430

35-
/-- The rank of a free module `M` over `R` is the cardinality of `choose_basis_index R M`. -/
36-
lemma rank_eq_card_choose_basis_index : module.rank R M = #(choose_basis_index R M) :=
37-
(choose_basis R M).mk_eq_rank''.symm
31+
open module.free
3832

39-
/-- The rank of `(ι →₀ R)` is `(# ι).lift`. -/
40-
@[simp] lemma rank_finsupp {ι : Type v} : module.rank R (ι →₀ R) = (# ι).lift :=
41-
by simpa [lift_id', lift_umax] using
42-
(basis.of_repr (linear_equiv.refl _ (ι →₀ R))).mk_eq_rank.symm
33+
@[simp] lemma rank_finsupp (ι : Type w) :
34+
module.rank R (ι →₀ M) = cardinal.lift.{v} #ι * cardinal.lift.{w} (module.rank R M) :=
35+
begin
36+
obtain ⟨⟨_, bs⟩⟩ := module.free.exists_basis R M,
37+
rw [← bs.mk_eq_rank'', ← (finsupp.basis (λa:ι, bs)).mk_eq_rank'',
38+
cardinal.mk_sigma, cardinal.sum_const]
39+
end
4340

44-
/-- If `R` and `ι` lie in the same universe, the rank of `(ι →₀ R)` is `# ι`. -/
45-
lemma rank_finsupp' {ι : Type u} : module.rank R (ι →₀ R) = # ι := by simp
41+
lemma rank_finsupp' (ι : Type v) : module.rank R (ι →₀ M) = #ι * module.rank R M :=
42+
by simp [rank_finsupp]
4643

47-
/-- The rank of `M × N` is `(module.rank R M).lift + (module.rank R N).lift`. -/
48-
@[simp] lemma rank_prod :
49-
module.rank R (M × N) = lift.{w v} (module.rank R M) + lift.{v w} (module.rank R N) :=
50-
by simpa [rank_eq_card_choose_basis_index R M, rank_eq_card_choose_basis_index R N,
51-
lift_umax, lift_umax'] using ((choose_basis R M).prod (choose_basis R N)).mk_eq_rank.symm
44+
/-- The rank of `(ι →₀ R)` is `(# ι).lift`. -/
45+
@[simp] lemma rank_finsupp_self (ι : Type w) : module.rank R (ι →₀ R) = (# ι).lift :=
46+
by simp [rank_finsupp]
5247

53-
/-- If `M` and `N` lie in the same universe, the rank of `M × N` is
54-
`(module.rank R M) + (module.rank R N)`. -/
55-
lemma rank_prod' (N : Type v) [add_comm_group N] [module R N] [module.free R N] :
56-
module.rank R (M × N) = (module.rank R M) + (module.rank R N) := by simp
48+
/-- If `R` and `ι` lie in the same universe, the rank of `(ι →₀ R)` is `# ι`. -/
49+
lemma rank_finsupp_self' {ι : Type u} : module.rank R (ι →₀ R) = # ι := by simp
5750

5851
/-- The rank of the direct sum is the sum of the ranks. -/
5952
@[simp] lemma rank_direct_sum {ι : Type v} (M : ι → Type w) [Π (i : ι), add_comm_group (M i)]
@@ -65,13 +58,6 @@ begin
6558
simp [← b.mk_eq_rank'', λ i, (B i).mk_eq_rank''],
6659
end
6760

68-
/-- The rank of a finite product is the sum of the ranks. -/
69-
@[simp] lemma rank_pi_finite {ι : Type v} [finite ι] {M : ι → Type w}
70-
[Π (i : ι), add_comm_group (M i)] [Π (i : ι), module R (M i)] [Π (i : ι), module.free R (M i)] :
71-
module.rank R (Π i, M i) = cardinal.sum (λ i, module.rank R (M i)) :=
72-
by { casesI nonempty_fintype ι,
73-
rw [←(direct_sum.linear_equiv_fun_on_fintype _ _ M).rank_eq, rank_direct_sum] }
74-
7561
/-- If `m` and `n` are `fintype`, the rank of `m × n` matrices is `(# m).lift * (# n).lift`. -/
7662
@[simp] lemma rank_matrix (m : Type v) (n : Type w) [finite m] [finite n] :
7763
module.rank R (matrix m n R) = (lift.{(max v w u) v} (# m)) * (lift.{(max v w u) w} (# n)) :=
@@ -102,6 +88,8 @@ variables [comm_ring R] [strong_rank_condition R]
10288
variables [add_comm_group M] [module R M] [module.free R M]
10389
variables [add_comm_group N] [module R N] [module.free R N]
10490

91+
open module.free
92+
10593
/-- The rank of `M ⊗[R] N` is `(module.rank R M).lift * (module.rank R N).lift`. -/
10694
@[simp] lemma rank_tensor_product : module.rank R (M ⊗[R] N) = lift.{w v} (module.rank R M) *
10795
lift.{v w} (module.rank R N) :=
@@ -121,5 +109,3 @@ lemma rank_tensor_product' (N : Type v) [add_comm_group N] [module R N] [module.
121109
module.rank R (M ⊗[R] N) = (module.rank R M) * (module.rank R N) := by simp
122110

123111
end comm_ring
124-
125-
end module.free

0 commit comments

Comments
 (0)