bump to nightly-2023-06-08-03

mathlib commit leanprover-community/mathlib@31c24aa

Mathbin/Algebra/Category/Module/Colimits.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 
 ! This file was ported from Lean 3 source module algebra.category.Module.colimits
-! leanprover-community/mathlib commit 5a684ce82399d820475609907c6ef8dba5b1b97c
+! leanprover-community/mathlib commit c20927220ef87bb4962ba08bf6da2ce3cf50a6dd
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.CategoryTheory.ConcreteCategory.Elementwise
 /-!
 # The category of R-modules has all colimits.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file uses a "pre-automated" approach, just as for `Mon/colimits.lean`.
 
 Note that finite colimits can already be obtained from the instance `abelian (Module R)`.

Mathbin/Algebra/Category/Module/Monoidal/Closed.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Buzzard, Scott Morrison, Jakob von Raumer
 
 ! This file was ported from Lean 3 source module algebra.category.Module.monoidal.closed
-! leanprover-community/mathlib commit 74403a3b2551b0970855e14ef5e8fd0d6af1bfc2
+! leanprover-community/mathlib commit c20927220ef87bb4962ba08bf6da2ce3cf50a6dd
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,6 +13,9 @@ import Mathbin.Algebra.Category.Module.Monoidal.Symmetric
 
 /-!
 # The monoidal closed structure on `Module R`.
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 

Mathbin/Algebra/Homology/LocalCohomology.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Emily Witt, Scott Morrison, Jake Levinson, Sam van Gool
 
 ! This file was ported from Lean 3 source module algebra.homology.local_cohomology
-! leanprover-community/mathlib commit 5a684ce82399d820475609907c6ef8dba5b1b97c
+! leanprover-community/mathlib commit c20927220ef87bb4962ba08bf6da2ce3cf50a6dd
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -17,6 +17,9 @@ import Mathbin.RingTheory.Finiteness
 /-!
 # Local cohomology.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 This file defines the `i`-th local cohomology module of an `R`-module `M` with support in an
 ideal `I` of `R`, where `R` is a commutative ring, as the direct limit of Ext modules:
 

Mathbin/Algebra/Lie/Nilpotent.lean

@@ -4,14 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 
 ! This file was ported from Lean 3 source module algebra.lie.nilpotent
-! leanprover-community/mathlib commit 938fead7abdc0cbbca8eba7a1052865a169dc102
+! leanprover-community/mathlib commit 6b0169218d01f2837d79ea2784882009a0da1aa1
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathbin.Algebra.Lie.Solvable
 import Mathbin.Algebra.Lie.Quotient
 import Mathbin.Algebra.Lie.Normalizer
-import Mathbin.LinearAlgebra.Eigenspace
+import Mathbin.LinearAlgebra.Eigenspace.Basic
 import Mathbin.RingTheory.Nilpotent
 
 /-!

Mathbin/Algebra/Lie/Weights.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 
 ! This file was ported from Lean 3 source module algebra.lie.weights
-! leanprover-community/mathlib commit 938fead7abdc0cbbca8eba7a1052865a169dc102
+! leanprover-community/mathlib commit 6b0169218d01f2837d79ea2784882009a0da1aa1
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -13,7 +13,7 @@ import Mathbin.Algebra.Lie.TensorProduct
 import Mathbin.Algebra.Lie.Character
 import Mathbin.Algebra.Lie.Engel
 import Mathbin.Algebra.Lie.CartanSubalgebra
-import Mathbin.LinearAlgebra.Eigenspace
+import Mathbin.LinearAlgebra.Eigenspace.Basic
 import Mathbin.RingTheory.TensorProduct
 
 /-!

Mathbin/Algebra/Star/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 
 ! This file was ported from Lean 3 source module algebra.star.basic
-! leanprover-community/mathlib commit dc7ac07acd84584426773e69e51035bea9a770e7
+! leanprover-community/mathlib commit 31c24aa72e7b3e5ed97a8412470e904f82b81004
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -27,23 +27,12 @@ These are implemented as "mixin" typeclasses, so to summon a star ring (for exam
 one needs to write `(R : Type) [ring R] [star_ring R]`.
 This avoids difficulties with diamond inheritance.
 
-We also define the class `star_ordered_ring R`, which says that the order on `R` respects the
-star operation, i.e. an element `r` is nonnegative iff there exists an `s` such that
-`r = star s * s`.
-
 For now we simply do not introduce notations,
 as different users are expected to feel strongly about the relative merits of
 `r^*`, `r†`, `rᘁ`, and so on.
 
 Our star rings are actually star semirings, but of course we can prove
 `star_neg : star (-r) = - star r` when the underlying semiring is a ring.
-
-## TODO
-
-* In a Banach star algebra without a well-defined square root, the natural ordering is given by the
-positive cone which is the closure of the sums of elements `star r * r`. A weaker version of
-`star_ordered_ring` could be defined for this case. Note that the current definition has the
-advantage of not requiring a topology.
 -/
 
 
@@ -503,67 +492,6 @@ def starRingOfComm {R : Type _} [CommSemiring R] : StarRing R :=
 #align star_ring_of_comm starRingOfComm
 -/
 
-#print StarOrderedRing /-
-/-- An ordered `*`-ring is a ring which is both an `ordered_add_comm_group` and a `*`-ring,
-and `0 ≤ r ↔ ∃ s, r = star s * s`.
--/
-class StarOrderedRing (R : Type u) [NonUnitalSemiring R] [PartialOrder R] extends StarRing R where
-  add_le_add_left : ∀ a b : R, a ≤ b → ∀ c : R, c + a ≤ c + b
-  nonneg_iff : ∀ r : R, 0 ≤ r ↔ ∃ s, r = star s * s
-#align star_ordered_ring StarOrderedRing
--/
-
-namespace StarOrderedRing
-
--- see note [lower instance priority]
-instance (priority := 100) [NonUnitalRing R] [PartialOrder R] [StarOrderedRing R] :
-    OrderedAddCommGroup R :=
-  { show NonUnitalRing R by infer_instance, show PartialOrder R by infer_instance,
-    show StarOrderedRing R by infer_instance with }
-
-end StarOrderedRing
-
-section NonUnitalSemiring
-
-variable [NonUnitalSemiring R] [PartialOrder R] [StarOrderedRing R]
-
-theorem star_mul_self_nonneg {r : R} : 0 ≤ star r * r :=
-  (StarOrderedRing.nonneg_iff _).mpr ⟨r, rfl⟩
-#align star_mul_self_nonneg star_mul_self_nonneg
-
-theorem star_mul_self_nonneg' {r : R} : 0 ≤ r * star r := by nth_rw_rhs 1 [← star_star r];
-  exact star_mul_self_nonneg
-#align star_mul_self_nonneg' star_mul_self_nonneg'
-
-theorem conjugate_nonneg {a : R} (ha : 0 ≤ a) (c : R) : 0 ≤ star c * a * c :=
-  by
-  obtain ⟨x, rfl⟩ := (StarOrderedRing.nonneg_iff _).1 ha
-  exact (StarOrderedRing.nonneg_iff _).2 ⟨x * c, by rw [star_mul, ← mul_assoc, mul_assoc _ _ c]⟩
-#align conjugate_nonneg conjugate_nonneg
-
-theorem conjugate_nonneg' {a : R} (ha : 0 ≤ a) (c : R) : 0 ≤ c * a * star c := by
-  simpa only [star_star] using conjugate_nonneg ha (star c)
-#align conjugate_nonneg' conjugate_nonneg'
-
-end NonUnitalSemiring
-
-section NonUnitalRing
-
-variable [NonUnitalRing R] [PartialOrder R] [StarOrderedRing R]
-
-theorem conjugate_le_conjugate {a b : R} (hab : a ≤ b) (c : R) : star c * a * c ≤ star c * b * c :=
-  by
-  rw [← sub_nonneg] at hab ⊢
-  convert conjugate_nonneg hab c
-  simp only [mul_sub, sub_mul]
-#align conjugate_le_conjugate conjugate_le_conjugate
-
-theorem conjugate_le_conjugate' {a b : R} (hab : a ≤ b) (c : R) : c * a * star c ≤ c * b * star c :=
-  by simpa only [star_star] using conjugate_le_conjugate hab (star c)
-#align conjugate_le_conjugate' conjugate_le_conjugate'
-
-end NonUnitalRing
-
 #print StarModule /-
 /-- A star module `A` over a star ring `R` is a module which is a star add monoid,
 and the two star structures are compatible in the sense

Mathbin/Algebra/Star/Chsh.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 
 ! This file was ported from Lean 3 source module algebra.star.chsh
-! leanprover-community/mathlib commit 31ca6f9cf5f90a6206092cd7f84b359dcb6d52e0
+! leanprover-community/mathlib commit 31c24aa72e7b3e5ed97a8412470e904f82b81004
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -151,7 +151,7 @@ theorem CHSH_inequality_of_comm [OrderedCommRing R] [StarOrderedRing R] [Algebra
       skip
       congr
       rw [← sa]
-    convert smul_le_smul_of_nonneg (star_mul_self_nonneg : 0 ≤ star P * P) _
+    convert smul_le_smul_of_nonneg (star_mul_self_nonneg P) _
     · simp
     · infer_instance
     · norm_num
@@ -245,15 +245,15 @@ theorem tsirelson_inequality [OrderedRing R] [StarOrderedRing R] [Algebra ℝ R]
         skip
         congr
         rw [← P_sa]
-      convert (star_mul_self_nonneg : 0 ≤ star P * P)
+      convert star_mul_self_nonneg P
     have Q2_nonneg : 0 ≤ Q ^ 2 := by
       rw [sq]
       conv =>
         congr
         skip
         congr
         rw [← Q_sa]
-      convert (star_mul_self_nonneg : 0 ≤ star Q * Q)
+      convert star_mul_self_nonneg Q
     convert
       smul_le_smul_of_nonneg (add_nonneg P2_nonneg Q2_nonneg) (le_of_lt (show 0 < √2⁻¹ by norm_num))
     -- `norm_num` can't directly show `0 ≤ √2⁻¹`