diff --git a/Mathlib/Algebra/Lie/TraceForm.lean b/Mathlib/Algebra/Lie/TraceForm.lean index 62c493ca9f4c7..2d1253e2b18c9 100644 --- a/Mathlib/Algebra/Lie/TraceForm.lean +++ b/Mathlib/Algebra/Lie/TraceForm.lean @@ -277,7 +277,7 @@ lemma lowerCentralSeries_one_inf_center_le_ker_traceForm [Module.Free R M] [Modu intro y exact y.induction_on rfl (fun a u ↦ by simp [hzc u]) (fun u v hu hv ↦ by simp [hu, hv]) apply LinearMap.trace_comp_eq_zero_of_commute_of_trace_restrict_eq_zero - · simpa only [Module.End.maxGenEigenspace_def] using IsTriangularizable.iSup_eq_top (1 ⊗ₜ[R] x) + · exact IsTriangularizable.maxGenEigenspace_eq_top (1 ⊗ₜ[R] x) · exact fun μ ↦ trace_toEnd_eq_zero_of_mem_lcs A (A ⊗[R] L) (genWeightSpaceOf (A ⊗[R] M) μ ((1:A) ⊗ₜ[R] x)) (le_refl 1) hz · exact commute_toEnd_of_mem_center_right (A ⊗[R] M) hzc (1 ⊗ₜ x) diff --git a/Mathlib/Algebra/Lie/Weights/Basic.lean b/Mathlib/Algebra/Lie/Weights/Basic.lean index 1d5d4302ac426..a903c7e4c8c88 100644 --- a/Mathlib/Algebra/Lie/Weights/Basic.lean +++ b/Mathlib/Algebra/Lie/Weights/Basic.lean @@ -165,7 +165,7 @@ theorem mem_genWeightSpaceOf (χ : R) (x : L) (m : M) : theorem coe_genWeightSpaceOf_zero (x : L) : ↑(genWeightSpaceOf M (0 : R) x) = ⨆ k, LinearMap.ker (toEnd R L M x ^ k) := by - simp [genWeightSpaceOf, Module.End.maxGenEigenspace_def] + simp [genWeightSpaceOf, ← Module.End.iSup_genEigenspace_eq] /-- If `M` is a representation of a nilpotent Lie algebra `L` and `χ : L → R` is a family of scalars, @@ -267,7 +267,7 @@ lemma genWeightSpaceOf_ne_bot (χ : Weight R L M) (x : L) : lemma hasEigenvalueAt (χ : Weight R L M) (x : L) : (toEnd R L M x).HasEigenvalue (χ x) := by obtain ⟨k : ℕ, hk : (toEnd R L M x).genEigenspace (χ x) k ≠ ⊥⟩ := by - simpa [genWeightSpaceOf, Module.End.maxGenEigenspace_def] using χ.genWeightSpaceOf_ne_bot x + simpa [genWeightSpaceOf, ← Module.End.iSup_genEigenspace_eq] using χ.genWeightSpaceOf_ne_bot x exact Module.End.hasEigenvalue_of_hasGenEigenvalue hk lemma apply_eq_zero_of_isNilpotent [NoZeroSMulDivisors R M] [IsReduced R] @@ -631,8 +631,7 @@ lemma disjoint_genWeightSpaceOf [NoZeroSMulDivisors R M] {x : L} {φ₁ φ₂ : Disjoint (genWeightSpaceOf M φ₁ x) (genWeightSpaceOf M φ₂ x) := by rw [LieSubmodule.disjoint_iff_coe_toSubmodule] dsimp [genWeightSpaceOf] - simp_rw [Module.End.maxGenEigenspace_def] - exact Module.End.disjoint_iSup_genEigenspace _ h + exact Module.End.disjoint_unifEigenspace _ h _ _ lemma disjoint_genWeightSpace [NoZeroSMulDivisors R M] {χ₁ χ₂ : L → R} (h : χ₁ ≠ χ₂) : Disjoint (genWeightSpace M χ₁) (genWeightSpace M χ₂) := by @@ -665,8 +664,7 @@ lemma independent_genWeightSpaceOf [NoZeroSMulDivisors R M] (x : L) : CompleteLattice.Independent fun (χ : R) ↦ genWeightSpaceOf M χ x := by rw [LieSubmodule.independent_iff_coe_toSubmodule] dsimp [genWeightSpaceOf] - simp_rw [Module.End.maxGenEigenspace_def] - exact (toEnd R L M x).independent_genEigenspace + exact (toEnd R L M x).independent_unifEigenspace _ lemma finite_genWeightSpaceOf_ne_bot [NoZeroSMulDivisors R M] [IsNoetherian R M] (x : L) : {χ : R | genWeightSpaceOf M χ x ≠ ⊥}.Finite := @@ -688,16 +686,18 @@ noncomputable instance Weight.instFintype [NoZeroSMulDivisors R M] [IsNoetherian /-- A Lie module `M` of a Lie algebra `L` is triangularizable if the endomorhpism of `M` defined by any `x : L` is triangularizable. -/ class IsTriangularizable : Prop where - iSup_eq_top : ∀ x, ⨆ φ, ⨆ k, (toEnd R L M x).genEigenspace φ k = ⊤ + maxGenEigenspace_eq_top : ∀ x, ⨆ φ, (toEnd R L M x).maxGenEigenspace φ = ⊤ instance (L' : LieSubalgebra R L) [IsTriangularizable R L M] : IsTriangularizable R L' M where - iSup_eq_top x := IsTriangularizable.iSup_eq_top (x : L) + maxGenEigenspace_eq_top x := IsTriangularizable.maxGenEigenspace_eq_top (x : L) instance (I : LieIdeal R L) [IsTriangularizable R L M] : IsTriangularizable R I M where - iSup_eq_top x := IsTriangularizable.iSup_eq_top (x : L) + maxGenEigenspace_eq_top x := IsTriangularizable.maxGenEigenspace_eq_top (x : L) instance [IsTriangularizable R L M] : IsTriangularizable R (LieModule.toEnd R L M).range M where - iSup_eq_top := by rintro ⟨-, x, rfl⟩; exact IsTriangularizable.iSup_eq_top x + maxGenEigenspace_eq_top := by + rintro ⟨-, x, rfl⟩ + exact IsTriangularizable.maxGenEigenspace_eq_top x @[simp] lemma iSup_genWeightSpaceOf_eq_top [IsTriangularizable R L M] (x : L) : @@ -705,8 +705,7 @@ lemma iSup_genWeightSpaceOf_eq_top [IsTriangularizable R L M] (x : L) : rw [← LieSubmodule.coe_toSubmodule_eq_iff, LieSubmodule.iSup_coe_toSubmodule, LieSubmodule.top_coeSubmodule] dsimp [genWeightSpaceOf] - simp_rw [Module.End.maxGenEigenspace_def] - exact IsTriangularizable.iSup_eq_top x + exact IsTriangularizable.maxGenEigenspace_eq_top x open LinearMap Module in @[simp] @@ -729,12 +728,12 @@ variable [Field K] [LieAlgebra K L] [Module K M] [LieModule K L M] [LieAlgebra.I [FiniteDimensional K M] instance instIsTriangularizableOfIsAlgClosed [IsAlgClosed K] : IsTriangularizable K L M := - ⟨fun _ ↦ Module.End.iSup_genEigenspace_eq_top _⟩ + ⟨fun _ ↦ Module.End.iSup_maxGenEigenspace_eq_top _⟩ instance (N : LieSubmodule K L M) [IsTriangularizable K L M] : IsTriangularizable K L N := by refine ⟨fun y ↦ ?_⟩ rw [← N.toEnd_restrict_eq_toEnd y] - exact Module.End.iSup_genEigenspace_restrict_eq_top _ (IsTriangularizable.iSup_eq_top y) + exact Module.End.unifEigenspace_restrict_eq_top _ (IsTriangularizable.maxGenEigenspace_eq_top y) /-- For a triangularizable Lie module in finite dimensions, the weight spaces span the entire space. @@ -745,8 +744,7 @@ lemma iSup_genWeightSpace_eq_top [IsTriangularizable K L M] : LieSubmodule.iInf_coe_toSubmodule, LieSubmodule.top_coeSubmodule, genWeightSpace] refine Module.End.iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo (toEnd K L M) (fun x y φ z ↦ (genWeightSpaceOf M φ y).lie_mem) ?_ - simp_rw [Module.End.maxGenEigenspace_def] - apply IsTriangularizable.iSup_eq_top + apply IsTriangularizable.maxGenEigenspace_eq_top lemma iSup_genWeightSpace_eq_top' [IsTriangularizable K L M] : ⨆ χ : Weight K L M, genWeightSpace M χ = ⊤ := by diff --git a/Mathlib/Algebra/Lie/Weights/Linear.lean b/Mathlib/Algebra/Lie/Weights/Linear.lean index 741b68fdabb92..2898ac57b5d73 100644 --- a/Mathlib/Algebra/Lie/Weights/Linear.lean +++ b/Mathlib/Algebra/Lie/Weights/Linear.lean @@ -98,17 +98,15 @@ instance instLinearWeightsOfIsLieAbelian [IsLieAbelian L] [NoZeroSMulDivisors R rw [commute_iff_lie_eq, ← LieHom.map_lie, trivial_lie_zero, LieHom.map_zero] intro χ hχ x y simp_rw [Ne, ← LieSubmodule.coe_toSubmodule_eq_iff, genWeightSpace, genWeightSpaceOf, - LieSubmodule.iInf_coe_toSubmodule, LieSubmodule.bot_coeSubmodule, - Module.End.maxGenEigenspace_def] at hχ - exact Module.End.map_add_of_iInf_genEigenspace_ne_bot_of_commute - (toEnd R L M).toLinearMap χ hχ h x y + LieSubmodule.iInf_coe_toSubmodule, LieSubmodule.bot_coeSubmodule] at hχ + exact Module.End.map_add_of_iInf_unifEigenspace_ne_bot_of_commute + (toEnd R L M).toLinearMap χ _ hχ h x y { map_add := aux map_smul := fun χ hχ t x ↦ by simp_rw [Ne, ← LieSubmodule.coe_toSubmodule_eq_iff, genWeightSpace, genWeightSpaceOf, - LieSubmodule.iInf_coe_toSubmodule, LieSubmodule.bot_coeSubmodule, - Module.End.maxGenEigenspace_def] at hχ - exact Module.End.map_smul_of_iInf_genEigenspace_ne_bot - (toEnd R L M).toLinearMap χ hχ t x + LieSubmodule.iInf_coe_toSubmodule, LieSubmodule.bot_coeSubmodule] at hχ + exact Module.End.map_smul_of_iInf_unifEigenspace_ne_bot + (toEnd R L M).toLinearMap χ _ hχ t x map_lie := fun χ hχ t x ↦ by rw [trivial_lie_zero, ← add_left_inj (χ 0), ← aux χ hχ, zero_add, zero_add] } diff --git a/Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean b/Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean index 049ba1532a238..f10d670703e8a 100644 --- a/Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean +++ b/Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean @@ -72,7 +72,7 @@ theorem eigenspace_inf_eigenspace (hAB : A ∘ₗ B = B ∘ₗ A) (γ : 𝕜) : eigenspace A α ⊓ eigenspace B γ = map (Submodule.subtype (eigenspace A α)) (eigenspace (B.restrict (eigenspace_invariant_of_commute hAB α)) γ) := - (eigenspace A α).inf_genEigenspace _ _ (k := 1) + (eigenspace A α).inf_unifEigenspace _ _ (k := 1) variable [FiniteDimensional 𝕜 E] diff --git a/Mathlib/CategoryTheory/Functor/Const.lean b/Mathlib/CategoryTheory/Functor/Const.lean index 6d6844ebf3690..ba2d6a7b37e98 100644 --- a/Mathlib/CategoryTheory/Functor/Const.lean +++ b/Mathlib/CategoryTheory/Functor/Const.lean @@ -99,6 +99,13 @@ def compConstIso (F : C ⥤ D) : (fun X => NatIso.ofComponents (fun _ => Iso.refl _) (by aesop_cat)) (by aesop_cat) +/-- The canonical isomorphism +`const D ⋙ (whiskeringLeft J _ _).obj F ≅ const J`.-/ +@[simps!] +def constCompWhiskeringLeftIso (F : J ⥤ D) : + const D ⋙ (whiskeringLeft J D C).obj F ≅ const J := + NatIso.ofComponents fun X => NatIso.ofComponents fun Y => Iso.refl _ + end end CategoryTheory.Functor diff --git a/Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean b/Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean index 274273b8794c3..8998a80ca9e01 100644 --- a/Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean +++ b/Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean @@ -22,7 +22,7 @@ right Kan extension along `L`. namespace CategoryTheory -open Category +open Category Limits namespace Functor @@ -122,6 +122,20 @@ lemma isIso_lanAdjunction_counit_app_iff (G : D ⥤ H) : IsIso ((L.lanAdjunction H).counit.app G) ↔ G.IsLeftKanExtension (𝟙 (L ⋙ G)) := (isLeftKanExtension_iff_isIso _ (L.lanUnit.app (L ⋙ G)) _ (by simp)).symm +/-- Composing the left Kan extension of `L : C ⥤ D` with `colim` on shapes `D` is isomorphic +to `colim` on shapes `C`. -/ +@[simps!] +noncomputable def lanCompColimIso (L : C ⥤ D) [∀ (G : C ⥤ H), L.HasLeftKanExtension G] + [HasColimitsOfShape C H] [HasColimitsOfShape D H] : L.lan ⋙ colim ≅ colim (C := H) := + Iso.symm <| NatIso.ofComponents + (fun G ↦ (colimitIsoOfIsLeftKanExtension _ (L.lanUnit.app G)).symm) + (fun f ↦ colimit.hom_ext (fun i ↦ by + dsimp + rw [ι_colimMap_assoc, ι_colimitIsoOfIsLeftKanExtension_inv, + ι_colimitIsoOfIsLeftKanExtension_inv_assoc, ι_colimMap, ← assoc, ← assoc] + congr 1 + exact congr_app (L.lanUnit.naturality f) i)) + end section @@ -251,6 +265,20 @@ lemma isIso_ranAdjunction_unit_app_iff (G : D ⥤ H) : IsIso ((L.ranAdjunction H).unit.app G) ↔ G.IsRightKanExtension (𝟙 (L ⋙ G)) := (isRightKanExtension_iff_isIso _ (L.ranCounit.app (L ⋙ G)) _ (by simp)).symm +/-- Composing the right Kan extension of `L : C ⥤ D` with `lim` on shapes `D` is isomorphic +to `lim` on shapes `C`. -/ +@[simps!] +noncomputable def ranCompLimIso (L : C ⥤ D) [∀ (G : C ⥤ H), L.HasRightKanExtension G] + [HasLimitsOfShape C H] [HasLimitsOfShape D H] : L.ran ⋙ lim ≅ lim (C := H) := + NatIso.ofComponents + (fun G ↦ limitIsoOfIsRightKanExtension _ (L.ranCounit.app G)) + (fun f ↦ limit.hom_ext (fun i ↦ by + dsimp + rw [assoc, assoc, limMap_π, limitIsoOfIsRightKanExtension_hom_π_assoc, + limitIsoOfIsRightKanExtension_hom_π, limMap_π_assoc] + congr 1 + exact congr_app (L.ranCounit.naturality f) i)) + end section diff --git a/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean b/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean index 7c08315b07111..4ea68229bb26b 100644 --- a/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean +++ b/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean @@ -544,6 +544,106 @@ lemma isRightKanExtension_iff_of_iso₂ {F₁' F₂' : D ⥤ H} (α₁ : L ⋙ F end +section Colimit + +variable (F' : D ⥤ H) {L : C ⥤ D} {F : C ⥤ H} (α : F ⟶ L ⋙ F') [F'.IsLeftKanExtension α] + +/-- Construct a cocone for a left Kan extension `F' : D ⥤ H` of `F : C ⥤ H` along a functor +`L : C ⥤ D` given a cocone for `F`. -/ +@[simps] +noncomputable def coconeOfIsLeftKanExtension (c : Cocone F) : Cocone F' where + pt := c.pt + ι := F'.descOfIsLeftKanExtension α _ c.ι + +/-- If `c` is a colimit cocone for a functor `F : C ⥤ H` and `α : F ⟶ L ⋙ F'` is the unit of any +left Kan extension `F' : D ⥤ H` of `F` along `L : C ⥤ D`, then `coconeOfIsLeftKanExtension α c` is +a colimit cocone, too. -/ +@[simps] +def isColimitCoconeOfIsLeftKanExtension {c : Cocone F} (hc : IsColimit c) : + IsColimit (F'.coconeOfIsLeftKanExtension α c) where + desc s := hc.desc (Cocone.mk _ (α ≫ whiskerLeft L s.ι)) + fac s := by + have : F'.descOfIsLeftKanExtension α ((const D).obj c.pt) c.ι ≫ + (Functor.const _).map (hc.desc (Cocone.mk _ (α ≫ whiskerLeft L s.ι))) = s.ι := + F'.hom_ext_of_isLeftKanExtension α _ _ (by aesop_cat) + exact congr_app this + uniq s m hm := hc.hom_ext (fun j ↦ by + have := hm (L.obj j) + nth_rw 1 [← F'.descOfIsLeftKanExtension_fac_app α ((const D).obj c.pt)] + dsimp at this ⊢ + rw [assoc, this, IsColimit.fac, NatTrans.comp_app, whiskerLeft_app]) + +variable [HasColimit F] [HasColimit F'] + +/-- If `F' : D ⥤ H` is a left Kan extension of `F : C ⥤ H` along `L : C ⥤ D`, the colimit over `F'` +is isomorphic to the colimit over `F`. -/ +noncomputable def colimitIsoOfIsLeftKanExtension : colimit F' ≅ colimit F := + IsColimit.coconePointUniqueUpToIso (colimit.isColimit F') + (F'.isColimitCoconeOfIsLeftKanExtension α (colimit.isColimit F)) + +@[reassoc (attr := simp)] +lemma ι_colimitIsoOfIsLeftKanExtension_hom (i : C) : + α.app i ≫ colimit.ι F' (L.obj i) ≫ (F'.colimitIsoOfIsLeftKanExtension α).hom = + colimit.ι F i := by + simp [colimitIsoOfIsLeftKanExtension] + +@[reassoc (attr := simp)] +lemma ι_colimitIsoOfIsLeftKanExtension_inv (i : C) : + colimit.ι F i ≫ (F'.colimitIsoOfIsLeftKanExtension α).inv = + α.app i ≫ colimit.ι F' (L.obj i) := by + rw [Iso.comp_inv_eq, assoc, ι_colimitIsoOfIsLeftKanExtension_hom] + +end Colimit + +section Limit + +variable (F' : D ⥤ H) {L : C ⥤ D} {F : C ⥤ H} (α : L ⋙ F' ⟶ F) [F'.IsRightKanExtension α] + +/-- Construct a cone for a right Kan extension `F' : D ⥤ H` of `F : C ⥤ H` along a functor +`L : C ⥤ D` given a cone for `F`. -/ +@[simps] +noncomputable def coneOfIsRightKanExtension (c : Cone F) : Cone F' where + pt := c.pt + π := F'.liftOfIsRightKanExtension α _ c.π + +/-- If `c` is a limit cone for a functor `F : C ⥤ H` and `α : L ⋙ F' ⟶ F` is the counit of any +right Kan extension `F' : D ⥤ H` of `F` along `L : C ⥤ D`, then `coneOfIsRightKanExtension α c` is +a limit cone, too. -/ +@[simps] +def isLimitConeOfIsRightKanExtension {c : Cone F} (hc : IsLimit c) : + IsLimit (F'.coneOfIsRightKanExtension α c) where + lift s := hc.lift (Cone.mk _ (whiskerLeft L s.π ≫ α)) + fac s := by + have : (Functor.const _).map (hc.lift (Cone.mk _ (whiskerLeft L s.π ≫ α))) ≫ + F'.liftOfIsRightKanExtension α ((const D).obj c.pt) c.π = s.π := + F'.hom_ext_of_isRightKanExtension α _ _ (by aesop_cat) + exact congr_app this + uniq s m hm := hc.hom_ext (fun j ↦ by + have := hm (L.obj j) + nth_rw 1 [← F'.liftOfIsRightKanExtension_fac_app α ((const D).obj c.pt)] + dsimp at this ⊢ + rw [← assoc, this, IsLimit.fac, NatTrans.comp_app, whiskerLeft_app]) + +variable [HasLimit F] [HasLimit F'] + +/-- If `F' : D ⥤ H` is a right Kan extension of `F : C ⥤ H` along `L : C ⥤ D`, the limit over `F'` +is isomorphic to the limit over `F`. -/ +noncomputable def limitIsoOfIsRightKanExtension : limit F' ≅ limit F := + IsLimit.conePointUniqueUpToIso (limit.isLimit F') + (F'.isLimitConeOfIsRightKanExtension α (limit.isLimit F)) + +@[reassoc (attr := simp)] +lemma limitIsoOfIsRightKanExtension_inv_π (i : C) : + (F'.limitIsoOfIsRightKanExtension α).inv ≫ limit.π F' (L.obj i) ≫ α.app i = limit.π F i := by + simp [limitIsoOfIsRightKanExtension] + +@[reassoc (attr := simp)] +lemma limitIsoOfIsRightKanExtension_hom_π (i : C) : + (F'.limitIsoOfIsRightKanExtension α).hom ≫ limit.π F i = limit.π F' (L.obj i) ≫ α.app i := by + rw [← Iso.eq_inv_comp, limitIsoOfIsRightKanExtension_inv_π] + +end Limit + end Functor end CategoryTheory diff --git a/Mathlib/CategoryTheory/Limits/Final.lean b/Mathlib/CategoryTheory/Limits/Final.lean index 8dea5b13733db..6390aaa372617 100644 --- a/Mathlib/CategoryTheory/Limits/Final.lean +++ b/Mathlib/CategoryTheory/Limits/Final.lean @@ -319,9 +319,21 @@ variable (G) https://stacks.math.columbia.edu/tag/04E7 -/ +@[simps! (config := .lemmasOnly)] def colimitIso [HasColimit G] : colimit (F ⋙ G) ≅ colimit G := asIso (colimit.pre G F) +/-- A pointfree version of `colimitIso`, stating that whiskering by `F` followed by taking the +colimit is isomorpic to taking the colimit on the codomain of `F`. -/ +def colimIso [HasColimitsOfShape D E] [HasColimitsOfShape C E] : + (whiskeringLeft _ _ _).obj F ⋙ colim ≅ colim (J := D) (C := E) := + NatIso.ofComponents (fun G => colimitIso F G) fun f => by + simp only [comp_obj, whiskeringLeft_obj_obj, colim_obj, comp_map, whiskeringLeft_obj_map, + colim_map, colimitIso_hom] + ext + simp only [comp_obj, ι_colimMap_assoc, whiskerLeft_app, colimit.ι_pre, colimit.ι_pre_assoc, + ι_colimMap] + end /-- Given a colimit cocone over `F ⋙ G` we can construct a colimit cocone over `G`. -/ @@ -342,24 +354,6 @@ include F in theorem hasColimitsOfShape_of_final [HasColimitsOfShape C E] : HasColimitsOfShape D E where has_colimit := fun _ => hasColimit_of_comp F -section - --- Porting note: this instance does not seem to be found automatically ---attribute [local instance] hasColimit_of_comp - -/-- When `F` is final, and `F ⋙ G` has a colimit, then `G` has a colimit also and -`colimit (F ⋙ G) ≅ colimit G` - -https://stacks.math.columbia.edu/tag/04E7 --/ -def colimitIso' [HasColimit (F ⋙ G)] : - haveI : HasColimit G := hasColimit_of_comp F - colimit (F ⋙ G) ≅ colimit G := - haveI : HasColimit G := hasColimit_of_comp F - asIso (colimit.pre G F) - -end - end Final end ArbitraryUniverse @@ -602,9 +596,20 @@ variable (G) https://stacks.math.columbia.edu/tag/04E7 -/ +@[simps! (config := .lemmasOnly)] def limitIso [HasLimit G] : limit (F ⋙ G) ≅ limit G := (asIso (limit.pre G F)).symm +/-- A pointfree version of `limitIso`, stating that whiskering by `F` followed by taking the +limit is isomorpic to taking the limit on the codomain of `F`. -/ +def limIso [HasLimitsOfShape D E] [HasLimitsOfShape C E] : + (whiskeringLeft _ _ _).obj F ⋙ lim ≅ lim (J := D) (C := E) := + Iso.symm <| NatIso.ofComponents (fun G => (limitIso F G).symm) fun f => by + simp only [comp_obj, whiskeringLeft_obj_obj, lim_obj, comp_map, whiskeringLeft_obj_map, lim_map, + Iso.symm_hom, limitIso_inv] + ext + simp + end /-- Given a limit cone over `F ⋙ G` we can construct a limit cone over `G`. -/ @@ -625,24 +630,6 @@ include F in theorem hasLimitsOfShape_of_initial [HasLimitsOfShape C E] : HasLimitsOfShape D E where has_limit := fun _ => hasLimit_of_comp F -section - --- Porting note: this instance does not seem to be found automatically --- attribute [local instance] hasLimit_of_comp - -/-- When `F` is initial, and `F ⋙ G` has a limit, then `G` has a limit also and -`limit (F ⋙ G) ≅ limit G` - -https://stacks.math.columbia.edu/tag/04E7 --/ -def limitIso' [HasLimit (F ⋙ G)] : - haveI : HasLimit G := hasLimit_of_comp F - limit (F ⋙ G) ≅ limit G := - haveI : HasLimit G := hasLimit_of_comp F - (asIso (limit.pre G F)).symm - -end - end Initial section diff --git a/Mathlib/Data/List/Infix.lean b/Mathlib/Data/List/Infix.lean index b7bf8b65b8356..030675eb9f683 100644 --- a/Mathlib/Data/List/Infix.lean +++ b/Mathlib/Data/List/Infix.lean @@ -70,6 +70,7 @@ theorem mem_of_mem_dropLast (h : a ∈ l.dropLast) : a ∈ l := dropLast_subset l h attribute [gcongr] Sublist.drop +attribute [refl] prefix_refl suffix_refl infix_refl theorem concat_get_prefix {x y : List α} (h : x <+: y) (hl : x.length < y.length) : x ++ [y.get ⟨x.length, hl⟩] <+: y := by diff --git a/Mathlib/Data/Set/Subset.lean b/Mathlib/Data/Set/Subset.lean index 675ae793d1bc8..6672f997e1bd5 100644 --- a/Mathlib/Data/Set/Subset.lean +++ b/Mathlib/Data/Set/Subset.lean @@ -112,8 +112,10 @@ lemma image_val_union_self_left_eq : ↑D ∪ A = A := union_eq_right.2 image_val_subset @[simp] -lemma cou_inter_self_right_eq_coe : A ∩ ↑D = ↑D := +lemma image_val_inter_self_right_eq_coe : A ∩ ↑D = ↑D := inter_eq_right.2 image_val_subset +@[deprecated (since := "2024-10-25")] +alias cou_inter_self_right_eq_coe := image_val_inter_self_right_eq_coe @[simp] lemma image_val_inter_self_left_eq_coe : ↑D ∩ A = ↑D := diff --git a/Mathlib/LinearAlgebra/Eigenspace/Basic.lean b/Mathlib/LinearAlgebra/Eigenspace/Basic.lean index d323e2e549474..05a16ab184670 100644 --- a/Mathlib/LinearAlgebra/Eigenspace/Basic.lean +++ b/Mathlib/LinearAlgebra/Eigenspace/Basic.lean @@ -519,10 +519,15 @@ theorem exp_ne_zero_of_hasGenEigenvalue {f : End R M} {μ : R} {k : ℕ} abbrev maxGenEigenspace (f : End R M) (μ : R) : Submodule R M := unifEigenspace f μ ⊤ -lemma maxGenEigenspace_def (f : End R M) (μ : R) : - f.maxGenEigenspace μ = ⨆ k, f.genEigenspace μ k := by +lemma iSup_genEigenspace_eq (f : End R M) (μ : R) : + ⨆ k, (f.genEigenspace μ) k = f.maxGenEigenspace μ := by simp_rw [maxGenEigenspace, unifEigenspace_top, genEigenspace, OrderHom.coe_mk] +@[deprecated iSup_genEigenspace_eq (since := "2024-10-23")] +lemma maxGenEigenspace_def (f : End R M) (μ : R) : + f.maxGenEigenspace μ = ⨆ k, f.genEigenspace μ k := + (iSup_genEigenspace_eq f μ).symm + theorem genEigenspace_le_maximal (f : End R M) (μ : R) (k : ℕ) : f.genEigenspace μ k ≤ f.maxGenEigenspace μ := (f.unifEigenspace μ).monotone le_top @@ -578,10 +583,12 @@ theorem genEigenspace_le_genEigenspace_finrank [FiniteDimensional K V] (f : End (μ : K) (k : ℕ) : f.genEigenspace μ k ≤ f.genEigenspace μ (finrank K V) := unifEigenspace_le_unifEigenspace_finrank _ _ _ -@[simp] theorem iSup_genEigenspace_eq_genEigenspace_finrank +theorem maxGenEigenspace_eq_genEigenspace_finrank [FiniteDimensional K V] (f : End K V) (μ : K) : - ⨆ k, f.genEigenspace μ k = f.genEigenspace μ (finrank K V) := - le_antisymm (iSup_le (genEigenspace_le_genEigenspace_finrank f μ)) (le_iSup _ _) + f.maxGenEigenspace μ = f.genEigenspace μ (finrank K V) := by + apply le_antisymm _ <| (f.unifEigenspace μ).monotone le_top + rw [unifEigenspace_top_eq_maxUnifEigenspaceIndex] + apply genEigenspace_le_genEigenspace_finrank f μ /-- Generalized eigenspaces for exponents at least `finrank K V` are equal to each other. -/ theorem genEigenspace_eq_genEigenspace_finrank_of_le [FiniteDimensional K V] @@ -590,31 +597,17 @@ theorem genEigenspace_eq_genEigenspace_finrank_of_le [FiniteDimensional K V] unifEigenspace_eq_unifEigenspace_finrank_of_le f μ hk lemma mapsTo_genEigenspace_of_comm {f g : End R M} (h : Commute f g) (μ : R) (k : ℕ) : - MapsTo g (f.genEigenspace μ k) (f.genEigenspace μ k) := by - replace h : Commute ((f - μ • (1 : End R M)) ^ k) g := - (h.sub_left <| Algebra.commute_algebraMap_left μ g).pow_left k - intro x hx - simp only [SetLike.mem_coe, mem_genEigenspace] at hx ⊢ - rw [← LinearMap.comp_apply, ← LinearMap.mul_eq_comp, h.eq, LinearMap.mul_eq_comp, - LinearMap.comp_apply, hx, map_zero] - -lemma iSup_genEigenspace_eq (f : End R M) (μ : R) : - ⨆ k, (f.genEigenspace μ) k = f.unifEigenspace μ ⊤ := by - rw [unifEigenspace_eq_iSup_unifEigenspace_nat] - ext - simp only [iSup_subtype, le_top, iSup_pos] - rfl + MapsTo g (f.genEigenspace μ k) (f.genEigenspace μ k) := + mapsTo_unifEigenspace_of_comm h μ k lemma mapsTo_maxGenEigenspace_of_comm {f g : End R M} (h : Commute f g) (μ : R) : - MapsTo g ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ) := by - rw [maxGenEigenspace_def] - simp only [MapsTo, Submodule.coe_iSup_of_chain, mem_iUnion, SetLike.mem_coe] - rintro x ⟨k, hk⟩ - exact ⟨k, f.mapsTo_genEigenspace_of_comm h μ k hk⟩ + MapsTo g ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ) := + mapsTo_unifEigenspace_of_comm h μ ⊤ +@[deprecated mapsTo_iSup_genEigenspace_of_comm (since := "2024-10-23")] lemma mapsTo_iSup_genEigenspace_of_comm {f g : End R M} (h : Commute f g) (μ : R) : MapsTo g ↑(⨆ k, f.genEigenspace μ k) ↑(⨆ k, f.genEigenspace μ k) := by - rw [← maxGenEigenspace_def] + rw [iSup_genEigenspace_eq] apply mapsTo_maxGenEigenspace_of_comm h /-- The restriction of `f - μ • 1` to the `k`-fold generalized `μ`-eigenspace is nilpotent. -/ @@ -636,7 +629,9 @@ lemma isNilpotent_restrict_maxGenEigenspace_sub_algebraMap [IsNoetherian R M] (f rw [maxGenEigenspace_eq] exact le_rfl +set_option linter.deprecated false in /-- The restriction of `f - μ • 1` to the generalized `μ`-eigenspace is nilpotent. -/ +@[deprecated isNilpotent_restrict_maxGenEigenspace_sub_algebraMap (since := "2024-10-23")] lemma isNilpotent_restrict_iSup_sub_algebraMap [IsNoetherian R M] (f : End R M) (μ : R) (h : MapsTo (f - algebraMap R (End R M) μ) ↑(⨆ k, f.genEigenspace μ k) ↑(⨆ k, f.genEigenspace μ k) := @@ -680,31 +675,40 @@ lemma disjoint_unifEigenspace [NoZeroSMulDivisors R M] isNilpotent_iff_eq_zero, sub_eq_zero] at this contradiction +lemma injOn_unifEigenspace [NoZeroSMulDivisors R M] (f : End R M) (k : ℕ∞) : + InjOn (f.unifEigenspace · k) {μ | f.unifEigenspace μ k ≠ ⊥} := by + rintro μ₁ _ μ₂ hμ₂ hμ₁₂ + by_contra contra + apply hμ₂ + simpa only [hμ₁₂, disjoint_self] using f.disjoint_unifEigenspace contra k k + lemma disjoint_genEigenspace [NoZeroSMulDivisors R M] (f : End R M) {μ₁ μ₂ : R} (hμ : μ₁ ≠ μ₂) (k l : ℕ) : Disjoint (f.genEigenspace μ₁ k) (f.genEigenspace μ₂ l) := disjoint_unifEigenspace f hμ k l +@[deprecated disjoint_unifEigenspace (since := "2024-10-23")] lemma disjoint_iSup_genEigenspace [NoZeroSMulDivisors R M] (f : End R M) {μ₁ μ₂ : R} (hμ : μ₁ ≠ μ₂) : Disjoint (⨆ k, f.genEigenspace μ₁ k) (⨆ k, f.genEigenspace μ₂ k) := by simpa only [iSup_genEigenspace_eq] using disjoint_unifEigenspace f hμ ⊤ ⊤ +lemma injOn_maxGenEigenspace [NoZeroSMulDivisors R M] (f : End R M) : + InjOn (f.maxGenEigenspace ·) {μ | f.maxGenEigenspace μ ≠ ⊥} := + injOn_unifEigenspace f ⊤ + +@[deprecated injOn_unifEigenspace (since := "2024-10-23")] lemma injOn_genEigenspace [NoZeroSMulDivisors R M] (f : End R M) : InjOn (⨆ k, f.genEigenspace · k) {μ | ⨆ k, f.genEigenspace μ k ≠ ⊥} := by - rintro μ₁ _ μ₂ hμ₂ (hμ₁₂ : ⨆ k, f.genEigenspace μ₁ k = ⨆ k, f.genEigenspace μ₂ k) - by_contra contra - apply hμ₂ - simpa only [hμ₁₂, disjoint_self] using f.disjoint_iSup_genEigenspace contra + simp_rw [iSup_genEigenspace_eq] + apply injOn_maxGenEigenspace -theorem independent_maxGenEigenspace [NoZeroSMulDivisors R M] (f : End R M) : - CompleteLattice.Independent f.maxGenEigenspace := by +theorem independent_unifEigenspace [NoZeroSMulDivisors R M] (f : End R M) (k : ℕ∞) : + CompleteLattice.Independent (f.unifEigenspace · k) := by classical - suffices ∀ μ (s : Finset R), μ ∉ s → Disjoint (⨆ k, f.genEigenspace μ k) - (s.sup fun μ ↦ ⨆ k, f.genEigenspace μ k) by - show CompleteLattice.Independent (f.maxGenEigenspace ·) - simp_rw [maxGenEigenspace_def, - CompleteLattice.independent_iff_supIndep_of_injOn f.injOn_genEigenspace, + suffices ∀ μ₁ (s : Finset R), μ₁ ∉ s → Disjoint (f.unifEigenspace μ₁ k) + (s.sup fun μ ↦ f.unifEigenspace μ k) by + simp_rw [CompleteLattice.independent_iff_supIndep_of_injOn (injOn_unifEigenspace f k), Finset.supIndep_iff_disjoint_erase] exact fun s μ _ ↦ this _ _ (s.not_mem_erase μ) intro μ₁ s @@ -716,38 +720,43 @@ theorem independent_maxGenEigenspace [NoZeroSMulDivisors R M] (f : End R M) : rw [Finset.sup_insert, disjoint_iff, Submodule.eq_bot_iff] rintro x ⟨hx, hx'⟩ simp only [SetLike.mem_coe] at hx hx' - suffices x ∈ ⨆ k, genEigenspace f μ₂ k by - rw [← Submodule.mem_bot (R := R), ← (f.disjoint_iSup_genEigenspace hμ₁₂).eq_bot] + suffices x ∈ unifEigenspace f μ₂ k by + rw [← Submodule.mem_bot (R := R), ← (f.disjoint_unifEigenspace hμ₁₂ k k).eq_bot] exact ⟨hx, this⟩ obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.mp hx'; clear hx' - let g := f - algebraMap R (End R M) μ₂ - obtain ⟨k : ℕ, hk : (g ^ k) y = 0⟩ := by simpa using hy - have hyz : (g ^ k) (y + z) ∈ - (⨆ k, genEigenspace f μ₁ k) ⊓ s.sup fun μ ↦ ⨆ k, f.genEigenspace μ k := by - refine ⟨f.mapsTo_iSup_genEigenspace_of_comm ?_ μ₁ hx, ?_⟩ - · exact Algebra.mul_sub_algebraMap_pow_commutes f μ₂ k - · rw [SetLike.mem_coe, map_add, hk, zero_add] - suffices (s.sup fun μ ↦ ⨆ k, f.genEigenspace μ k).map (g ^ k) ≤ - s.sup fun μ ↦ ⨆ k, f.genEigenspace μ k by exact this (Submodule.mem_map_of_mem hz) + let g := f - μ₂ • 1 + simp_rw [mem_unifEigenspace, ← exists_prop] at hy ⊢ + peel hy with l hlk hl + simp only [mem_unifEigenspace_nat, LinearMap.mem_ker] at hl + have hyz : (g ^ l) (y + z) ∈ + (f.unifEigenspace μ₁ k) ⊓ s.sup fun μ ↦ f.unifEigenspace μ k := by + refine ⟨f.mapsTo_unifEigenspace_of_comm (g := g ^ l) ?_ μ₁ k hx, ?_⟩ + · exact Algebra.mul_sub_algebraMap_pow_commutes f μ₂ l + · rw [SetLike.mem_coe, map_add, hl, zero_add] + suffices (s.sup fun μ ↦ f.unifEigenspace μ k).map (g ^ l) ≤ + s.sup fun μ ↦ f.unifEigenspace μ k by exact this (Submodule.mem_map_of_mem hz) simp_rw [Finset.sup_eq_iSup, Submodule.map_iSup (ι := R), Submodule.map_iSup (ι := _ ∈ s)] refine iSup₂_mono fun μ _ ↦ ?_ rintro - ⟨u, hu, rfl⟩ - refine f.mapsTo_iSup_genEigenspace_of_comm ?_ μ hu - exact Algebra.mul_sub_algebraMap_pow_commutes f μ₂ k - rw [ih.eq_bot, Submodule.mem_bot] at hyz - simp_rw [Submodule.mem_iSup_of_chain, mem_genEigenspace] - exact ⟨k, hyz⟩ + refine f.mapsTo_unifEigenspace_of_comm ?_ μ k hu + exact Algebra.mul_sub_algebraMap_pow_commutes f μ₂ l + rwa [ih.eq_bot, Submodule.mem_bot] at hyz + +theorem independent_maxGenEigenspace [NoZeroSMulDivisors R M] (f : End R M) : + CompleteLattice.Independent f.maxGenEigenspace := by + apply independent_unifEigenspace +@[deprecated independent_unifEigenspace (since := "2024-10-23")] theorem independent_genEigenspace [NoZeroSMulDivisors R M] (f : End R M) : CompleteLattice.Independent (fun μ ↦ ⨆ k, f.genEigenspace μ k) := by - simp_rw [← maxGenEigenspace_def] + simp_rw [iSup_genEigenspace_eq] apply independent_maxGenEigenspace /-- The eigenspaces of a linear operator form an independent family of subspaces of `M`. That is, any eigenspace has trivial intersection with the span of all the other eigenspaces. -/ theorem eigenspaces_independent [NoZeroSMulDivisors R M] (f : End R M) : CompleteLattice.Independent f.eigenspace := - f.independent_genEigenspace.mono fun μ ↦ le_iSup (genEigenspace f μ) 1 + (f.independent_unifEigenspace 1).mono fun _ ↦ le_rfl /-- Eigenvectors corresponding to distinct eigenvalues of a linear operator are linearly independent. -/ @@ -781,11 +790,28 @@ theorem genEigenspace_restrict (f : End R M) (p : Submodule R M) (k : ℕ) (μ : · erw [pow_succ, pow_succ, LinearMap.ker_comp, LinearMap.ker_comp, ih, ← LinearMap.ker_comp, LinearMap.comp_assoc] +/-- If `f` maps a subspace `p` into itself, then the generalized eigenspace of the restriction + of `f` to `p` is the part of the generalized eigenspace of `f` that lies in `p`. -/ +theorem unifEigenspace_restrict (f : End R M) (p : Submodule R M) (k : ℕ∞) (μ : R) + (hfp : ∀ x : M, x ∈ p → f x ∈ p) : + unifEigenspace (LinearMap.restrict f hfp) μ k = + Submodule.comap p.subtype (f.unifEigenspace μ k) := by + ext x + simp only [mem_unifEigenspace, LinearMap.mem_ker, ← mem_genEigenspace, genEigenspace_restrict, + Submodule.mem_comap] + +lemma _root_.Submodule.inf_unifEigenspace (f : End R M) (p : Submodule R M) {k : ℕ∞} {μ : R} + (hfp : ∀ x : M, x ∈ p → f x ∈ p) : + p ⊓ f.unifEigenspace μ k = + (unifEigenspace (LinearMap.restrict f hfp) μ k).map p.subtype := by + rw [f.unifEigenspace_restrict _ _ _ hfp, Submodule.map_comap_eq, Submodule.range_subtype] + +@[deprecated Submodule.inf_unifEigenspace (since := "2024-10-23")] lemma _root_.Submodule.inf_genEigenspace (f : End R M) (p : Submodule R M) {k : ℕ} {μ : R} (hfp : ∀ x : M, x ∈ p → f x ∈ p) : p ⊓ f.genEigenspace μ k = - (genEigenspace (LinearMap.restrict f hfp) μ k).map p.subtype := by - rw [f.genEigenspace_restrict _ _ _ hfp, Submodule.map_comap_eq, Submodule.range_subtype] + (genEigenspace (LinearMap.restrict f hfp) μ k).map p.subtype := + Submodule.inf_unifEigenspace _ _ _ 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} @@ -859,62 +885,97 @@ theorem map_genEigenrange_le {f : End K V} {μ : K} {n : ℕ} : rw [genEigenrange, unifEigenrange_nat] apply LinearMap.map_le_range +lemma unifEigenspace_le_smul (f : Module.End R M) (μ t : R) (k : ℕ∞) : + (f.unifEigenspace μ k) ≤ (t • f).unifEigenspace (t * μ) k := by + intro m hm + simp_rw [mem_unifEigenspace, ← exists_prop, LinearMap.mem_ker] at hm ⊢ + peel hm with l hlk hl + rw [mul_smul, ← smul_sub, smul_pow, LinearMap.smul_apply, hl, smul_zero] + +@[deprecated unifEigenspace_le_smul (since := "2024-10-23")] lemma iSup_genEigenspace_le_smul (f : Module.End R M) (μ t : R) : (⨆ k, f.genEigenspace μ k) ≤ ⨆ k, (t • f).genEigenspace (t * μ) k := by - intro m hm - simp only [Submodule.mem_iSup_of_chain, mem_genEigenspace] at hm ⊢ - refine Exists.imp (fun k hk ↦ ?_) hm - rw [mul_smul, ← smul_sub, smul_pow, LinearMap.smul_apply, hk, smul_zero] + rw [iSup_genEigenspace_eq, iSup_genEigenspace_eq] + apply unifEigenspace_le_smul -lemma iSup_genEigenspace_inf_le_add - (f₁ f₂ : End R M) (μ₁ μ₂ : R) (h : Commute f₁ f₂) : - (⨆ k, f₁.genEigenspace μ₁ k) ⊓ (⨆ k, f₂.genEigenspace μ₂ k) ≤ - ⨆ k, (f₁ + f₂).genEigenspace (μ₁ + μ₂) k := by +lemma unifEigenspace_inf_le_add + (f₁ f₂ : End R M) (μ₁ μ₂ : R) (k₁ k₂ : ℕ∞) (h : Commute f₁ f₂) : + (f₁.unifEigenspace μ₁ k₁) ⊓ (f₂.unifEigenspace μ₂ k₂) ≤ + (f₁ + f₂).unifEigenspace (μ₁ + μ₂) (k₁ + k₂) := by intro m hm - simp only [iSup_le_iff, Submodule.mem_inf, Submodule.mem_iSup_of_chain, - mem_genEigenspace] at hm ⊢ - obtain ⟨⟨k₁, hk₁⟩, ⟨k₂, hk₂⟩⟩ := hm - use k₁ + k₂ - 1 + simp only [Submodule.mem_inf, mem_unifEigenspace, LinearMap.mem_ker] at hm ⊢ + obtain ⟨⟨l₁, hlk₁, hl₁⟩, ⟨l₂, hlk₂, hl₂⟩⟩ := hm + use l₁ + l₂ have : f₁ + f₂ - (μ₁ + μ₂) • 1 = (f₁ - μ₁ • 1) + (f₂ - μ₂ • 1) := by rw [add_smul]; exact add_sub_add_comm f₁ f₂ (μ₁ • 1) (μ₂ • 1) replace h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1) := (h.sub_right <| Algebra.commute_algebraMap_right μ₂ f₁).sub_left (Algebra.commute_algebraMap_left μ₁ _) rw [this, h.add_pow', LinearMap.coeFn_sum, Finset.sum_apply] + constructor + · simpa only [Nat.cast_add] using add_le_add hlk₁ hlk₂ refine Finset.sum_eq_zero fun ⟨i, j⟩ hij ↦ ?_ suffices (((f₁ - μ₁ • 1) ^ i) * ((f₂ - μ₂ • 1) ^ j)) m = 0 by rw [LinearMap.smul_apply, this, smul_zero] - cases' Nat.le_or_le_of_add_eq_add_pred (Finset.mem_antidiagonal.mp hij) with hi hj - · rw [(h.pow_pow i j).eq, LinearMap.mul_apply, LinearMap.pow_map_zero_of_le hi hk₁, + rw [Finset.mem_antidiagonal] at hij + obtain hi|hj : l₁ ≤ i ∨ l₂ ≤ j := by omega + · rw [(h.pow_pow i j).eq, LinearMap.mul_apply, LinearMap.pow_map_zero_of_le hi hl₁, LinearMap.map_zero] - · rw [LinearMap.mul_apply, LinearMap.pow_map_zero_of_le hj hk₂, LinearMap.map_zero] + · rw [LinearMap.mul_apply, LinearMap.pow_map_zero_of_le hj hl₂, LinearMap.map_zero] -lemma map_smul_of_iInf_genEigenspace_ne_bot [NoZeroSMulDivisors R M] +@[deprecated unifEigenspace_inf_le_add (since := "2024-10-23")] +lemma iSup_genEigenspace_inf_le_add + (f₁ f₂ : End R M) (μ₁ μ₂ : R) (h : Commute f₁ f₂) : + (⨆ k, f₁.genEigenspace μ₁ k) ⊓ (⨆ k, f₂.genEigenspace μ₂ k) ≤ + ⨆ k, (f₁ + f₂).genEigenspace (μ₁ + μ₂) k := by + simp_rw [iSup_genEigenspace_eq] + apply unifEigenspace_inf_le_add + assumption + +lemma map_smul_of_iInf_unifEigenspace_ne_bot [NoZeroSMulDivisors R M] {L F : Type*} [SMul R L] [FunLike F L (End R M)] [MulActionHomClass F R L (End R M)] (f : F) - (μ : L → R) (h_ne : ⨅ x, ⨆ k, (f x).genEigenspace (μ x) k ≠ ⊥) + (μ : L → R) (k : ℕ∞) (h_ne : ⨅ x, (f x).unifEigenspace (μ x) k ≠ ⊥) (t : R) (x : L) : μ (t • x) = t • μ x := by by_contra contra - let g : L → Submodule R M := fun x ↦ ⨆ k, (f x).genEigenspace (μ x) k + let g : L → Submodule R M := fun x ↦ (f x).unifEigenspace (μ x) k have : ⨅ x, g x ≤ g x ⊓ g (t • x) := le_inf_iff.mpr ⟨iInf_le g x, iInf_le g (t • x)⟩ refine h_ne <| eq_bot_iff.mpr (le_trans this (disjoint_iff_inf_le.mp ?_)) - apply Disjoint.mono_left (iSup_genEigenspace_le_smul (f x) (μ x) t) + apply Disjoint.mono_left (unifEigenspace_le_smul (f x) (μ x) t k) simp only [g, map_smul] - exact disjoint_iSup_genEigenspace (t • f x) (Ne.symm contra) + exact disjoint_unifEigenspace (t • f x) (Ne.symm contra) k k -lemma map_add_of_iInf_genEigenspace_ne_bot_of_commute [NoZeroSMulDivisors R M] - {L F : Type*} [Add L] [FunLike F L (End R M)] [AddHomClass F L (End R M)] (f : F) +@[deprecated map_smul_of_iInf_unifEigenspace_ne_bot (since := "2024-10-23")] +lemma map_smul_of_iInf_genEigenspace_ne_bot [NoZeroSMulDivisors R M] + {L F : Type*} [SMul R L] [FunLike F L (End R M)] [MulActionHomClass F R L (End R M)] (f : F) (μ : L → R) (h_ne : ⨅ x, ⨆ k, (f x).genEigenspace (μ x) k ≠ ⊥) + (t : R) (x : L) : + μ (t • x) = t • μ x := by + simp_rw [iSup_genEigenspace_eq] at h_ne + apply map_smul_of_iInf_unifEigenspace_ne_bot f μ ⊤ h_ne t x + +lemma map_add_of_iInf_unifEigenspace_ne_bot_of_commute [NoZeroSMulDivisors R M] + {L F : Type*} [Add L] [FunLike F L (End R M)] [AddHomClass F L (End R M)] (f : F) + (μ : L → R) (k : ℕ∞) (h_ne : ⨅ x, (f x).unifEigenspace (μ x) k ≠ ⊥) (h : ∀ x y, Commute (f x) (f y)) (x y : L) : μ (x + y) = μ x + μ y := by by_contra contra - let g : L → Submodule R M := fun x ↦ ⨆ k, (f x).genEigenspace (μ x) k + let g : L → Submodule R M := fun x ↦ (f x).unifEigenspace (μ x) k have : ⨅ x, g x ≤ (g x ⊓ g y) ⊓ g (x + y) := le_inf_iff.mpr ⟨le_inf_iff.mpr ⟨iInf_le g x, iInf_le g y⟩, iInf_le g (x + y)⟩ refine h_ne <| eq_bot_iff.mpr (le_trans this (disjoint_iff_inf_le.mp ?_)) - apply Disjoint.mono_left (iSup_genEigenspace_inf_le_add (f x) (f y) (μ x) (μ y) (h x y)) + apply Disjoint.mono_left (unifEigenspace_inf_le_add (f x) (f y) (μ x) (μ y) k k (h x y)) simp only [g, map_add] - exact disjoint_iSup_genEigenspace (f x + f y) (Ne.symm contra) + exact disjoint_unifEigenspace (f x + f y) (Ne.symm contra) _ k + +@[deprecated map_add_of_iInf_unifEigenspace_ne_bot_of_commute (since := "2024-10-23")] +lemma map_add_of_iInf_genEigenspace_ne_bot_of_commute [NoZeroSMulDivisors R M] + {L F : Type*} [Add L] [FunLike F L (End R M)] [AddHomClass F L (End R M)] (f : F) + (μ : L → R) (h_ne : ⨅ x, ⨆ k, (f x).genEigenspace (μ x) k ≠ ⊥) + (h : ∀ x y, Commute (f x) (f y)) (x y : L) : + μ (x + y) = μ x + μ y := by + simp_rw [iSup_genEigenspace_eq] at h_ne + apply map_add_of_iInf_unifEigenspace_ne_bot_of_commute f μ ⊤ h_ne h x y end End diff --git a/Mathlib/LinearAlgebra/Eigenspace/Pi.lean b/Mathlib/LinearAlgebra/Eigenspace/Pi.lean index 3eeacc0153eb7..2980b51c48875 100644 --- a/Mathlib/LinearAlgebra/Eigenspace/Pi.lean +++ b/Mathlib/LinearAlgebra/Eigenspace/Pi.lean @@ -45,8 +45,7 @@ lemma _root_.Submodule.inf_iInf_maxGenEigenspace_of_forall_mapsTo {μ : ι → R (⨅ 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_def, ((f _).genEigenspace _).mono.directed_le.inf_iSup_eq, - p.inf_genEigenspace _ (hfp _), ← Submodule.map_iSup, Submodule.map_iInf _ p.injective_subtype] + · simp_rw [inf_iInf, p.inf_unifEigenspace _ (hfp _), 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`, @@ -64,8 +63,10 @@ lemma iInf_maxGenEigenspace_restrict_map_subtype_eq 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 _)] + conv_rhs => + enter [1] + ext + rw [p.inf_unifEigenspace (f _) (h _)] variable [NoZeroSMulDivisors R M] @@ -166,8 +167,7 @@ lemma iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo [FiniteDimensional K M] apply ih _ (hy φ) · intro j k μ exact mapsTo_restrict_maxGenEigenspace_restrict_of_mapsTo (f j) (f k) _ _ (h j k μ) - · simp_rw [maxGenEigenspace_def] at h' ⊢ - exact fun j ↦ Module.End.iSup_genEigenspace_restrict_eq_top _ (h' j) + · exact fun j ↦ Module.End.unifEigenspace_restrict_eq_top _ (h' j) · rfl replace ih (φ : K) : ⨆ (χ : ι → K) (_ : χ i = φ), ⨅ j, maxGenEigenspace ((f j).restrict (hi j φ)) (χ j) = ⊤ := by @@ -177,8 +177,7 @@ lemma iSup_iInf_maxGenEigenspace_eq_top_of_forall_mapsTo [FiniteDimensional K M] 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] - simp_rw [maxGenEigenspace_def] - exact ((f i).disjoint_iSup_genEigenspace hχ.symm).mono_right (iInf_le _ i) + exact ((f i).disjoint_unifEigenspace hχ.symm _ _).mono_right (iInf_le _ i) replace ih (φ : K) : ⨆ (χ : ι → K) (_ : χ i = φ), ⨅ j, maxGenEigenspace (f j) (χ j) = maxGenEigenspace (f i) φ := by diff --git a/Mathlib/LinearAlgebra/Eigenspace/Semisimple.lean b/Mathlib/LinearAlgebra/Eigenspace/Semisimple.lean index 96229aa54786f..26ccc18c96849 100644 --- a/Mathlib/LinearAlgebra/Eigenspace/Semisimple.lean +++ b/Mathlib/LinearAlgebra/Eigenspace/Semisimple.lean @@ -26,17 +26,20 @@ namespace Module.End variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] {f g : End R M} lemma apply_eq_of_mem_of_comm_of_isFinitelySemisimple_of_isNil - {μ : R} {k : ℕ} {m : M} (hm : m ∈ f.genEigenspace μ k) + {μ : R} {k : ℕ∞} {m : M} (hm : m ∈ f.unifEigenspace μ k) (hfg : Commute f g) (hss : g.IsFinitelySemisimple) (hnil : IsNilpotent (f - g)) : g m = μ • m := by - set p := f.genEigenspace μ k - have h₁ : MapsTo g p p := mapsTo_genEigenspace_of_comm hfg μ k + rw [f.mem_unifEigenspace] at hm + obtain ⟨l, -, hm⟩ := hm + rw [LinearMap.mem_ker, ← f.mem_genEigenspace] at hm + set p := f.genEigenspace μ l + have h₁ : MapsTo g p p := mapsTo_unifEigenspace_of_comm hfg μ l have h₂ : MapsTo (g - algebraMap R (End R M) μ) p p := - mapsTo_genEigenspace_of_comm (hfg.sub_right <| Algebra.commute_algebraMap_right μ f) μ k + mapsTo_unifEigenspace_of_comm (hfg.sub_right <| Algebra.commute_algebraMap_right μ f) μ l have h₃ : MapsTo (f - g) p p := - mapsTo_genEigenspace_of_comm (Commute.sub_right rfl hfg) μ k + mapsTo_unifEigenspace_of_comm (Commute.sub_right rfl hfg) μ l have h₄ : MapsTo (f - algebraMap R (End R M) μ) p p := - mapsTo_genEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f μ) μ k + mapsTo_unifEigenspace_of_comm (Algebra.mul_sub_algebraMap_commutes f μ) μ l replace hfg : Commute (f - algebraMap R (End R M) μ) (f - g) := (Commute.sub_right rfl hfg).sub_left <| Algebra.commute_algebraMap_left μ (f - g) suffices IsNilpotent ((g - algebraMap R (End R M) μ).restrict h₂) by @@ -44,7 +47,15 @@ lemma apply_eq_of_mem_of_comm_of_isFinitelySemisimple_of_isNil eq_zero_of_isNilpotent_of_isFinitelySemisimple this (by simpa using hss.restrict _) simpa [LinearMap.restrict_apply, sub_eq_zero] using LinearMap.congr_fun this ⟨m, hm⟩ simpa [LinearMap.restrict_sub h₄ h₃] using (LinearMap.restrict_commute hfg h₄ h₃).isNilpotent_sub - (f.isNilpotent_restrict_sub_algebraMap μ k) (Module.End.isNilpotent.restrict h₃ hnil) + (f.isNilpotent_restrict_sub_algebraMap μ l) (Module.End.isNilpotent.restrict h₃ hnil) + +lemma IsFinitelySemisimple.unifEigenspace_eq_eigenspace + (hf : f.IsFinitelySemisimple) (μ : R) {k : ℕ∞} (hk : 0 < k) : + f.unifEigenspace μ k = f.eigenspace μ := by + refine le_antisymm (fun m hm ↦ mem_eigenspace_iff.mpr ?_) (f.unifEigenspace μ |>.mono ?_) + · apply apply_eq_of_mem_of_comm_of_isFinitelySemisimple_of_isNil hm rfl hf + simp + · exact Order.one_le_iff_pos.mpr hk lemma IsFinitelySemisimple.genEigenspace_eq_eigenspace (hf : f.IsFinitelySemisimple) (μ : R) {k : ℕ} (hk : 0 < k) : @@ -54,8 +65,7 @@ lemma IsFinitelySemisimple.genEigenspace_eq_eigenspace lemma IsFinitelySemisimple.maxGenEigenspace_eq_eigenspace (hf : f.IsFinitelySemisimple) (μ : R) : - f.maxGenEigenspace μ = f.eigenspace μ := by - simp_rw [maxGenEigenspace_def, ← (f.genEigenspace μ).monotone.iSup_nat_add 1, - hf.genEigenspace_eq_eigenspace μ (Nat.zero_lt_succ _), ciSup_const] + f.maxGenEigenspace μ = f.eigenspace μ := + hf.unifEigenspace_eq_eigenspace μ ENat.top_pos end Module.End diff --git a/Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean b/Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean index e619e16819564..4ac57d9a9c04a 100644 --- a/Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean +++ b/Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean @@ -45,16 +45,20 @@ variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V] namespace Module.End +theorem exists_hasEigenvalue_of_unifEigenspace_eq_top [Nontrivial M] {f : End R M} (k : ℕ∞) + (hf : ⨆ μ, f.unifEigenspace μ k = ⊤) : + ∃ μ, f.HasEigenvalue μ := by + suffices ∃ μ, f.HasUnifEigenvalue μ k by + peel this with μ hμ + exact HasUnifEigenvalue.lt zero_lt_one hμ + simp [HasUnifEigenvalue, ← not_forall, ← iSup_eq_bot, hf] + +@[deprecated exists_hasEigenvalue_of_unifEigenspace_eq_top (since := "2024-10-11")] theorem exists_hasEigenvalue_of_iSup_genEigenspace_eq_top [Nontrivial M] {f : End R M} (hf : ⨆ μ, ⨆ k, f.genEigenspace μ k = ⊤) : ∃ μ, f.HasEigenvalue μ := by - by_contra! contra - suffices ∀ μ, ⨆ k, f.genEigenspace μ k = ⊥ by simp [this] at hf - intro μ - replace contra : ∀ k, f.genEigenspace μ k = ⊥ := fun k ↦ by - have hk : ¬ f.HasGenEigenvalue μ k := fun hk ↦ contra μ (f.hasEigenvalue_of_hasGenEigenvalue hk) - rwa [hasGenEigenvalue_iff, not_not] at hk - simp [contra] + simp_rw [iSup_genEigenspace_eq] at hf + apply exists_hasEigenvalue_of_unifEigenspace_eq_top _ hf -- This is Lemma 5.21 of [axler2015], although we are no longer following that proof. /-- In finite dimensions, over an algebraically closed field, every linear endomorphism has an @@ -71,8 +75,8 @@ noncomputable instance [IsAlgClosed K] [FiniteDimensional K V] [Nontrivial V] (f -- Lemma 8.21 of [axler2015] /-- In finite dimensions, over an algebraically closed field, the generalized eigenspaces of any linear endomorphism span the whole space. -/ -theorem iSup_genEigenspace_eq_top [IsAlgClosed K] [FiniteDimensional K V] (f : End K V) : - ⨆ (μ : K) (k : ℕ), f.genEigenspace μ k = ⊤ := by +theorem iSup_maxGenEigenspace_eq_top [IsAlgClosed K] [FiniteDimensional K V] (f : End K V) : + ⨆ (μ : K), f.maxGenEigenspace μ = ⊤ := by -- We prove the claim by strong induction on the dimension of the vector space. induction' h_dim : finrank K V using Nat.strong_induction_on with n ih generalizing V cases' n with n @@ -105,57 +109,68 @@ theorem iSup_genEigenspace_eq_top [IsAlgClosed K] [FiniteDimensional K V] (f : E -- Therefore the dimension `ER` mus be smaller than `finrank K V`. have h_dim_ER : finrank K ER < n.succ := by linarith -- This allows us to apply the induction hypothesis on `ER`: - have ih_ER : ⨆ (μ : K) (k : ℕ), f'.genEigenspace μ k = ⊤ := + have ih_ER : ⨆ (μ : K), f'.maxGenEigenspace μ = ⊤ := ih (finrank K ER) h_dim_ER f' rfl -- The induction hypothesis gives us a statement about subspaces of `ER`. We can transfer this -- to a statement about subspaces of `V` via `Submodule.subtype`: - have ih_ER' : ⨆ (μ : K) (k : ℕ), (f'.genEigenspace μ k).map ER.subtype = ER := by + have ih_ER' : ⨆ (μ : K), (f'.maxGenEigenspace μ).map ER.subtype = ER := by simp only [(Submodule.map_iSup _ _).symm, ih_ER, Submodule.map_subtype_top ER] -- Moreover, every generalized eigenspace of `f'` is contained in the corresponding generalized -- eigenspace of `f`. have hff' : - ∀ μ k, (f'.genEigenspace μ k).map ER.subtype ≤ f.genEigenspace μ k := by + ∀ μ, (f'.maxGenEigenspace μ).map ER.subtype ≤ f.maxGenEigenspace μ := by intros - rw [genEigenspace_restrict] + rw [maxGenEigenspace, unifEigenspace_restrict] apply Submodule.map_comap_le -- It follows that `ER` is contained in the span of all generalized eigenvectors. - have hER : ER ≤ ⨆ (μ : K) (k : ℕ), f.genEigenspace μ k := by + have hER : ER ≤ ⨆ (μ : K), f.maxGenEigenspace μ := by rw [← ih_ER'] - exact iSup₂_mono hff' + exact iSup_mono hff' -- `ES` is contained in this span by definition. - have hES : ES ≤ ⨆ (μ : K) (k : ℕ), f.genEigenspace μ k := - le_trans (le_iSup (fun k => f.genEigenspace μ₀ k) (finrank K V)) - (le_iSup (fun μ : K => ⨆ k : ℕ, f.genEigenspace μ k) μ₀) + have hES : ES ≤ ⨆ (μ : K), f.maxGenEigenspace μ := + ((f.unifEigenspace μ₀).mono le_top).trans (le_iSup f.maxGenEigenspace μ₀) -- Moreover, we know that `ER` and `ES` are disjoint. have h_disjoint : Disjoint ER ES := generalized_eigenvec_disjoint_range_ker f μ₀ -- Since the dimensions of `ER` and `ES` add up to the dimension of `V`, it follows that the -- span of all generalized eigenvectors is all of `V`. - show ⨆ (μ : K) (k : ℕ), f.genEigenspace μ k = ⊤ + show ⨆ (μ : K), f.maxGenEigenspace μ = ⊤ rw [← top_le_iff, ← Submodule.eq_top_of_disjoint ER ES h_dim_add h_disjoint] apply sup_le hER hES +-- Lemma 8.21 of [axler2015] +/-- In finite dimensions, over an algebraically closed field, the generalized eigenspaces of any +linear endomorphism span the whole space. -/ +@[deprecated iSup_maxGenEigenspace_eq_top (since := "2024-10-11")] +theorem iSup_genEigenspace_eq_top [IsAlgClosed K] [FiniteDimensional K V] (f : End K V) : + ⨆ (μ : K) (k : ℕ), f.genEigenspace μ k = ⊤ := by + simp_rw [iSup_genEigenspace_eq] + apply iSup_maxGenEigenspace_eq_top + end Module.End namespace Submodule variable {p : Submodule K V} {f : Module.End K V} -theorem inf_iSup_genEigenspace [FiniteDimensional K V] (h : ∀ x ∈ p, f x ∈ p) : - p ⊓ ⨆ μ, ⨆ k, f.genEigenspace μ k = ⨆ μ, ⨆ k, p ⊓ f.genEigenspace μ k := by - simp_rw [← (f.genEigenspace _).mono.directed_le.inf_iSup_eq] +theorem inf_iSup_unifEigenspace [FiniteDimensional K V] (h : ∀ x ∈ p, f x ∈ p) (k : ℕ∞) : + p ⊓ ⨆ μ, f.unifEigenspace μ k = ⨆ μ, p ⊓ f.unifEigenspace μ k := by refine le_antisymm (fun m hm ↦ ?_) (le_inf_iff.mpr ⟨iSup_le fun μ ↦ inf_le_left, iSup_mono fun μ ↦ inf_le_right⟩) classical - obtain ⟨hm₀ : m ∈ p, hm₁ : m ∈ ⨆ μ, ⨆ k, f.genEigenspace μ k⟩ := hm + obtain ⟨hm₀ : m ∈ p, hm₁ : m ∈ ⨆ μ, f.unifEigenspace μ k⟩ := hm obtain ⟨m, hm₂, rfl⟩ := (mem_iSup_iff_exists_finsupp _ _).mp hm₁ suffices ∀ μ, (m μ : V) ∈ p by exact (mem_iSup_iff_exists_finsupp _ _).mpr ⟨m, fun μ ↦ mem_inf.mp ⟨this μ, hm₂ μ⟩, rfl⟩ intro μ by_cases hμ : μ ∈ m.support; swap · simp only [Finsupp.not_mem_support_iff.mp hμ, p.zero_mem] + have hm₂_aux := hm₂ + simp_rw [Module.End.mem_unifEigenspace] at hm₂_aux + choose l hlk hl using hm₂_aux + let l₀ : ℕ := m.support.sup l have h_comm : ∀ (μ₁ μ₂ : K), - Commute ((f - algebraMap K (End K V) μ₁) ^ finrank K V) - ((f - algebraMap K (End K V) μ₂) ^ finrank K V) := fun μ₁ μ₂ ↦ + Commute ((f - algebraMap K (End K V) μ₁) ^ l₀) + ((f - algebraMap K (End K V) μ₂) ^ l₀) := fun μ₁ μ₂ ↦ ((Commute.sub_right rfl <| Algebra.commute_algebraMap_right _ _).sub_left (Algebra.commute_algebraMap_left _ _)).pow_pow _ _ let g : End K V := (m.support.erase μ).noncommProd _ fun μ₁ _ μ₂ _ _ ↦ h_comm μ₁ μ₂ @@ -168,42 +183,72 @@ theorem inf_iSup_genEigenspace [FiniteDimensional K V] (h : ∀ x ∈ p, f x ∈ rintro μ' hμ' split_ifs with hμμ' · rw [hμμ'] - replace hm₂ : ((f - algebraMap K (End K V) μ') ^ finrank K V) (m μ') = 0 := by - obtain ⟨k, hk⟩ := (mem_iSup_of_chain _ _).mp (hm₂ μ') - simpa only [End.mem_genEigenspace] using - Module.End.genEigenspace_le_genEigenspace_finrank _ _ k hk + have hl₀ : ((f - algebraMap K (End K V) μ') ^ l₀) (m μ') = 0 := by + rw [← LinearMap.mem_ker, Algebra.algebraMap_eq_smul_one, ← End.mem_unifEigenspace_nat] + simp_rw [← End.mem_unifEigenspace_nat] at hl + suffices (l μ' : ℕ∞) ≤ l₀ from (f.unifEigenspace μ').mono this (hl μ') + simpa only [Nat.cast_le] using Finset.le_sup hμ' have : _ = g := (m.support.erase μ).noncommProd_erase_mul (Finset.mem_erase.mpr ⟨hμμ', hμ'⟩) - (fun μ ↦ (f - algebraMap K (End K V) μ) ^ finrank K V) (fun μ₁ _ μ₂ _ _ ↦ h_comm μ₁ μ₂) - rw [← this, LinearMap.mul_apply, hm₂, _root_.map_zero] + (fun μ ↦ (f - algebraMap K (End K V) μ) ^ l₀) (fun μ₁ _ μ₂ _ _ ↦ h_comm μ₁ μ₂) + rw [← this, LinearMap.mul_apply, hl₀, _root_.map_zero] have hg₁ : MapsTo g p p := Finset.noncommProd_induction _ _ _ (fun g' : End K V ↦ MapsTo g' p p) (fun f₁ f₂ ↦ MapsTo.comp) (mapsTo_id _) fun μ' _ ↦ by suffices MapsTo (f - algebraMap K (End K V) μ') p p by - simp only [LinearMap.coe_pow]; exact this.iterate (finrank K V) + simp only [LinearMap.coe_pow]; exact this.iterate l₀ intro x hx rw [LinearMap.sub_apply, algebraMap_end_apply] exact p.sub_mem (h _ hx) (smul_mem p μ' hx) - have hg₂ : MapsTo g ↑(⨆ k, f.genEigenspace μ k) ↑(⨆ k, f.genEigenspace μ k) := - f.mapsTo_iSup_genEigenspace_of_comm hfg μ - have hg₃ : InjOn g ↑(⨆ k, f.genEigenspace μ k) := by + have hg₂ : MapsTo g ↑(f.unifEigenspace μ k) ↑(f.unifEigenspace μ k) := + f.mapsTo_unifEigenspace_of_comm hfg μ k + have hg₃ : InjOn g ↑(f.unifEigenspace μ k) := by apply LinearMap.injOn_of_disjoint_ker (subset_refl _) - have this := f.independent_genEigenspace - simp_rw [f.iSup_genEigenspace_eq_genEigenspace_finrank] at this ⊢ + have this := f.independent_unifEigenspace k + have aux (μ') (_hμ' : μ' ∈ m.support.erase μ) : + (f.unifEigenspace μ') ↑l₀ ≤ (f.unifEigenspace μ') k := by + apply (f.unifEigenspace μ').mono + rintro k rfl + simp only [ENat.some_eq_coe, Nat.cast_inj, exists_eq_left'] + apply Finset.sup_le + intro i _hi + simpa using hlk i rw [LinearMap.ker_noncommProd_eq_of_supIndep_ker, ← Finset.sup_eq_iSup] - · simpa only [End.genEigenspace_def] using - Finset.supIndep_iff_disjoint_erase.mp (this.supIndep' m.support) μ hμ - · simpa only [End.genEigenspace_def] using this.supIndep' (m.support.erase μ) + · have := Finset.supIndep_iff_disjoint_erase.mp (this.supIndep' m.support) μ hμ + apply this.mono_right + apply Finset.sup_mono_fun + intro μ' hμ' + rw [Algebra.algebraMap_eq_smul_one, ← End.unifEigenspace_nat] + apply aux μ' hμ' + · have := this.supIndep' (m.support.erase μ) + apply Finset.supIndep_antimono_fun _ this + intro μ' hμ' + rw [Algebra.algebraMap_eq_smul_one, ← End.unifEigenspace_nat] + apply aux μ' hμ' have hg₄ : SurjOn g - ↑(p ⊓ ⨆ k, f.genEigenspace μ k) ↑(p ⊓ ⨆ k, f.genEigenspace μ k) := by + ↑(p ⊓ f.unifEigenspace μ k) ↑(p ⊓ f.unifEigenspace μ k) := by have : MapsTo g - ↑(p ⊓ ⨆ k, f.genEigenspace μ k) ↑(p ⊓ ⨆ k, f.genEigenspace μ k) := + ↑(p ⊓ f.unifEigenspace μ k) ↑(p ⊓ f.unifEigenspace μ k) := hg₁.inter_inter hg₂ rw [← LinearMap.injOn_iff_surjOn this] exact hg₃.mono inter_subset_right specialize hm₂ μ - obtain ⟨y, ⟨hy₀ : y ∈ p, hy₁ : y ∈ ⨆ k, f.genEigenspace μ k⟩, hy₂ : g y = g (m μ)⟩ := + obtain ⟨y, ⟨hy₀ : y ∈ p, hy₁ : y ∈ f.unifEigenspace μ k⟩, hy₂ : g y = g (m μ)⟩ := hg₄ ⟨(hg₀ ▸ hg₁ hm₀), hg₂ hm₂⟩ rwa [← hg₃ hy₁ hm₂ hy₂] +set_option linter.deprecated false in +@[deprecated inf_iSup_unifEigenspace (since := "2024-10-11")] +theorem inf_iSup_genEigenspace [FiniteDimensional K V] (h : ∀ x ∈ p, f x ∈ p) : + p ⊓ ⨆ μ, ⨆ k, f.genEigenspace μ k = ⨆ μ, ⨆ k, p ⊓ f.genEigenspace μ k := by + simp_rw [← (f.genEigenspace _).mono.directed_le.inf_iSup_eq, f.iSup_genEigenspace_eq] + apply inf_iSup_unifEigenspace h ⊤ + +theorem eq_iSup_inf_unifEigenspace [FiniteDimensional K V] (k : ℕ∞) + (h : ∀ x ∈ p, f x ∈ p) (h' : ⨆ μ, f.unifEigenspace μ k = ⊤) : + p = ⨆ μ, p ⊓ f.unifEigenspace μ k := by + rw [← inf_iSup_unifEigenspace h, h', inf_top_eq] + +set_option linter.deprecated false in +@[deprecated eq_iSup_inf_unifEigenspace (since := "2024-10-11")] theorem eq_iSup_inf_genEigenspace [FiniteDimensional K V] (h : ∀ x ∈ p, f x ∈ p) (h' : ⨆ μ, ⨆ k, f.genEigenspace μ k = ⊤) : p = ⨆ μ, ⨆ k, p ⊓ f.genEigenspace μ k := by @@ -213,12 +258,22 @@ end Submodule /-- In finite dimensions, if the generalized eigenspaces of a linear endomorphism span the whole space then the same is true of its restriction to any invariant submodule. -/ +theorem Module.End.unifEigenspace_restrict_eq_top + {p : Submodule K V} {f : Module.End K V} [FiniteDimensional K V] {k : ℕ∞} + (h : ∀ x ∈ p, f x ∈ p) (h' : ⨆ μ, f.unifEigenspace μ k = ⊤) : + ⨆ μ, Module.End.unifEigenspace (LinearMap.restrict f h) μ k = ⊤ := by + have := congr_arg (Submodule.comap p.subtype) (Submodule.eq_iSup_inf_unifEigenspace k h h') + have h_inj : Function.Injective p.subtype := Subtype.coe_injective + simp_rw [Submodule.inf_unifEigenspace f p h, Submodule.comap_subtype_self, + ← Submodule.map_iSup, Submodule.comap_map_eq_of_injective h_inj] at this + exact this.symm + +/-- In finite dimensions, if the generalized eigenspaces of a linear endomorphism span the whole +space then the same is true of its restriction to any invariant submodule. -/ +@[deprecated Module.End.unifEigenspace_restrict_eq_top (since := "2024-10-11")] theorem Module.End.iSup_genEigenspace_restrict_eq_top {p : Submodule K V} {f : Module.End K V} [FiniteDimensional K V] (h : ∀ x ∈ p, f x ∈ p) (h' : ⨆ μ, ⨆ k, f.genEigenspace μ k = ⊤) : ⨆ μ, ⨆ k, Module.End.genEigenspace (LinearMap.restrict f h) μ k = ⊤ := by - have := congr_arg (Submodule.comap p.subtype) (Submodule.eq_iSup_inf_genEigenspace h h') - have h_inj : Function.Injective p.subtype := Subtype.coe_injective - 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 + simp_rw [iSup_genEigenspace_eq] at h' ⊢ + apply Module.End.unifEigenspace_restrict_eq_top h h' diff --git a/Mathlib/LinearAlgebra/Eigenspace/Zero.lean b/Mathlib/LinearAlgebra/Eigenspace/Zero.lean index 30837353e1b0a..cbae5ab149388 100644 --- a/Mathlib/LinearAlgebra/Eigenspace/Zero.lean +++ b/Mathlib/LinearAlgebra/Eigenspace/Zero.lean @@ -132,7 +132,7 @@ lemma finrank_maxGenEigenspace (φ : Module.End K M) : finrank K (φ.maxGenEigenspace 0) = natTrailingDegree (φ.charpoly) := by set V := φ.maxGenEigenspace 0 have hV : V = ⨆ (n : ℕ), ker (φ ^ n) := by - simp [V, Module.End.maxGenEigenspace_def, Module.End.genEigenspace_def] + simp [V, ← Module.End.iSup_genEigenspace_eq, Module.End.genEigenspace_def] let W := ⨅ (n : ℕ), LinearMap.range (φ ^ n) have hVW : IsCompl V W := by rw [hV] diff --git a/Mathlib/MeasureTheory/Measure/Dirac.lean b/Mathlib/MeasureTheory/Measure/Dirac.lean index 29e9d534230ce..bf8d888f3eea2 100644 --- a/Mathlib/MeasureTheory/Measure/Dirac.lean +++ b/Mathlib/MeasureTheory/Measure/Dirac.lean @@ -80,6 +80,14 @@ theorem restrict_singleton (μ : Measure α) (a : α) : μ.restrict {a} = μ {a} · have : s ∩ {a} = ∅ := inter_singleton_eq_empty.2 ha simp [*] +/-- Two measures on a countable space are equal if they agree on singletons. -/ +theorem ext_of_singleton [Countable α] {μ ν : Measure α} (h : ∀ a, μ {a} = ν {a}) : μ = ν := + ext_of_sUnion_eq_univ (countable_range singleton) (by aesop) (by aesop) + +/-- Two measures on a countable space are equal if and only if they agree on singletons. -/ +theorem ext_iff_singleton [Countable α] {μ ν : Measure α} : μ = ν ↔ ∀ a, μ {a} = ν {a} := + ⟨fun h _ ↦ h ▸ rfl, ext_of_singleton⟩ + /-- If `f` is a map with countable codomain, then `μ.map f` is a sum of Dirac measures. -/ theorem map_eq_sum [Countable β] [MeasurableSingletonClass β] (μ : Measure α) (f : α → β) (hf : Measurable f) : μ.map f = sum fun b : β => μ (f ⁻¹' {b}) • dirac b := by diff --git a/Mathlib/Order/SupIndep.lean b/Mathlib/Order/SupIndep.lean index cb3c3c12cac6a..19f1467d5960c 100644 --- a/Mathlib/Order/SupIndep.lean +++ b/Mathlib/Order/SupIndep.lean @@ -94,6 +94,29 @@ theorem supIndep_iff_disjoint_erase [DecidableEq ι] : ⟨fun hs _ hi => hs (erase_subset _ _) hi (not_mem_erase _ _), fun hs _ ht i hi hit => (hs i hi).mono_right (sup_mono fun _ hj => mem_erase.2 ⟨ne_of_mem_of_not_mem hj hit, ht hj⟩)⟩ +theorem supIndep_antimono_fun {g : ι → α} (h : ∀ x ∈ s, f x ≤ g x) (h : s.SupIndep g) : + s.SupIndep f := by + classical + induction s using Finset.induction_on with + | empty => apply Finset.supIndep_empty + | @insert i s his IH => + rename_i hle + rw [Finset.supIndep_iff_disjoint_erase] at h ⊢ + intro j hj + simp_all only [Finset.mem_insert, or_true, implies_true, true_implies, forall_eq_or_imp, + Finset.erase_insert_eq_erase, not_false_eq_true, Finset.erase_eq_of_not_mem] + obtain rfl | hj := hj + · simp only [Finset.erase_insert_eq_erase] + apply h.left.mono hle.left + apply (Finset.sup_mono _).trans (Finset.sup_mono_fun hle.right) + exact Finset.erase_subset _ _ + · apply (h.right j hj).mono (hle.right j hj) (Finset.sup_mono_fun _) + intro k hk + simp only [Finset.mem_erase, ne_eq, Finset.mem_insert] at hk + obtain ⟨-, rfl | hk⟩ := hk + · exact hle.left + · exact hle.right k hk + theorem SupIndep.image [DecidableEq ι] {s : Finset ι'} {g : ι' → ι} (hs : s.SupIndep (f ∘ g)) : (s.image g).SupIndep f := by intro t ht i hi hit diff --git a/lake-manifest.json b/lake-manifest.json index f6b641e2a0b8c..ab608786a1b29 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4e209effe5c38bb592c11e4ad06f7796980175cc", + "rev": "ee4b11ddc59ae83d8a31f69c99943a05d90519b2", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "fin-coding",