diff --git a/Mathlib.lean b/Mathlib.lean index 4dab0c5f04762..e4b9325d5fce1 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2577,6 +2577,7 @@ import Mathlib.LinearAlgebra.Dimension.Finrank import Mathlib.LinearAlgebra.Dimension.Free import Mathlib.LinearAlgebra.Dimension.LinearMap import Mathlib.LinearAlgebra.Dimension.Localization +import Mathlib.LinearAlgebra.Dimension.RankNullity import Mathlib.LinearAlgebra.Dimension.StrongRankCondition import Mathlib.LinearAlgebra.DirectSum.Finsupp import Mathlib.LinearAlgebra.DirectSum.TensorProduct diff --git a/Mathlib/LinearAlgebra/Dimension/Constructions.lean b/Mathlib/LinearAlgebra/Dimension/Constructions.lean index ac53365d04fe7..e452a4b15e79a 100644 --- a/Mathlib/LinearAlgebra/Dimension/Constructions.lean +++ b/Mathlib/LinearAlgebra/Dimension/Constructions.lean @@ -44,25 +44,35 @@ variable [Module R M] [Module R M'] [Module R M₁] section Quotient +theorem LinearIndependent.sum_elim_of_quotient + {M' : Submodule R M} {ι₁ ι₂} {f : ι₁ → M'} (hf : LinearIndependent R f) (g : ι₂ → M) + (hg : LinearIndependent R (Submodule.Quotient.mk (p := M') ∘ g)) : + LinearIndependent R (Sum.elim (f · : ι₁ → M) g) := by + refine .sum_type (hf.map' M'.subtype M'.ker_subtype) (.of_comp M'.mkQ hg) ?_ + refine disjoint_def.mpr fun x h₁ h₂ ↦ ?_ + have : x ∈ M' := span_le.mpr (Set.range_subset_iff.mpr fun i ↦ (f i).prop) h₁ + obtain ⟨c, rfl⟩ := Finsupp.mem_span_range_iff_exists_finsupp.mp h₂ + simp_rw [← Quotient.mk_eq_zero, ← mkQ_apply, map_finsupp_sum, map_smul, mkQ_apply] at this + rw [linearIndependent_iff.mp hg _ this, Finsupp.sum_zero_index] + +theorem LinearIndependent.union_of_quotient + {M' : Submodule R M} {s : Set M} (hs : s ⊆ M') (hs' : LinearIndependent (ι := s) R Subtype.val) + {t : Set M} (ht : LinearIndependent (ι := t) R (Submodule.Quotient.mk (p := M') ∘ Subtype.val)) : + LinearIndependent (ι := (s ∪ t : _)) R Subtype.val := by + refine (LinearIndependent.sum_elim_of_quotient (f := Set.embeddingOfSubset s M' hs) + (of_comp M'.subtype (by simpa using hs')) Subtype.val ht).to_subtype_range' ?_ + simp only [embeddingOfSubset_apply_coe, Sum.elim_range, Subtype.range_val] + theorem rank_quotient_add_rank_le [Nontrivial R] (M' : Submodule R M) : Module.rank R (M ⧸ M') + Module.rank R M' ≤ Module.rank R M := by - simp_rw [Module.rank_def] + conv_lhs => simp only [Module.rank_def] have := nonempty_linearIndependent_set R (M ⧸ M') have := nonempty_linearIndependent_set R M' rw [Cardinal.ciSup_add_ciSup _ (bddAbove_range.{v, v} _) _ (bddAbove_range.{v, v} _)] refine ciSup_le fun ⟨s, hs⟩ ↦ ciSup_le fun ⟨t, ht⟩ ↦ ?_ choose f hf using Quotient.mk_surjective M' - let g : s ⊕ t → M := Sum.elim (f ·) (·) - suffices LinearIndependent R g by - refine le_trans ?_ (le_ciSup (bddAbove_range.{v, v} _) ⟨_, this.to_subtype_range⟩) - rw [mk_range_eq _ this.injective, mk_sum, lift_id, lift_id] - refine .sum_type (.of_comp M'.mkQ ?_) (ht.map' M'.subtype M'.ker_subtype) ?_ - · convert hs; ext x; exact hf x - refine disjoint_def.mpr fun x h₁ h₂ ↦ ?_ - have : x ∈ M' := span_le.mpr (Set.range_subset_iff.mpr fun i ↦ i.1.2) h₂ - obtain ⟨c, rfl⟩ := Finsupp.mem_span_range_iff_exists_finsupp.mp h₁ - simp_rw [← Quotient.mk_eq_zero, ← mkQ_apply, map_finsupp_sum, map_smul, mkQ_apply, hf] at this - rw [linearIndependent_iff.mp hs _ this, Finsupp.sum_zero_index] + simpa [add_comm] using (LinearIndependent.sum_elim_of_quotient ht (fun (i : s) ↦ f i) + (by simpa [Function.comp, hf] using hs)).cardinal_le_rank theorem rank_quotient_le (p : Submodule R M) : Module.rank R (M ⧸ p) ≤ Module.rank R M := (mkQ p).rank_le_of_surjective (surjective_quot_mk _) diff --git a/Mathlib/LinearAlgebra/Dimension/DivisionRing.lean b/Mathlib/LinearAlgebra/Dimension/DivisionRing.lean index be5df0cf1c17f..f69dcf6bb85d2 100644 --- a/Mathlib/LinearAlgebra/Dimension/DivisionRing.lean +++ b/Mathlib/LinearAlgebra/Dimension/DivisionRing.lean @@ -7,7 +7,7 @@ Scott Morrison, Chris Hughes, Anne Baanen, Junyan Xu import Mathlib.LinearAlgebra.Basis.VectorSpace import Mathlib.LinearAlgebra.Dimension.Finite import Mathlib.SetTheory.Cardinal.Subfield -import Mathlib.LinearAlgebra.Dimension.Constructions +import Mathlib.LinearAlgebra.Dimension.RankNullity #align_import linear_algebra.dimension from "leanprover-community/mathlib"@"47a5f8186becdbc826190ced4312f8199f9db6a5" @@ -21,7 +21,7 @@ over division rings. For vector spaces (i.e. modules over a field), we have -* `rank_quotient_add_rank`: if `V₁` is a submodule of `V`, then +* `rank_quotient_add_rank_of_divisionRing`: if `V₁` is a submodule of `V`, then `Module.rank (V/V₁) + Module.rank V₁ = Module.rank V`. * `rank_range_add_rank_ker`: the rank-nullity theorem. * `rank_dual_eq_card_dual_of_aleph0_le_rank`: The **Erdős-Kaplansky Theorem** which says that @@ -33,7 +33,7 @@ For vector spaces (i.e. modules over a field), we have noncomputable section -universe u v v' v'' u₁' w w' +universe u₀ u v v' v'' u₁' w w' variable {K R : Type u} {V V₁ V₂ V₃ : Type v} {V' V'₁ : Type v'} {V'' : Type v''} variable {ι : Type w} {ι' : Type w'} {η : Type u₁'} {φ : η → Type*} @@ -55,60 +55,20 @@ theorem Basis.finite_ofVectorSpaceIndex_of_rank_lt_aleph0 (h : Module.rank K V < finite_def.2 <| (Basis.ofVectorSpace K V).nonempty_fintype_index_of_rank_lt_aleph0 h #align basis.finite_of_vector_space_index_of_rank_lt_aleph_0 Basis.finite_ofVectorSpaceIndex_of_rank_lt_aleph0 -theorem rank_quotient_add_rank (p : Submodule K V) : +/-- Also see `rank_quotient_add_rank`. -/ +theorem rank_quotient_add_rank_of_divisionRing (p : Submodule K V) : Module.rank K (V ⧸ p) + Module.rank K p = Module.rank K V := by classical let ⟨f⟩ := quotient_prod_linearEquiv p exact rank_prod'.symm.trans f.rank_eq -#align rank_quotient_add_rank rank_quotient_add_rank - -/-- The **rank-nullity theorem** -/ -theorem rank_range_add_rank_ker (f : V →ₗ[K] V₁) : - Module.rank K (LinearMap.range f) + Module.rank K (LinearMap.ker f) = Module.rank K V := by - haveI := fun p : Submodule K V => Classical.decEq (V ⧸ p) - rw [← f.quotKerEquivRange.rank_eq, rank_quotient_add_rank] -#align rank_range_add_rank_ker rank_range_add_rank_ker - -theorem rank_eq_of_surjective (f : V →ₗ[K] V₁) (h : Surjective f) : - Module.rank K V = Module.rank K V₁ + Module.rank K (LinearMap.ker f) := by - rw [← rank_range_add_rank_ker f, ← rank_range_of_surjective f h] -#align rank_eq_of_surjective rank_eq_of_surjective - -/-- Given a family of `n` linearly independent vectors in a space of dimension `> n`, one may extend -the family by another vector while retaining linear independence. -/ -theorem exists_linearIndependent_cons_of_lt_rank {n : ℕ} {v : Fin n → V} - (hv : LinearIndependent K v) (h : n < Module.rank K V) : - ∃ (x : V), LinearIndependent K (Fin.cons x v) := by - have A : Submodule.span K (range v) ≠ ⊤ := by - intro H - rw [← rank_top, ← H] at h - have : Module.rank K (Submodule.span K (range v)) ≤ n := by - have := Cardinal.mk_range_le_lift (f := v) - simp only [Cardinal.lift_id'] at this - exact (rank_span_le _).trans (this.trans (by simp)) - exact lt_irrefl _ (h.trans_le this) - obtain ⟨x, hx⟩ : ∃ x, x ∉ Submodule.span K (range v) := by - contrapose! A - exact Iff.mpr Submodule.eq_top_iff' A - exact ⟨x, linearIndependent_fin_cons.2 ⟨hv, hx⟩⟩ - -/-- Given a family of `n` linearly independent vectors in a space of dimension `> n`, one may extend -the family by another vector while retaining linear independence. -/ -theorem exists_linearIndependent_snoc_of_lt_rank {n : ℕ} {v : Fin n → V} - (hv : LinearIndependent K v) (h : n < Module.rank K V) : - ∃ (x : V), LinearIndependent K (Fin.snoc v x) := by - simpa [linearIndependent_fin_cons, ← linearIndependent_fin_snoc] - using exists_linearIndependent_cons_of_lt_rank hv h - -/-- Given a nonzero vector in a space of dimension `> 1`, one may find another vector linearly -independent of the first one. -/ -theorem exists_linearIndependent_pair_of_one_lt_rank - (h : 1 < Module.rank K V) {x : V} (hx : x ≠ 0) : - ∃ y, LinearIndependent K ![x, y] := by - obtain ⟨y, hy⟩ := exists_linearIndependent_snoc_of_lt_rank (linearIndependent_unique ![x] hx) h - have : Fin.snoc ![x] y = ![x, y] := Iff.mp List.ofFn_inj rfl - rw [this] at hy - exact ⟨y, hy⟩ + +instance DivisionRing.hasRankNullity : HasRankNullity.{u₀} K where + rank_quotient_add_rank := rank_quotient_add_rank_of_divisionRing + exists_set_linearIndependent V _ _ := by + let b := Module.Free.chooseBasis K V + refine ⟨range b, ?_, b.linearIndependent.to_subtype_range⟩ + rw [← lift_injective.eq_iff, mk_range_eq_of_injective b.injective, + Module.Free.rank_eq_card_chooseBasisIndex] section @@ -125,7 +85,7 @@ theorem rank_add_rank_split (db : V₂ →ₗ[K] V) (eb : V₃ →ₗ[K] V) (cd have hf : Surjective (coprod db eb) := by rwa [← range_eq_top, range_coprod, eq_top_iff] conv => rhs - rw [← rank_prod', rank_eq_of_surjective _ hf] + rw [← rank_prod', rank_eq_of_surjective hf] congr 1 apply LinearEquiv.rank_eq let L : V₁ →ₗ[K] ker (coprod db eb) := by -- Porting note: this is needed to avoid a timeout @@ -148,29 +108,6 @@ theorem rank_add_rank_split (db : V₂ →ₗ[K] V) (eb : V₃ →ₗ[K] V) (cd rw [h₂, _root_.neg_neg] #align rank_add_rank_split rank_add_rank_split -theorem Submodule.rank_sup_add_rank_inf_eq (s t : Submodule K V) : - Module.rank K (s ⊔ t : Submodule K V) + Module.rank K (s ⊓ t : Submodule K V) = - Module.rank K s + Module.rank K t := - rank_add_rank_split - (inclusion le_sup_left) (inclusion le_sup_right) - (inclusion inf_le_left) (inclusion inf_le_right) - (by - rw [← map_le_map_iff' (ker_subtype <| s ⊔ t), Submodule.map_sup, Submodule.map_top, ← - LinearMap.range_comp, ← LinearMap.range_comp, subtype_comp_inclusion, - subtype_comp_inclusion, range_subtype, range_subtype, range_subtype]) - (ker_inclusion _ _ _) (by ext ⟨x, hx⟩; rfl) - (by - rintro ⟨b₁, hb₁⟩ ⟨b₂, hb₂⟩ eq - obtain rfl : b₁ = b₂ := congr_arg Subtype.val eq - exact ⟨⟨b₁, hb₁, hb₂⟩, rfl, rfl⟩) -#align submodule.rank_sup_add_rank_inf_eq Submodule.rank_sup_add_rank_inf_eq - -theorem Submodule.rank_add_le_rank_add_rank (s t : Submodule K V) : - Module.rank K (s ⊔ t : Submodule K V) ≤ Module.rank K s + Module.rank K t := by - rw [← Submodule.rank_sup_add_rank_inf_eq] - exact self_le_add_right _ _ -#align submodule.rank_add_le_rank_add_rank Submodule.rank_add_le_rank_add_rank - end end DivisionRing @@ -307,35 +244,6 @@ theorem Module.rank_le_one_iff_top_isPrincipal : end Module -section Span - -open Submodule FiniteDimensional - -variable [DivisionRing K] [AddCommGroup V] [Module K V] - -/-- Given a family of `n` linearly independent vectors in a finite-dimensional space of -dimension `> n`, one may extend the family by another vector while retaining linear independence. -/ -theorem exists_linearIndependent_snoc_of_lt_finrank {n : ℕ} {v : Fin n → V} - (hv : LinearIndependent K v) (h : n < finrank K V) : - ∃ (x : V), LinearIndependent K (Fin.snoc v x) := - exists_linearIndependent_snoc_of_lt_rank hv (lt_rank_of_lt_finrank h) - -/-- Given a family of `n` linearly independent vectors in a finite-dimensional space of -dimension `> n`, one may extend the family by another vector while retaining linear independence. -/ -theorem exists_linearIndependent_cons_of_lt_finrank {n : ℕ} {v : Fin n → V} - (hv : LinearIndependent K v) (h : n < finrank K V) : - ∃ (x : V), LinearIndependent K (Fin.cons x v) := - exists_linearIndependent_cons_of_lt_rank hv (lt_rank_of_lt_finrank h) - -/-- Given a nonzero vector in a finite-dimensional space of dimension `> 1`, one may find another -vector linearly independent of the first one. -/ -theorem exists_linearIndependent_pair_of_one_lt_finrank - (h : 1 < finrank K V) {x : V} (hx : x ≠ 0) : - ∃ y, LinearIndependent K ![x, y] := - exists_linearIndependent_pair_of_one_lt_rank (one_lt_rank_of_one_lt_finrank h) hx - -end Span - section Basis open FiniteDimensional diff --git a/Mathlib/LinearAlgebra/Dimension/Finite.lean b/Mathlib/LinearAlgebra/Dimension/Finite.lean index 4c701e5c4cd05..a949fa9de34f5 100644 --- a/Mathlib/LinearAlgebra/Dimension/Finite.lean +++ b/Mathlib/LinearAlgebra/Dimension/Finite.lean @@ -211,6 +211,54 @@ alias finset_card_le_finrank_of_linearIndependent := LinearIndependent.finset_ca @[deprecated] alias Module.Finite.lt_aleph0_of_linearIndependent := LinearIndependent.lt_aleph0_of_finite +lemma exists_set_linearIndependent_of_lt_rank {n : Cardinal} (hn : n < Module.rank R M) : + ∃ s : Set M, #s = n ∧ LinearIndependent R ((↑) : s → M) := by + obtain ⟨⟨s, hs⟩, hs'⟩ := exists_lt_of_lt_ciSup' (hn.trans_eq (Module.rank_def R M)) + obtain ⟨t, ht, ht'⟩ := le_mk_iff_exists_subset.mp hs'.le + exact ⟨t, ht', .mono ht hs⟩ + +lemma exists_finset_linearIndependent_of_le_rank {n : ℕ} (hn : n ≤ Module.rank R M) : + ∃ s : Finset M, s.card = n ∧ LinearIndependent R ((↑) : s → M) := by + have := nonempty_linearIndependent_set + cases' hn.eq_or_lt with h h + · obtain ⟨⟨s, hs⟩, hs'⟩ := Cardinal.exists_eq_natCast_of_iSup_eq _ + (Cardinal.bddAbove_range.{v, v} _) _ (h.trans (Module.rank_def R M)).symm + have : Finite s := lt_aleph0_iff_finite.mp (hs' ▸ nat_lt_aleph0 n) + cases nonempty_fintype s + exact ⟨s.toFinset, by simpa using hs', by convert hs <;> exact Set.mem_toFinset⟩ + · obtain ⟨s, hs, hs'⟩ := exists_set_linearIndependent_of_lt_rank h + have : Finite s := lt_aleph0_iff_finite.mp (hs ▸ nat_lt_aleph0 n) + cases nonempty_fintype s + exact ⟨s.toFinset, by simpa using hs, by convert hs' <;> exact Set.mem_toFinset⟩ + +lemma exists_linearIndependent_of_le_rank {n : ℕ} (hn : n ≤ Module.rank R M) : + ∃ f : Fin n → M, LinearIndependent R f := + have ⟨_, hs, hs'⟩ := exists_finset_linearIndependent_of_le_rank hn + ⟨_, (linearIndependent_equiv (Finset.equivFinOfCardEq hs).symm).mpr hs'⟩ + +lemma natCast_le_rank_iff {n : ℕ} : + n ≤ Module.rank R M ↔ ∃ f : Fin n → M, LinearIndependent R f := + ⟨exists_linearIndependent_of_le_rank, + fun H ↦ by simpa using H.choose_spec.cardinal_lift_le_rank⟩ + +lemma natCast_le_rank_iff_finset {n : ℕ} : + n ≤ Module.rank R M ↔ ∃ s : Finset M, s.card = n ∧ LinearIndependent R ((↑) : s → M) := + ⟨exists_finset_linearIndependent_of_le_rank, + fun ⟨s, h₁, h₂⟩ ↦ by simpa [h₁] using h₂.cardinal_le_rank⟩ + +lemma exists_finset_linearIndependent_of_le_finrank {n : ℕ} (hn : n ≤ finrank R M) : + ∃ s : Finset M, s.card = n ∧ LinearIndependent R ((↑) : s → M) := by + by_cases h : finrank R M = 0 + · rw [le_zero_iff.mp (hn.trans_eq h)] + exact ⟨∅, rfl, by convert linearIndependent_empty R M using 2 <;> aesop⟩ + exact exists_finset_linearIndependent_of_le_rank + ((natCast_le.mpr hn).trans_eq (cast_toNat_of_lt_aleph0 (toNat_ne_zero.mp h).2)) + +lemma exists_linearIndependent_of_le_finrank {n : ℕ} (hn : n ≤ finrank R M) : + ∃ f : Fin n → M, LinearIndependent R f := + have ⟨_, hs, hs'⟩ := exists_finset_linearIndependent_of_le_finrank hn + ⟨_, (linearIndependent_equiv (Finset.equivFinOfCardEq hs).symm).mpr hs'⟩ + variable [Module.Finite R M] theorem Module.Finite.not_linearIndependent_of_infinite {ι : Type*} [Infinite ι] diff --git a/Mathlib/LinearAlgebra/Dimension/Localization.lean b/Mathlib/LinearAlgebra/Dimension/Localization.lean index 4485bc7cda3de..b03b91b17ef8e 100644 --- a/Mathlib/LinearAlgebra/Dimension/Localization.lean +++ b/Mathlib/LinearAlgebra/Dimension/Localization.lean @@ -6,6 +6,7 @@ Authors: Andrew Yang import Mathlib.Algebra.Module.Submodule.Localization import Mathlib.LinearAlgebra.Dimension.DivisionRing import Mathlib.RingTheory.Localization.FractionRing +import Mathlib.RingTheory.OreLocalization.OreSet /-! # Rank of localization @@ -28,6 +29,20 @@ variable [Module R M] [Module R N] [Algebra R S] [Module S N] [IsScalarTower R S variable (p : Submonoid R) [IsLocalization p S] (f : M →ₗ[R] N) [IsLocalizedModule p f] variable (hp : p ≤ R⁰) +variable {S} in +lemma IsLocalizedModule.linearIndependent_lift {ι} {v : ι → N} (hf : LinearIndependent S v) : + ∃ w : ι → M, LinearIndependent R w := by + choose sec hsec using IsLocalizedModule.surj p f + use fun i ↦ (sec (v i)).1 + rw [linearIndependent_iff'] at hf ⊢ + intro t g hg i hit + apply hp (sec (v i)).2.prop + apply IsLocalization.injective S hp + rw [map_zero] + refine hf t (fun i ↦ algebraMap R S (g i * (sec (v i)).2)) ?_ _ hit + simp only [map_mul, mul_smul, algebraMap_smul, ← Submonoid.smul_def, + hsec, ← map_smul, ← map_sum, hg, map_zero] + lemma IsLocalizedModule.lift_rank_eq : Cardinal.lift.{v} (Module.rank S N) = Cardinal.lift.{v'} (Module.rank R M) := by cases' subsingleton_or_nontrivial R @@ -37,16 +52,7 @@ lemma IsLocalizedModule.lift_rank_eq : · rw [Module.rank_def, lift_iSup (bddAbove_range.{v', v'} _)] apply ciSup_le' intro ⟨s, hs⟩ - choose sec hsec using IsLocalizedModule.surj p f - refine LinearIndependent.cardinal_lift_le_rank (ι := s) (v := fun i ↦ (sec i).1) ?_ - rw [linearIndependent_iff'] at hs ⊢ - intro t g hg i hit - apply hp (sec i).2.prop - apply IsLocalization.injective S hp - rw [map_zero] - refine hs t (fun i ↦ algebraMap R S (g i * (sec i).2)) ?_ _ hit - simp only [map_mul, mul_smul, algebraMap_smul, ← Submonoid.smul_def, - hsec, ← map_smul, ← map_sum, hg, map_zero] + exact (IsLocalizedModule.linearIndependent_lift p f hp hs).choose_spec.cardinal_lift_le_rank · rw [Module.rank_def, lift_iSup (bddAbove_range.{v, v} _)] apply ciSup_le' intro ⟨s, hs⟩ @@ -75,13 +81,75 @@ lemma IsLocalizedModule.rank_eq {N : Type v} [AddCommGroup N] [Module R N] [Module S N] [IsScalarTower R S N] (f : M →ₗ[R] N) [IsLocalizedModule p f] : Module.rank S N = Module.rank R M := by simpa using IsLocalizedModule.lift_rank_eq S p f hp -/-- The **rank-nullity theorem** for commutative domains. -/ +variable (R M) in +theorem exists_set_linearIndependent_of_isDomain [IsDomain R] : + ∃ s : Set M, #s = Module.rank R M ∧ LinearIndependent (ι := s) R Subtype.val := by + obtain ⟨w, hw⟩ := + IsLocalizedModule.linearIndependent_lift R⁰ (LocalizedModule.mkLinearMap R⁰ M) le_rfl + (Module.Free.chooseBasis (FractionRing R) (LocalizedModule R⁰ M)).linearIndependent + refine ⟨Set.range w, ?_, (linearIndependent_subtype_range hw.injective).mpr hw⟩ + apply Cardinal.lift_injective.{max u v} + rw [Cardinal.mk_range_eq_of_injective hw.injective, ← Module.Free.rank_eq_card_chooseBasisIndex, + IsLocalizedModule.lift_rank_eq (FractionRing R) R⁰ (LocalizedModule.mkLinearMap R⁰ M) le_rfl] + +/-- The **rank-nullity theorem** for commutative domains. Also see `rank_quotient_add_rank`. -/ theorem rank_quotient_add_rank_of_isDomain [IsDomain R] (M' : Submodule R M) : Module.rank R (M ⧸ M') + Module.rank R M' = Module.rank R M := by apply lift_injective.{max u v} rw [lift_add, ← IsLocalizedModule.lift_rank_eq (FractionRing R) R⁰ (M'.toLocalized R⁰) le_rfl, ← IsLocalizedModule.lift_rank_eq (FractionRing R) R⁰ (LocalizedModule.mkLinearMap R⁰ M) le_rfl, ← IsLocalizedModule.lift_rank_eq (FractionRing R) R⁰ (M'.toLocalizedQuotient R⁰) le_rfl, - ← lift_add, rank_quotient_add_rank] + ← lift_add, rank_quotient_add_rank_of_divisionRing] + +universe w in +instance IsDomain.hasRankNullity [IsDomain R] : HasRankNullity.{w} R where + rank_quotient_add_rank := rank_quotient_add_rank_of_isDomain + exists_set_linearIndependent M := exists_set_linearIndependent_of_isDomain R M end CommRing + +section Ring + +variable {R} [Ring R] [IsDomain R] (S : Submonoid R) + +open BigOperators in +/-- A domain that is not (right) Ore is of infinite (right) rank. +See [cohn_1995] Proposition 1.3.6 -/ +lemma aleph0_le_rank_of_isEmpty_oreSet (hS : IsEmpty (OreLocalization.OreSet R⁰)) : + ℵ₀ ≤ Module.rank Rᵐᵒᵖ R := by + classical + rw [← not_nonempty_iff, OreLocalization.nonempty_oreSet_iff_of_noZeroDivisors] at hS + push_neg at hS + obtain ⟨r, s, h⟩ := hS + refine Cardinal.aleph0_le.mpr fun n ↦ ?_ + suffices LinearIndependent Rᵐᵒᵖ (fun (i : Fin n) ↦ s ^ (i : ℕ) * r) by + simpa using this.cardinal_lift_le_rank + suffices ∀ (g : ℕ → Rᵐᵒᵖ) (x), (∑ i in Finset.range n, g i • (s ^ (i + x) * r)) = 0 → + ∀ i < n, g i = 0 by + refine Fintype.linearIndependent_iff.mpr fun g hg i ↦ ?_ + simpa only [dif_pos i.prop] using this (fun i ↦ if h : i < n then g ⟨i, h⟩ else 0) 0 + (by simp [← Fin.sum_univ_eq_sum_range, ← hg]) i i.prop + intro g x hg i hin + induction' n with n IH generalizing g x i + · exact (hin.not_le (zero_le i)).elim + · rw [Finset.sum_range_succ'] at hg + by_cases hg0 : g 0 = 0 + · simp only [hg0, zero_smul, add_zero, add_assoc] at hg + cases i; exacts [hg0, IH _ _ hg _ (Nat.succ_lt_succ_iff.mp hin)] + simp only [MulOpposite.smul_eq_mul_unop, zero_add, ← add_comm x, pow_add _ x, + mul_assoc, pow_succ', ← Finset.mul_sum, pow_zero, one_mul] at hg + rw [← neg_eq_iff_add_eq_zero, ← neg_mul, neg_mul_comm, ← neg_mul, neg_mul_comm] at hg + have := mul_left_cancel₀ (mem_nonZeroDivisors_iff_ne_zero.mp (s ^ x).prop) hg + exact (h _ ⟨(g 0).unop, mem_nonZeroDivisors_iff_ne_zero.mpr (by simpa)⟩ this.symm).elim + +-- TODO: Upgrade this to an iff. See [lam_1999] Exercise 10.21 +lemma nonempty_oreSet_of_strongRankCondition [StrongRankCondition R] : + Nonempty (OreLocalization.OreSet Rᵐᵒᵖ⁰) := by + by_contra h + have H : Module.rank R R = Module.rank Rᵐᵒᵖᵐᵒᵖ Rᵐᵒᵖ := rank_eq_of_equiv_equiv (RingEquiv.opOp R) + MulOpposite.opAddEquiv (RingEquiv.opOp R).bijective (by simp) + have := aleph0_le_rank_of_isEmpty_oreSet (not_nonempty_iff.mp h) + rw [← H, rank_self] at this + exact this.not_lt one_lt_aleph0 + +end Ring diff --git a/Mathlib/LinearAlgebra/Dimension/RankNullity.lean b/Mathlib/LinearAlgebra/Dimension/RankNullity.lean new file mode 100644 index 0000000000000..e43de4cca94c0 --- /dev/null +++ b/Mathlib/LinearAlgebra/Dimension/RankNullity.lean @@ -0,0 +1,202 @@ +/- +Copyright (c) 2024 Andrew Yang. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Andrew Yang +-/ +import Mathlib.LinearAlgebra.Dimension.Constructions +import Mathlib.LinearAlgebra.Dimension.Finite + +/-! + +# The rank nullity theorem + +In this file we provide the rank nullity theorem as a typeclass, and prove various corollaries +of the theorem. The main definition is `HasRankNullity.{u} R`, which states that +1. Every `R`-module `M : Type u` has a linear independent subset of cardinality `Module.rank R M`. +2. `rank (M ⧸ N) + rank N = rank M` for every `R`-module `M : Type u` and every `N : Submodule R M`. + +The following instances are provided in mathlib: +1. `DivisionRing.hasRankNullity` for division rings in `LinearAlgebra/Dimension/DivisionRing.lean`. +2. `IsDomain.hasRankNullity` for commutative domains in `LinearAlgebra/Dimension/Localization.lean`. + +TODO: prove the rank-nullity theorem for `[Ring R] [IsDomain R] [StrongRankCondition R]`. +See `nonempty_oreSet_of_strongRankCondition` for a start. +-/ +universe u v + +open Function Set Cardinal + +variable {R} {M M₁ M₂ M₃ : Type u} {M' : Type v} [Ring R] +variable [AddCommGroup M] [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup M₃] [AddCommGroup M'] +variable [Module R M] [Module R M₁] [Module R M₂] [Module R M₃] [Module R M'] + +/-- +`HasRankNullity.{u}` is a class of rings satisfying +1. Every `R`-module `M : Type u` has a linear independent subset of cardinality `Module.rank R M`. +2. `rank (M ⧸ N) + rank N = rank M` for every `R`-module `M : Type u` and every `N : Submodule R M`. + +Usually such a ring satisfies `HasRankNullity.{w}` for all universes `w`, and the universe +argument is there because of technical limitations to universe polymorphism. + +See `DivisionRing.hasRankNullity` and `IsDomain.hasRankNullity`. +-/ +@[pp_with_univ] +class HasRankNullity (R : Type v) [inst : Ring R] : Prop where + exists_set_linearIndependent : ∀ (M : Type u) [AddCommGroup M] [Module R M], + ∃ s : Set M, #s = Module.rank R M ∧ LinearIndependent (ι := s) R Subtype.val + rank_quotient_add_rank : ∀ {M : Type u} [AddCommGroup M] [Module R M] (N : Submodule R M), + Module.rank R (M ⧸ N) + Module.rank R N = Module.rank R M + +variable [HasRankNullity.{u} R] + +lemma rank_quotient_add_rank (N : Submodule R M) : + Module.rank R (M ⧸ N) + Module.rank R N = Module.rank R M := + HasRankNullity.rank_quotient_add_rank N +#align rank_quotient_add_rank rank_quotient_add_rank + +variable (R M) in +lemma exists_set_linearIndependent : + ∃ s : Set M, #s = Module.rank R M ∧ LinearIndependent (ι := s) R Subtype.val := + HasRankNullity.exists_set_linearIndependent M + +variable (R) in +instance (priority := 100) : Nontrivial R := by + refine (subsingleton_or_nontrivial R).resolve_left fun H ↦ ?_ + have := rank_quotient_add_rank (R := R) (M := PUnit) ⊥ + simp [one_add_one_eq_two] at this + +theorem lift_rank_range_add_rank_ker (f : M →ₗ[R] M') : + lift.{u} (Module.rank R (LinearMap.range f)) + lift.{v} (Module.rank R (LinearMap.ker f)) = + lift.{v} (Module.rank R M) := by + haveI := fun p : Submodule R M => Classical.decEq (M ⧸ p) + rw [← f.quotKerEquivRange.lift_rank_eq, ← lift_add, rank_quotient_add_rank] + +/-- The **rank-nullity theorem** -/ +theorem rank_range_add_rank_ker (f : M →ₗ[R] M₁) : + Module.rank R (LinearMap.range f) + Module.rank R (LinearMap.ker f) = Module.rank R M := by + haveI := fun p : Submodule R M => Classical.decEq (M ⧸ p) + rw [← f.quotKerEquivRange.rank_eq, rank_quotient_add_rank] +#align rank_range_add_rank_ker rank_range_add_rank_ker + +theorem lift_rank_eq_of_surjective {f : M →ₗ[R] M'} (h : Surjective f) : + lift.{v} (Module.rank R M) = + lift.{u} (Module.rank R M') + lift.{v} (Module.rank R (LinearMap.ker f)) := by + rw [← lift_rank_range_add_rank_ker f, ← rank_range_of_surjective f h] + +theorem rank_eq_of_surjective {f : M →ₗ[R] M₁} (h : Surjective f) : + Module.rank R M = Module.rank R M₁ + Module.rank R (LinearMap.ker f) := by + rw [← rank_range_add_rank_ker f, ← rank_range_of_surjective f h] +#align rank_eq_of_surjective rank_eq_of_surjective + +theorem exists_linearIndependent_of_lt_rank [StrongRankCondition R] + {s : Set M} (hs : LinearIndependent (ι := s) R Subtype.val) : + ∃ t, s ⊆ t ∧ #t = Module.rank R M ∧ LinearIndependent (ι := t) R Subtype.val := by + obtain ⟨t, ht, ht'⟩ := exists_set_linearIndependent R (M ⧸ Submodule.span R s) + choose sec hsec using Submodule.Quotient.mk_surjective (Submodule.span R s) + have hsec' : Submodule.Quotient.mk ∘ sec = id := funext hsec + have hst : Disjoint s (sec '' t) := by + rw [Set.disjoint_iff] + rintro _ ⟨hxs, ⟨x, hxt, rfl⟩⟩ + apply ht'.ne_zero ⟨x, hxt⟩ + rw [Subtype.coe_mk, ← hsec x, Submodule.Quotient.mk_eq_zero] + exact Submodule.subset_span hxs + refine ⟨s ∪ sec '' t, subset_union_left _ _, ?_, ?_⟩ + rw [Cardinal.mk_union_of_disjoint hst, Cardinal.mk_image_eq, ht, + ← rank_quotient_add_rank (Submodule.span R s), add_comm, rank_span_set hs] + · exact HasLeftInverse.injective ⟨Submodule.Quotient.mk, hsec⟩ + · apply LinearIndependent.union_of_quotient Submodule.subset_span hs + rwa [Function.comp, linearIndependent_image ((hsec'.symm ▸ injective_id).injOn t).image_of_comp, + ← image_comp, hsec', image_id] + +/-- Given a family of `n` linearly independent vectors in a space of dimension `> n`, one may extend +the family by another vector while retaining linear independence. -/ +theorem exists_linearIndependent_cons_of_lt_rank [StrongRankCondition R] {n : ℕ} {v : Fin n → M} + (hv : LinearIndependent R v) (h : n < Module.rank R M) : + ∃ (x : M), LinearIndependent R (Fin.cons x v) := by + obtain ⟨t, h₁, h₂, h₃⟩ := exists_linearIndependent_of_lt_rank hv.to_subtype_range + have : range v ≠ t := by + refine fun e ↦ h.ne ?_ + rw [← e, ← lift_injective.eq_iff, mk_range_eq_of_injective hv.injective] at h₂ + simpa only [mk_fintype, Fintype.card_fin, lift_natCast, lift_id'] using h₂ + obtain ⟨x, hx, hx'⟩ := nonempty_of_ssubset (h₁.ssubset_of_ne this) + exact ⟨x, (linearIndependent_subtype_range (Fin.cons_injective_iff.mpr ⟨hx', hv.injective⟩)).mp + (h₃.mono (Fin.range_cons x v ▸ insert_subset hx h₁))⟩ + +/-- Given a family of `n` linearly independent vectors in a space of dimension `> n`, one may extend +the family by another vector while retaining linear independence. -/ +theorem exists_linearIndependent_snoc_of_lt_rank [StrongRankCondition R] {n : ℕ} {v : Fin n → M} + (hv : LinearIndependent R v) (h : n < Module.rank R M) : + ∃ (x : M), LinearIndependent R (Fin.snoc v x) := by + simp only [Fin.snoc_eq_cons_rotate] + have ⟨x, hx⟩ := exists_linearIndependent_cons_of_lt_rank hv h + exact ⟨x, hx.comp _ (finRotate _).injective⟩ + +/-- Given a nonzero vector in a space of dimension `> 1`, one may find another vector linearly +independent of the first one. -/ +theorem exists_linearIndependent_pair_of_one_lt_rank [StrongRankCondition R] + [NoZeroSMulDivisors R M] (h : 1 < Module.rank R M) {x : M} (hx : x ≠ 0) : + ∃ y, LinearIndependent R ![x, y] := by + obtain ⟨y, hy⟩ := exists_linearIndependent_snoc_of_lt_rank (linearIndependent_unique ![x] hx) h + have : Fin.snoc ![x] y = ![x, y] := Iff.mp List.ofFn_inj rfl + rw [this] at hy + exact ⟨y, hy⟩ + +theorem exists_smul_not_mem_of_rank_lt {N : Submodule R M} (h : Module.rank R N < Module.rank R M) : + ∃ m : M, ∀ r : R, r ≠ 0 → r • m ∉ N := by + have : Module.rank R (M ⧸ N) ≠ 0 := by + intro e + rw [← rank_quotient_add_rank N, e, zero_add] at h + exact h.ne rfl + rw [ne_eq, rank_eq_zero_iff, (Submodule.Quotient.mk_surjective N).forall] at this + push_neg at this + simp_rw [← N.mkQ_apply, ← map_smul, N.mkQ_apply, ne_eq, Submodule.Quotient.mk_eq_zero] at this + exact this + +open BigOperators Cardinal Basis Submodule Function Set LinearMap + +theorem Submodule.rank_sup_add_rank_inf_eq (s t : Submodule R M) : + Module.rank R (s ⊔ t : Submodule R M) + Module.rank R (s ⊓ t : Submodule R M) = + Module.rank R s + Module.rank R t := by + conv_rhs => enter [2]; rw [show t = (s ⊔ t) ⊓ t by simp] + rw [← rank_quotient_add_rank ((s ⊓ t).comap s.subtype), + ← rank_quotient_add_rank (t.comap (s ⊔ t).subtype), + (quotientInfEquivSupQuotient s t).rank_eq, + (equivSubtypeMap s (comap _ (s ⊓ t))).rank_eq, Submodule.map_comap_subtype, + (equivSubtypeMap (s ⊔ t) (comap _ t)).rank_eq, Submodule.map_comap_subtype, + ← inf_assoc, inf_idem, add_right_comm] +#align submodule.rank_sup_add_rank_inf_eq Submodule.rank_sup_add_rank_inf_eq + +theorem Submodule.rank_add_le_rank_add_rank (s t : Submodule R M) : + Module.rank R (s ⊔ t : Submodule R M) ≤ Module.rank R s + Module.rank R t := by + rw [← Submodule.rank_sup_add_rank_inf_eq] + exact self_le_add_right _ _ +#align submodule.rank_add_le_rank_add_rank Submodule.rank_add_le_rank_add_rank + +section Finrank + +open Submodule FiniteDimensional + +variable [StrongRankCondition R] + +/-- Given a family of `n` linearly independent vectors in a finite-dimensional space of +dimension `> n`, one may extend the family by another vector while retaining linear independence. -/ +theorem exists_linearIndependent_snoc_of_lt_finrank {n : ℕ} {v : Fin n → M} + (hv : LinearIndependent R v) (h : n < finrank R M) : + ∃ (x : M), LinearIndependent R (Fin.snoc v x) := + exists_linearIndependent_snoc_of_lt_rank hv (lt_rank_of_lt_finrank h) + +/-- Given a family of `n` linearly independent vectors in a finite-dimensional space of +dimension `> n`, one may extend the family by another vector while retaining linear independence. -/ +theorem exists_linearIndependent_cons_of_lt_finrank {n : ℕ} {v : Fin n → M} + (hv : LinearIndependent R v) (h : n < finrank R M) : + ∃ (x : M), LinearIndependent R (Fin.cons x v) := + exists_linearIndependent_cons_of_lt_rank hv (lt_rank_of_lt_finrank h) + +/-- Given a nonzero vector in a finite-dimensional space of dimension `> 1`, one may find another +vector linearly independent of the first one. -/ +theorem exists_linearIndependent_pair_of_one_lt_finrank [NoZeroSMulDivisors R M] + (h : 1 < finrank R M) {x : M} (hx : x ≠ 0) : + ∃ y, LinearIndependent R ![x, y] := + exists_linearIndependent_pair_of_one_lt_rank (one_lt_rank_of_one_lt_finrank h) hx + +end Finrank diff --git a/Mathlib/Logic/Embedding/Set.lean b/Mathlib/Logic/Embedding/Set.lean index 86499d0996406..ff790121e3533 100644 --- a/Mathlib/Logic/Embedding/Set.lean +++ b/Mathlib/Logic/Embedding/Set.lean @@ -85,13 +85,13 @@ end Function namespace Set /-- The injection map is an embedding between subsets. -/ -@[simps apply] +@[simps apply_coe] def embeddingOfSubset {α} (s t : Set α) (h : s ⊆ t) : s ↪ t := ⟨fun x ↦ ⟨x.1, h x.2⟩, fun ⟨x, hx⟩ ⟨y, hy⟩ h ↦ by congr injection h⟩ #align set.embedding_of_subset Set.embeddingOfSubset -#align set.embedding_of_subset_apply Set.embeddingOfSubset_apply +#align set.embedding_of_subset_apply Set.embeddingOfSubset_apply_coeₓ end Set diff --git a/Mathlib/NumberTheory/Modular.lean b/Mathlib/NumberTheory/Modular.lean index b1af21757ad59..3e4b17aebb11e 100644 --- a/Mathlib/NumberTheory/Modular.lean +++ b/Mathlib/NumberTheory/Modular.lean @@ -191,6 +191,9 @@ def lcRow0Extend {cd : Fin 2 → ℤ} (hcd : IsCoprime (cd 0) (cd 1)) : exact hcd.sq_add_sq_ne_zero, LinearEquiv.refl ℝ (Fin 2 → ℝ)] #align modular_group.lc_row0_extend ModularGroup.lcRow0Extend +-- `simpNF` times out, but only in CI where all of `Mathlib` is imported +attribute [nolint simpNF] lcRow0Extend_apply lcRow0Extend_symm_apply + /-- The map `lcRow0` is proper, that is, preimages of cocompact sets are finite in `[[* , *], [c, d]]`. -/ theorem tendsto_lcRow0 {cd : Fin 2 → ℤ} (hcd : IsCoprime (cd 0) (cd 1)) : diff --git a/Mathlib/RingTheory/OreLocalization/OreSet.lean b/Mathlib/RingTheory/OreLocalization/OreSet.lean index 64853a88b774a..99b01c4f960a2 100644 --- a/Mathlib/RingTheory/OreLocalization/OreSet.lean +++ b/Mathlib/RingTheory/OreLocalization/OreSet.lean @@ -120,4 +120,22 @@ def oreSetOfNoZeroDivisors {R : Type*} [Ring R] [NoZeroDivisors R] {S : Submonoi oreSetOfCancelMonoidWithZero oreNum oreDenom ore_eq #align ore_localization.ore_set_of_no_zero_divisors OreLocalization.oreSetOfNoZeroDivisors +lemma nonempty_oreSet_iff {R : Type*} [Ring R] {S : Submonoid R} : + Nonempty (OreSet S) ↔ (∀ (r₁ r₂ : R) (s : S), ↑s * r₁ = s * r₂ → ∃ s' : S, r₁ * s' = r₂ * s') ∧ + (∀ (r : R) (s : S), ∃ (r' : R) (s' : S), r * s' = s * r') := by + constructor + · exact fun ⟨_⟩ ↦ ⟨ore_left_cancel, fun r s ↦ ⟨oreNum r s, oreDenom r s, ore_eq r s⟩⟩ + · intro ⟨H, H'⟩ + choose r' s' h using H' + exact ⟨H, r', s', h⟩ + +lemma nonempty_oreSet_iff_of_noZeroDivisors {R : Type*} [Ring R] [NoZeroDivisors R] + {S : Submonoid R} : + Nonempty (OreSet S) ↔ ∀ (r : R) (s : S), ∃ (r' : R) (s' : S), r * s' = s * r' := by + constructor + · exact fun ⟨_⟩ ↦ fun r s ↦ ⟨oreNum r s, oreDenom r s, ore_eq r s⟩ + · intro H + choose r' s' h using H + exact ⟨oreSetOfNoZeroDivisors r' s' h⟩ + end OreLocalization diff --git a/docs/references.bib b/docs/references.bib index f0040b7a4a741..93613fb63e63a 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -788,6 +788,17 @@ @Article{ cohen2012 bibsource = {dblp computer science bibliography, https://dblp.org} } +@Book{ cohn_1995, + place = {Cambridge}, + series = {Encyclopedia of Mathematics and its Applications}, + title = {Skew Fields: Theory of General Division Rings}, + doi = {10.1017/CBO9781139087193}, + publisher = {Cambridge University Press}, + author = {Cohn, P. M.}, + year = {1995}, + collection = {Encyclopedia of Mathematics and its Applications} +} + @Book{ conrad2000, author = {Conrad, Brian}, title = {Grothendieck duality and base change}, @@ -2000,6 +2011,15 @@ @Article{ kozen1994 over Kleene algebras.} } +@Book{ lam_1999, + series = {Graduate Texts in Mathematics}, + title = {Lectures on Modules and Rings}, + doi = {10.1007/978-1-4612-0525-8}, + publisher = {Springer New York, NY}, + author = {T. Y. Lam}, + year = {1999} +} + @Article{ lazarus1973, author = {Michel Lazarus}, title = {Les familles libres maximales d'un module ont-elles le