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

Commit c4658a6

Browse files
alreadydonexroblot
alreadydone
and
xroblot
committed
feat(linear_algebra/finite_dimensional): generalize from field to division_ring and more (#17401)
+ Replace K by ℕ in two proofs in *linear_algebra/basis*, which immediately allows generalization from `division_ring` to `field` in *submodule/basic*, *field_theory/tower*, *linear_algebra/dimension*, *projective_space/basic*, *linear_algebra/finite_dimensional*, and *affine_space/finite_dimensional*. (~~@riccardobrasca authored many of these;~~ @semorrison made some `division_ring` generalizations a while ago; @adamtopaz's TODO in *projective_space/basic* is now resolved. Let me know if you can think of more stuff to generalize.) + Add `subalgebra.is_simple_order_of_finrank_prime` in *field_theory/tower*. Inspired by [#17237](#17237 (comment)) (@xroblot). + Make `subalgebra.to_submodule` an `order_embedding` in *subalgebra/basic*, remove lemmas rendered redundant, and fix things in *intermediate_field*, *field_theory/normal*, and *adjoin/fg*. + Changes in *linear_algebra/finite_dimensional* and *linear_algebra/finrank*: + Add `finite_dimensional_of_dim_eq_nat`: used to golf `finite_dimensional_of_dim_eq_zero/one`. + Add `submodule.finrank_le_finrank_of_le` and `finrank_lt_finrank_of_lt` which only assumes the larger submodule is finite rather than the whole module. Rename the original `finrank_lt_finrank_of_lt` to `finrank_strict_mono`, matching the existing `finrank_mono`. + Remove `subalgebra.dim/finrank_eq_one_of_eq_bot` which has a substitutable equality among its assumptions (use `dim/finrank_bot` instead). + Add `subalgebra.dim/finrank/finite_dimensional_to_submodule` and an instance `finite_dimensional_subalgebra` similar to [finite_dimensional_submodule](https://leanprover-community.github.io/mathlib_docs/linear_algebra/finite_dimensional.html#finite_dimensional.finite_dimensional_submodule). + Generalize `section subalgebra_dim` from `[field E]` to `[ring E]`, adding `[nontrivial E]` hypothesis whenever necessary. + Generalize `subalgebra.eq_bot_of_dim_one` to `of_dim_le_one` and golf the proof (together with `eq_bot_of_finrank_one`). + Move `finite_dimensional.of_subalgebra_to_submodule` from *splitting_field* to *finite_dimensional*. + Add `exists_nat_eq_of_le_nat` in *cardinal/basic*. + Fix a slow proof in *polynomial/bernstein*. Co-authored-by: Xavier-François Roblot <46200072+xroblot@users.noreply.github.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
1 parent bc5c9b4 commit c4658a6

16 files changed

Lines changed: 191 additions & 251 deletions

File tree

‎src/algebra/algebra/subalgebra/basic.lean‎

Lines changed: 14 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -219,25 +219,24 @@ instance to_linear_ordered_comm_ring {R A}
219219

220220
end
221221

222-
/-- Convert a `subalgebra` to `submodule` -/
223-
def to_submodule : submodule R A :=
224-
{ carrier := S,
225-
zero_mem' := (0:S).2,
226-
add_mem' := λ x y hx hy, (⟨x, hx⟩ + ⟨y, hy⟩ : S).2,
227-
smul_mem' := λ c x hx, (algebra.smul_def c x).symm ▸
228-
(⟨algebra_map R A c, S.range_le ⟨c, rfl⟩⟩ * ⟨x, hx⟩:S).2 }
222+
/-- The forgetful map from `subalgebra` to `submodule` as an `order_embedding` -/
223+
def to_submodule : subalgebra R A ↪o submodule R A :=
224+
{ to_embedding :=
225+
{ to_fun := λ S,
226+
{ carrier := S,
227+
zero_mem' := (0:S).2,
228+
add_mem' := λ x y hx hy, (⟨x, hx⟩ + ⟨y, hy⟩ : S).2,
229+
smul_mem' := λ c x hx, (algebra.smul_def c x).symm ▸
230+
(⟨algebra_map R A c, S.range_le ⟨c, rfl⟩⟩ * ⟨x, hx⟩:S).2 },
231+
inj' := λ S T h, ext $ by apply set_like.ext_iff.1 h },
232+
map_rel_iff' := λ S T, set_like.coe_subset_coe.symm.trans set_like.coe_subset_coe }
233+
/- TODO: bundle other forgetful maps between algebraic substructures, e.g.
234+
`to_subsemiring` and `to_subring` in this file. -/
229235

230236
@[simp] lemma mem_to_submodule {x} : x ∈ S.to_submodule ↔ x ∈ S := iff.rfl
231237

232238
@[simp] lemma coe_to_submodule (S : subalgebra R A) : (↑S.to_submodule : set A) = S := rfl
233239

234-
theorem to_submodule_injective :
235-
function.injective (to_submodule : subalgebra R A → submodule R A) :=
236-
λ S T h, ext $ λ x, by rw [← mem_to_submodule, ← mem_to_submodule, h]
237-
238-
theorem to_submodule_inj {S U : subalgebra R A} : S.to_submodule = U.to_submodule ↔ S = U :=
239-
to_submodule_injective.eq_iff
240-
241240
section
242241

243242
/-! `subalgebra`s inherit structure from their `submodule` coercions. -/
@@ -573,7 +572,7 @@ set.mem_univ x
573572
(⊤ : subalgebra R A).to_subring = ⊤ := rfl
574573

575574
@[simp] lemma to_submodule_eq_top {S : subalgebra R A} : S.to_submodule = ⊤ ↔ S = ⊤ :=
576-
subalgebra.to_submodule_injective.eq_iff' top_to_submodule
575+
subalgebra.to_submodule.injective.eq_iff' top_to_submodule
577576

578577
@[simp] lemma to_subsemiring_eq_top {S : subalgebra R A} : S.to_subsemiring = ⊤ ↔ S = ⊤ :=
579578
subalgebra.to_subsemiring_injective.eq_iff' top_to_subsemiring

‎src/algebra/module/submodule/basic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -462,5 +462,5 @@ end submodule
462462

463463
/-- Subspace of a vector space. Defined to equal `submodule`. -/
464464
abbreviation subspace (R : Type u) (M : Type v)
465-
[field R] [add_comm_group M] [module R M] :=
465+
[division_ring R] [add_comm_group M] [module R M] :=
466466
submodule R M

‎src/analysis/inner_product_space/two_dim.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -350,7 +350,7 @@ linear_isometry_equiv.ext $ o.linear_isometry_equiv_comp_right_angle_rotation φ
350350
/-- For a nonzero vector `x` in an oriented two-dimensional real inner product space `E`,
351351
`![x, J x]` forms an (orthogonal) basis for `E`. -/
352352
def basis_right_angle_rotation (x : E) (hx : x ≠ 0) : basis (fin 2) ℝ E :=
353-
@basis_of_linear_independent_of_card_eq_finrank _ _ _ _ _ _ _ _ ![x, J x]
353+
@basis_of_linear_independent_of_card_eq_finrank ℝ _ _ _ _ _ _ _ ![x, J x]
354354
(linear_independent_of_ne_zero_of_inner_eq_zero (λ i, by { fin_cases i; simp [hx] })
355355
begin
356356
intros i j hij,

‎src/field_theory/intermediate_field.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -485,7 +485,7 @@ by { rw [set_like.ext_iff, set_like.ext'_iff, set.ext_iff], refl }
485485

486486
lemma eq_of_le_of_finrank_le [finite_dimensional K L] (h_le : F ≤ E)
487487
(h_finrank : finrank K E ≤ finrank K F) : F = E :=
488-
to_subalgebra_injective $ subalgebra.to_submodule_injective $ eq_of_le_of_finrank_le h_le h_finrank
488+
to_subalgebra_injective $ subalgebra.to_submodule.injective $ eq_of_le_of_finrank_le h_le h_finrank
489489

490490
lemma eq_of_le_of_finrank_eq [finite_dimensional K L] (h_le : F ≤ E)
491491
(h_finrank : finrank K F = finrank K E) : F = E :=

‎src/field_theory/normal.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -68,7 +68,7 @@ begin
6868
let s := basis.of_vector_space F K,
6969
refine ⟨∏ x, minpoly F (s x),
7070
splits_prod _ $ λ x hx, h.splits (s x),
71-
subalgebra.to_submodule_injective _⟩,
71+
subalgebra.to_submodule.injective _⟩,
7272
rw [algebra.top_to_submodule, eq_top_iff, ← s.span_eq, submodule.span_le, set.range_subset_iff],
7373
refine λ x, algebra.subset_adjoin (multiset.mem_to_finset.mpr $
7474
(mem_roots $ mt (polynomial.map_eq_zero $ algebra_map F K).1 $

‎src/field_theory/tower.lean‎

Lines changed: 16 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Kenny Lau
55
-/
66

7+
import data.nat.prime
78
import ring_theory.algebra_tower
89
import linear_algebra.matrix.finite_dimensional
910
import linear_algebra.matrix.to_lin
@@ -38,7 +39,7 @@ section field
3839
open cardinal
3940

4041
variables (F : Type u) (K : Type v) (A : Type w)
41-
variables [field F] [field K] [add_comm_group A]
42+
variables [field F] [division_ring K] [add_comm_group A]
4243
variables [algebra F K] [module K A] [module F A] [is_scalar_tower F K A]
4344

4445
/-- Tower law: if `A` is a `K`-vector space and `K` is a field extension of `F` then
@@ -73,7 +74,7 @@ of_fintype_basis $ b.smul c
7374
7475
Note this cannot be an instance as Lean cannot infer `L`.
7576
-/
76-
theorem left (L : Type*) [ring L] [nontrivial L]
77+
theorem left (K L : Type*) [field K] [algebra F K] [ring L] [nontrivial L]
7778
[algebra F L] [algebra K L] [is_scalar_tower F K L]
7879
[finite_dimensional F L] : finite_dimensional F K :=
7980
finite_dimensional.of_injective
@@ -100,6 +101,19 @@ begin
100101
exact mt (@right F K A _ _ _ _ _ _ _) hA }
101102
end
102103

104+
theorem subalgebra.is_simple_order_of_finrank_prime (A) [ring A] [is_domain A] [algebra F A]
105+
(hp : (finrank F A).prime) : is_simple_order (subalgebra F A) :=
106+
{ to_nontrivial :=
107+
⟨⟨⊥, ⊤, λ he, nat.not_prime_one ((subalgebra.bot_eq_top_iff_finrank_eq_one.1 he).subst hp)⟩⟩,
108+
eq_bot_or_eq_top := λ K, begin
109+
haveI := finite_dimensional_of_finrank hp.pos,
110+
letI := division_ring_of_finite_dimensional F K,
111+
refine (hp.eq_one_or_self_of_dvd _ ⟨_, (finrank_mul_finrank F K A).symm⟩).imp _ (λ h, _),
112+
{ exact subalgebra.eq_bot_of_finrank_one },
113+
{ exact algebra.to_submodule_eq_top.1 (eq_top_of_finrank_eq $ K.finrank_to_submodule.trans h) },
114+
end }
115+
/- TODO: `intermediate_field` version -/
116+
103117
instance linear_map (F : Type u) (V : Type v) (W : Type w)
104118
[field F] [add_comm_group V] [module F V] [add_comm_group W] [module F W]
105119
[finite_dimensional F V] [finite_dimensional F W] :

‎src/linear_algebra/affine_space/finite_dimensional.lean‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -565,14 +565,14 @@ by rw [coplanar, coplanar, vector_span_insert_eq_vector_span h]
565565

566566
end affine_space'
567567

568-
section field
568+
section division_ring
569569

570570
variables {k : Type*} {V : Type*} {P : Type*}
571571
include V
572572

573573
open affine_subspace finite_dimensional module
574574

575-
variables [field k] [add_comm_group V] [module k V] [affine_space V P]
575+
variables [division_ring k] [add_comm_group V] [module k V] [affine_space V P]
576576

577577
/-- Adding a point to a finite-dimensional subspace increases the dimension by at most one. -/
578578
lemma finrank_vector_span_insert_le (s : affine_subspace k P) (p : P) :
@@ -649,4 +649,4 @@ variables (k)
649649
lemma coplanar_triple (p₁ p₂ p₃ : P) : coplanar k ({p₁, p₂, p₃} : set P) :=
650650
(collinear_pair k p₂ p₃).coplanar_insert p₁
651651

652-
end field
652+
end division_ring

‎src/linear_algebra/basis.lean‎

Lines changed: 4 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1320,12 +1320,7 @@ instance : is_atomistic (submodule K V) :=
13201320

13211321
end atoms_of_submodule_lattice
13221322

1323-
end division_ring
1324-
1325-
section field
1326-
1327-
variables [field K] [add_comm_group V] [add_comm_group V'] [module K V] [module K V']
1328-
variables {v : ι → V} {s t : set V} {x y z : V}
1323+
variables {K V}
13291324

13301325
lemma linear_map.exists_left_inverse_of_injective (f : V →ₗ[K] V')
13311326
(hf_inj : f.ker = ⊥) : ∃g:V' →ₗ[K] V, g.comp f = linear_map.id :=
@@ -1342,7 +1337,7 @@ begin
13421337
have BC := this.subset_extend (subset_univ _),
13431338
let hC := basis.extend this,
13441339
haveI : inhabited V := ⟨0⟩,
1345-
refine ⟨hC.constr K (C.restrict (inv_fun f)), hB.ext (λ b, _)⟩,
1340+
refine ⟨hC.constr ℕ (C.restrict (inv_fun f)), hB.ext (λ b, _)⟩,
13461341
rw image_subset_iff at BC,
13471342
have fb_eq : f b = hC ⟨f b, BC b.2⟩,
13481343
{ change f b = basis.extend this _,
@@ -1365,7 +1360,7 @@ begin
13651360
let C := basis.of_vector_space_index K V',
13661361
let hC := basis.of_vector_space K V',
13671362
haveI : inhabited V := ⟨0⟩,
1368-
use hC.constr K (C.restrict (inv_fun f)),
1363+
use hC.constr ℕ (C.restrict (inv_fun f)),
13691364
refine hC.ext (λ c, _),
13701365
rw [linear_map.comp_apply, hC.constr_basis],
13711366
simp [right_inverse_inv_fun (linear_map.range_eq_top.1 hf_surj) c]
@@ -1402,4 +1397,4 @@ let ⟨q, hq⟩ := p.exists_is_compl in nonempty.intro $
14021397
((quotient_equiv_of_is_compl p q hq).prod (linear_equiv.refl _ _)).trans
14031398
(prod_equiv_of_is_compl q p hq.symm)
14041399

1405-
end field
1400+
end division_ring

‎src/linear_algebra/dimension.lean‎

Lines changed: 6 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -1020,12 +1020,6 @@ by simp [dim_fun']
10201020

10211021
end fintype
10221022

1023-
end division_ring
1024-
1025-
section field
1026-
variables [field K] [add_comm_group V] [module K V] [add_comm_group V₁] [module K V₁]
1027-
variables [add_comm_group V'] [module K V']
1028-
10291023
theorem dim_quotient_add_dim (p : submodule K V) :
10301024
module.rank K (V ⧸ p) + module.rank K p = module.rank K V :=
10311025
by classical; exact let ⟨f⟩ := quotient_prod_linear_equiv p in dim_prod.symm.trans f.dim_eq
@@ -1108,7 +1102,7 @@ lemma exists_mem_ne_zero_of_dim_pos {s : submodule K V} (h : 0 < module.rank K s
11081102
∃ b : V, b ∈ s ∧ b ≠ 0 :=
11091103
exists_mem_ne_zero_of_ne_bot $ assume eq, by rw [eq, dim_bot] at h; exact lt_irrefl _ h
11101104

1111-
end field
1105+
end division_ring
11121106

11131107
section rank
11141108

@@ -1141,8 +1135,10 @@ by rw [rank, rank, linear_map.range_comp]; exact dim_map_le _ _
11411135

11421136
end
11431137

1144-
section field
1145-
variables [field K] [add_comm_group V] [module K V] [add_comm_group V₁] [module K V₁]
1138+
end rank
1139+
1140+
section division_ring
1141+
variables [division_ring K] [add_comm_group V] [module K V] [add_comm_group V₁] [module K V₁]
11461142
variables [add_comm_group V'] [module K V']
11471143

11481144
lemma rank_le_domain (f : V →ₗ[K] V₁) : rank f ≤ module.rank K V :=
@@ -1163,13 +1159,6 @@ lemma rank_finset_sum_le {η} (s : finset η) (f : η → V →ₗ[K] V') :
11631159
@finset.sum_hom_rel _ _ _ _ _ (λa b, rank a ≤ b) f (λ d, rank (f d)) s (le_of_eq rank_zero)
11641160
(λ i g c h, le_trans (rank_add_le _ _) (add_le_add_left h _))
11651161

1166-
end field
1167-
1168-
end rank
1169-
1170-
section division_ring
1171-
variables [division_ring K] [add_comm_group V] [module K V] [add_comm_group V'] [module K V']
1172-
11731162
/-- The `ι` indexed basis on `V`, where `ι` is an empty type and `V` is zero-dimensional.
11741163
11751164
See also `finite_dimensional.fin_basis`.
@@ -1301,11 +1290,6 @@ lemma module.rank_le_one_iff_top_is_principal :
13011290
module.rank K V ≤ 1 ↔ (⊤ : submodule K V).is_principal :=
13021291
by rw [← submodule.rank_le_one_iff_is_principal, dim_top]
13031292

1304-
end division_ring
1305-
1306-
section field
1307-
variables [field K] [add_comm_group V] [module K V] [add_comm_group V'] [module K V']
1308-
13091293
lemma le_rank_iff_exists_linear_independent {c : cardinal} {f : V →ₗ[K] V'} :
13101294
c ≤ rank f ↔
13111295
∃ s : set V, cardinal.lift.{v'} (#s) = cardinal.lift.{v} c ∧
@@ -1340,6 +1324,6 @@ begin
13401324
exact ⟨s, ⟨s, rfl, rfl⟩, si⟩ }
13411325
end
13421326

1343-
end field
1327+
end division_ring
13441328

13451329
end module

0 commit comments

Comments
 (0)