From 9e4a4beff6f9d3ddf2c19c20948533afb4521927 Mon Sep 17 00:00:00 2001 From: Oliver Nash Date: Tue, 1 Oct 2024 22:14:14 +0000 Subject: [PATCH 1/3] feat: a family of compatible triangularisable endomorphisms are simultaneously triangularisable (#17194) Co-authored-by: Oliver Nash <7734364+ocfnash@users.noreply.github.com> --- Mathlib/Algebra/Lie/Weights/Basic.lean | 35 ++----------- Mathlib/Algebra/Module/Submodule/Lattice.lean | 4 ++ .../Algebra/Module/Submodule/LinearMap.lean | 7 +++ Mathlib/Algebra/Module/Submodule/Map.lean | 4 ++ Mathlib/LinearAlgebra/Eigenspace/Basic.lean | 45 +++++++++++++++++ .../Eigenspace/Triangularizable.lean | 49 +++++++++++++++++++ 6 files changed, 113 insertions(+), 31 deletions(-) diff --git a/Mathlib/Algebra/Lie/Weights/Basic.lean b/Mathlib/Algebra/Lie/Weights/Basic.lean index 310b0d062c7aa..810246b2c95a8 100644 --- a/Mathlib/Algebra/Lie/Weights/Basic.lean +++ b/Mathlib/Algebra/Lie/Weights/Basic.lean @@ -778,37 +778,10 @@ instance (N : LieSubmodule K L M) [IsTriangularizable K L M] : IsTriangularizabl See also `LieModule.iSup_genWeightSpace_eq_top'`. -/ lemma iSup_genWeightSpace_eq_top [IsTriangularizable K L M] : ⨆ χ : L → K, genWeightSpace M χ = ⊤ := by - generalize h_dim : finrank K M = n - induction n using Nat.strongRecOn generalizing M with | ind n ih => ?_ - obtain h' | ⟨y : L, hy : ¬ ∃ φ, genWeightSpaceOf M φ y = ⊤⟩ := - forall_or_exists_not (fun (x : L) ↦ ∃ (φ : K), genWeightSpaceOf M φ x = ⊤) - · choose χ hχ using h' - replace hχ : genWeightSpace M χ = ⊤ := by simpa only [genWeightSpace, hχ] using iInf_top - exact eq_top_iff.mpr <| hχ ▸ le_iSup (genWeightSpace M) χ - · replace hy : ∀ φ, finrank K (genWeightSpaceOf M φ y) < n := fun φ ↦ by - simp_rw [not_exists, ← lt_top_iff_ne_top] at hy; exact h_dim ▸ Submodule.finrank_lt (hy φ) - replace ih : ∀ φ, ⨆ χ : L → K, genWeightSpace (genWeightSpaceOf M φ y) χ = ⊤ := - fun φ ↦ ih _ (hy φ) (genWeightSpaceOf M φ y) rfl - replace ih : ∀ φ, ⨆ (χ : L → K) (_ : χ y = φ), - genWeightSpace (genWeightSpaceOf M φ y) χ = ⊤ := by - intro φ - suffices ∀ χ : L → K, χ y ≠ φ → genWeightSpace (genWeightSpaceOf M φ y) χ = ⊥ by - specialize ih φ; rw [iSup_split, biSup_congr this] at ih; simpa using ih - intro χ hχ - rw [eq_bot_iff, ← (genWeightSpaceOf M φ y).ker_incl, LieModuleHom.ker, - ← LieSubmodule.map_le_iff_le_comap, map_genWeightSpace_eq_of_injective - (genWeightSpaceOf M φ y).injective_incl, LieSubmodule.range_incl, ← disjoint_iff_inf_le] - exact (disjoint_genWeightSpaceOf K L M hχ).mono_left - (genWeightSpace_le_genWeightSpaceOf M y χ) - replace ih : ∀ φ, ⨆ (χ : L → K) (_ : χ y = φ), genWeightSpace M χ = genWeightSpaceOf M φ y := by - intro φ - have (χ : L → K) (hχ : χ y = φ) : genWeightSpace M χ = - (genWeightSpace (genWeightSpaceOf M φ y) χ).map (genWeightSpaceOf M φ y).incl := by - rw [← hχ, genWeightSpace_genWeightSpaceOf_map_incl] - simp_rw [biSup_congr this, ← LieSubmodule.map_iSup, ih, LieModuleHom.map_top, - LieSubmodule.range_incl] - simpa only [← ih, iSup_comm (ι := K), iSup_iSup_eq_right] using - iSup_genWeightSpaceOf_eq_top K L M y + simp only [← LieSubmodule.coe_toSubmodule_eq_iff, LieSubmodule.iSup_coe_toSubmodule, + LieSubmodule.iInf_coe_toSubmodule, LieSubmodule.top_coeSubmodule, genWeightSpace] + exact Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo (toEnd K L M) + (fun x y φ z ↦ (genWeightSpaceOf M φ y).lie_mem) (IsTriangularizable.iSup_eq_top) lemma iSup_genWeightSpace_eq_top' [IsTriangularizable K L M] : ⨆ χ : Weight K L M, genWeightSpace M χ = ⊤ := by diff --git a/Mathlib/Algebra/Module/Submodule/Lattice.lean b/Mathlib/Algebra/Module/Submodule/Lattice.lean index 1b9c97d71bbe6..ce617ef5b2a6b 100644 --- a/Mathlib/Algebra/Module/Submodule/Lattice.lean +++ b/Mathlib/Algebra/Module/Submodule/Lattice.lean @@ -241,6 +241,10 @@ theorem mem_finset_inf {ι} {s : Finset ι} {p : ι → Submodule R M} {x : M} : x ∈ s.inf p ↔ ∀ i ∈ s, x ∈ p i := by simp only [← SetLike.mem_coe, finset_inf_coe, Set.mem_iInter] +lemma inf_iInf {ι : Type*} [Nonempty ι] {p : ι → Submodule R M} (q : Submodule R M) : + q ⊓ ⨅ i, p i = ⨅ i, q ⊓ p i := + SetLike.coe_injective <| by simpa only [inf_coe, iInf_coe] using Set.inter_iInter _ _ + theorem mem_sup_left {S T : Submodule R M} : ∀ {x : M}, x ∈ S → x ∈ S ⊔ T := by have : S ≤ S ⊔ T := le_sup_left rw [LE.le] at this diff --git a/Mathlib/Algebra/Module/Submodule/LinearMap.lean b/Mathlib/Algebra/Module/Submodule/LinearMap.lean index 913de1199bb0c..36b04e8dc9c3d 100644 --- a/Mathlib/Algebra/Module/Submodule/LinearMap.lean +++ b/Mathlib/Algebra/Module/Submodule/LinearMap.lean @@ -183,6 +183,13 @@ lemma restrict_comp (g ∘ₗ f).restrict hfg = (g.restrict hg) ∘ₗ (f.restrict hf) := rfl +-- TODO Consider defining `Algebra R (p.compatibleMaps p)`, `AlgHom` version of `LinearMap.restrict` +lemma restrict_smul_one + {R M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} + (μ : R) (h : ∀ x ∈ p, (μ • (1 : Module.End R M)) x ∈ p := fun _ ↦ p.smul_mem μ) : + (μ • 1 : Module.End R M).restrict h = μ • (1 : Module.End R p) := + rfl + lemma restrict_commute {f g : M →ₗ[R] M} (h : Commute f g) {p : Submodule R M} (hf : MapsTo f p p) (hg : MapsTo g p p) : Commute (f.restrict hf) (g.restrict hg) := by diff --git a/Mathlib/Algebra/Module/Submodule/Map.lean b/Mathlib/Algebra/Module/Submodule/Map.lean index 6f6227fd83734..1d1245ea336c6 100644 --- a/Mathlib/Algebra/Module/Submodule/Map.lean +++ b/Mathlib/Algebra/Module/Submodule/Map.lean @@ -120,6 +120,10 @@ theorem map_inf (f : F) {p q : Submodule R M} (hf : Injective f) : (p ⊓ q).map f = p.map f ⊓ q.map f := SetLike.coe_injective <| Set.image_inter hf +lemma map_iInf {ι : Type*} [Nonempty ι] {p : ι → Submodule R M} (f : F) (hf : Injective f) : + (⨅ i, p i).map f = ⨅ i, (p i).map f := + SetLike.coe_injective <| by simpa only [map_coe, iInf_coe] using hf.injOn.image_iInter_eq + theorem range_map_nonempty (N : Submodule R M) : (Set.range (fun ϕ => Submodule.map ϕ N : (M →ₛₗ[σ₁₂] M₂) → Submodule R₂ M₂)).Nonempty := ⟨_, Set.mem_range.mpr ⟨0, rfl⟩⟩ diff --git a/Mathlib/LinearAlgebra/Eigenspace/Basic.lean b/Mathlib/LinearAlgebra/Eigenspace/Basic.lean index e5c7fcb4b592f..1495ca7c3ce48 100644 --- a/Mathlib/LinearAlgebra/Eigenspace/Basic.lean +++ b/Mathlib/LinearAlgebra/Eigenspace/Basic.lean @@ -449,6 +449,51 @@ lemma _root_.Submodule.inf_genEigenspace (f : End R M) (p : Submodule R M) {k : (genEigenspace (LinearMap.restrict f hfp) μ k).map p.subtype := by rw [f.genEigenspace_restrict _ _ _ hfp, Submodule.map_comap_eq, Submodule.range_subtype] +/-- Given a family of endomorphisms `i ↦ f i`, a family of candidate eigenvalues `i ↦ μ i`, and a +submodule `p` which is invariant wrt every `f i`, the intersection of `p` with the simultaneous +maximal generalised eigenspace (taken over all `i`), is the same as the simultaneous maximal +generalised eigenspace of the `f i` restricted to `p`. -/ +lemma _root_.Submodule.inf_iInf_maxGenEigenspace_of_forall_mapsTo {ι : Type*} {μ : ι → R} + (f : ι → End R M) (p : Submodule R M) (hfp : ∀ i, MapsTo (f i) p p) : + p ⊓ ⨅ i, (f i).maxGenEigenspace (μ i) = + (⨅ i, maxGenEigenspace ((f i).restrict (hfp i)) (μ i)).map p.subtype := by + cases isEmpty_or_nonempty ι + · simp [iInf_of_isEmpty] + · simp_rw [inf_iInf, maxGenEigenspace, ((f _).genEigenspace _).mono.directed_le.inf_iSup_eq, + p.inf_genEigenspace _ (hfp _), ← Submodule.map_iSup, Submodule.map_iInf _ p.injective_subtype] + +/-- Given a family of endomorphisms `i ↦ f i`, a family of candidate eigenvalues `i ↦ μ i`, and a +distinguished index `i` whose maximal generalised `μ i`-eigenspace is invariant wrt every `f j`, +taking simultaneous maximal generalised eigenspaces is unaffected by first restricting to the +distinguished generalised `μ i`-eigenspace. -/ +lemma iInf_maxGenEigenspace_restrict_map_subtype_eq + {ι : Type*} {μ : ι → R} (i : ι) (f : ι → End R M) + (h : ∀ j, MapsTo (f j) ((f i).maxGenEigenspace (μ i)) ((f i).maxGenEigenspace (μ i))) : + letI p := (f i).maxGenEigenspace (μ i) + letI q (j : ι) := maxGenEigenspace ((f j).restrict (h j)) (μ j) + (⨅ j, q j).map p.subtype = ⨅ j, (f j).maxGenEigenspace (μ j) := by + have : Nonempty ι := ⟨i⟩ + set p := (f i).maxGenEigenspace (μ i) + have : ⨅ j, (f j).maxGenEigenspace (μ j) = p ⊓ ⨅ j, (f j).maxGenEigenspace (μ j) := by + refine le_antisymm ?_ inf_le_right + simpa only [le_inf_iff, le_refl, and_true] using iInf_le _ _ + rw [Submodule.map_iInf _ p.injective_subtype, this, Submodule.inf_iInf] + simp_rw [maxGenEigenspace_def, Submodule.map_iSup, + ((f _).genEigenspace _).mono.directed_le.inf_iSup_eq, p.inf_genEigenspace (f _) (h _)] + rfl + +lemma mapsTo_restrict_maxGenEigenspace_restrict_of_mapsTo + {p : Submodule R M} (f g : End R M) (hf : MapsTo f p p) (hg : MapsTo g p p) {μ₁ μ₂ : R} + (h : MapsTo f (g.maxGenEigenspace μ₁) (g.maxGenEigenspace μ₂)) : + MapsTo (f.restrict hf) + (maxGenEigenspace (g.restrict hg) μ₁) + (maxGenEigenspace (g.restrict hg) μ₂) := by + intro x hx + simp_rw [SetLike.mem_coe, mem_maxGenEigenspace, ← LinearMap.restrict_smul_one _, + LinearMap.restrict_sub _, LinearMap.pow_restrict _, LinearMap.restrict_apply, + Submodule.mk_eq_zero, ← mem_maxGenEigenspace] at hx ⊢ + exact h hx + /-- If `p` is an invariant submodule of an endomorphism `f`, then the `μ`-eigenspace of the restriction of `f` to `p` is a submodule of the `μ`-eigenspace of `f`. -/ theorem eigenspace_restrict_le_eigenspace (f : End R M) {p : Submodule R M} (hfp : ∀ x ∈ p, f x ∈ p) diff --git a/Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean b/Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean index e2cd61a713f7f..a6fb4ee72e490 100644 --- a/Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean +++ b/Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean @@ -222,3 +222,52 @@ theorem Module.End.iSup_genEigenspace_restrict_eq_top simp_rw [Submodule.inf_genEigenspace f p h, Submodule.comap_subtype_self, ← Submodule.map_iSup, Submodule.comap_map_eq_of_injective h_inj] at this exact this.symm + +/-- Given a family of endomorphisms `i ↦ f i` which are compatible in the sense that every maximal +generalised eigenspace of `f i` is invariant wrt `f j`, if each `f i` is triangularizable, the +family is simultaneously triangularizable. -/ +lemma Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo + {ι : Type*} [FiniteDimensional K V] + (f : ι → End K V) + (h : ∀ i j φ, MapsTo (f i) ((f j).maxGenEigenspace φ) ((f j).maxGenEigenspace φ)) + (h' : ∀ i, ⨆ μ, (f i).maxGenEigenspace μ = ⊤) : + ⨆ χ : ι → K, ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤ := by + generalize h_dim : finrank K V = n + induction n using Nat.strongRecOn generalizing V with | ind n ih => ?_ + obtain this | ⟨i : ι, hy : ¬ ∃ φ, (f i).maxGenEigenspace φ = ⊤⟩ := + forall_or_exists_not (fun j : ι ↦ ∃ φ : K, (f j).maxGenEigenspace φ = ⊤) + · choose χ hχ using this + replace hχ : ⨅ i, (f i).maxGenEigenspace (χ i) = ⊤ := by simpa + simp_rw [eq_top_iff] at hχ ⊢ + exact le_trans hχ <| le_iSup (fun χ : ι → K ↦ ⨅ i, (f i).maxGenEigenspace (χ i)) χ + · replace hy : ∀ φ, finrank K ((f i).maxGenEigenspace φ) < n := fun φ ↦ by + simp_rw [not_exists, ← lt_top_iff_ne_top] at hy; exact h_dim ▸ Submodule.finrank_lt (hy φ) + have hi (j : ι) (φ : K) : + MapsTo (f j) ((f i).maxGenEigenspace φ) ((f i).maxGenEigenspace φ) := by + exact h j i φ + replace ih (φ : K) : + ⨆ χ : ι → K, ⨅ j, maxGenEigenspace ((f j).restrict (hi j φ)) (χ j) = ⊤ := by + apply ih _ (hy φ) + · intro j k μ + exact mapsTo_restrict_maxGenEigenspace_restrict_of_mapsTo (f j) (f k) _ _ (h j k μ) + · exact fun j ↦ Module.End.iSup_genEigenspace_restrict_eq_top _ (h' j) + · rfl + replace ih (φ : K) : + ⨆ (χ : ι → K) (_ : χ i = φ), ⨅ j, maxGenEigenspace ((f j).restrict (hi j φ)) (χ j) = ⊤ := by + suffices ∀ χ : ι → K, χ i ≠ φ → ⨅ j, maxGenEigenspace ((f j).restrict (hi j φ)) (χ j) = ⊥ by + specialize ih φ; rw [iSup_split, biSup_congr this] at ih; simpa using ih + intro χ hχ + rw [eq_bot_iff, ← ((f i).maxGenEigenspace φ).ker_subtype, LinearMap.ker, + ← Submodule.map_le_iff_le_comap, ← Submodule.inf_iInf_maxGenEigenspace_of_forall_mapsTo, + ← disjoint_iff_inf_le] + exact ((f i).disjoint_iSup_genEigenspace hχ.symm).mono_right (iInf_le _ i) + replace ih (φ : K) : + ⨆ (χ : ι → K) (_ : χ i = φ), ⨅ j, maxGenEigenspace (f j) (χ j) = + maxGenEigenspace (f i) φ := by + have (χ : ι → K) (hχ : χ i = φ) : ⨅ j, maxGenEigenspace (f j) (χ j) = + (⨅ j, maxGenEigenspace ((f j).restrict (hi j φ)) (χ j)).map + ((f i).maxGenEigenspace φ).subtype := by + rw [← hχ, iInf_maxGenEigenspace_restrict_map_subtype_eq] + simp_rw [biSup_congr this, ← Submodule.map_iSup, ih, Submodule.map_top, + Submodule.range_subtype] + simpa only [← ih, iSup_comm (ι := K), iSup_iSup_eq_right] using h' i From f7a8f884c8dab2fed9d8cc96fb2502dfc3da0665 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 2 Oct 2024 00:01:11 +0100 Subject: [PATCH 2/3] chore: add a focusing dot --- Mathlib/RingTheory/TwoSidedIdeal/Operations.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/TwoSidedIdeal/Operations.lean b/Mathlib/RingTheory/TwoSidedIdeal/Operations.lean index ea08a0c3e8866..455172552a77c 100644 --- a/Mathlib/RingTheory/TwoSidedIdeal/Operations.lean +++ b/Mathlib/RingTheory/TwoSidedIdeal/Operations.lean @@ -106,7 +106,8 @@ def ker : TwoSidedIdeal R := (by rintro _ _ (h : f _ = 0); simp [h]) lemma mem_ker {x : R} : x ∈ ker f ↔ f x = 0 := by - delta ker; rw [mem_mk']; rfl + delta ker; rw [mem_mk'] + · rfl · rintro _ _ (h1 : f _ = 0) (h2 : f _ = 0); simp [h1, h2] · rintro _ (h : f _ = 0); simp [h] · rintro _ _ (h : f _ = 0); simp [h] From 1f131791d022d7e2db03ee89c132488ec1602c68 Mon Sep 17 00:00:00 2001 From: adomani Date: Wed, 2 Oct 2024 00:28:15 +0100 Subject: [PATCH 3/3] Laurent --- Mathlib/RingTheory/LaurentSeries.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/LaurentSeries.lean b/Mathlib/RingTheory/LaurentSeries.lean index 669be5c1d5cd1..eea4d59465c7d 100644 --- a/Mathlib/RingTheory/LaurentSeries.lean +++ b/Mathlib/RingTheory/LaurentSeries.lean @@ -771,7 +771,7 @@ theorem Cauchy.eventually_mem_nhds {ℱ : Filter (LaurentSeries K)} (hℱ : Cauc rw [← WithZero.coe_unzero γ.ne_zero, WithZero.coe_lt_coe, hD₀, neg_neg, ofAdd_sub, ofAdd_toAdd, div_lt_comm, div_self', ← ofAdd_zero, Multiplicative.ofAdd_lt] exact zero_lt_one - apply coeff_eventually_equal hℱ |>.mono + apply coeff_eventually_equal (D := D) hℱ |>.mono intro _ hf apply lt_of_le_of_lt (valuation_le_iff_coeff_lt_eq_zero K |>.mpr _) hD intro n hn