Trigger CI for leanprover-community/batteries#1007

Author: leanprover-community-mathlib4-bot

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)

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,25 +686,26 @@ 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) :
     ⨆ (φ : R), genWeightSpaceOf M φ x = ⊤ := by
   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

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] }
 

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]
 

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

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

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