bump to nightly-2023-06-07-03

mathlib commit leanprover-community/mathlib@58a2722

Mathbin/Algebra/Algebra/Spectrum.lean

@@ -4,13 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jireh Loreaux
 
 ! This file was ported from Lean 3 source module algebra.algebra.spectrum
-! leanprover-community/mathlib commit 11dcb6b59dc9cc74e053b7ca8569bf6df4ac0f1e
+! leanprover-community/mathlib commit 58a272265b5e05f258161260dd2c5d247213cbd3
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
 import Mathbin.Algebra.Star.Pointwise
 import Mathbin.Algebra.Star.Subalgebra
-import Mathbin.FieldTheory.IsAlgClosed.Basic
 import Mathbin.Tactic.NoncommRing
 
 /-!
@@ -36,8 +35,6 @@ This theory will serve as the foundation for spectral theory in Banach algebras.
   units (of `R`) in `σ (a*b)` coincide with those in `σ (b*a)`.
 * `spectrum.scalar_eq`: in a nontrivial algebra over a field, the spectrum of a scalar is
   a singleton.
-* `spectrum.subset_polynomial_aeval`, `spectrum.map_polynomial_aeval_of_degree_pos`,
-  `spectrum.map_polynomial_aeval_of_nonempty`: variations on the spectral mapping theorem.
 
 ## Notations
 
@@ -100,8 +97,6 @@ end Defs
 
 namespace spectrum
 
-open scoped Polynomial
-
 section ScalarSemiring
 
 variable {R : Type u} {A : Type v}
@@ -224,8 +219,6 @@ theorem smul_mem_smul_iff {a : A} {s : R} {r : Rˣ} : r • s ∈ σ (r • a) 
     isUnit_smul_iff]
 #align spectrum.smul_mem_smul_iff spectrum.smul_mem_smul_iff
 
-open scoped Polynomial
-
 theorem unit_smul_eq_smul (a : A) (r : Rˣ) : σ (r • a) = r • σ a :=
   by
   ext
@@ -333,20 +326,6 @@ theorem sub_singleton_eq (a : A) (r : R) : σ a - {r} = σ (a - ↑ₐ r) := by
   simpa only [neg_sub, neg_eq] using congr_arg Neg.neg (singleton_sub_eq a r)
 #align spectrum.sub_singleton_eq spectrum.sub_singleton_eq
 
-open Polynomial
-
-theorem exists_mem_of_not_isUnit_aeval_prod [IsDomain R] {p : R[X]} {a : A} (hp : p ≠ 0)
-    (h : ¬IsUnit (aeval a (Multiset.map (fun x : R => X - C x) p.roots).Prod)) :
-    ∃ k : R, k ∈ σ a ∧ eval k p = 0 :=
-  by
-  rw [← Multiset.prod_toList, AlgHom.map_list_prod] at h 
-  replace h := mt List.prod_isUnit h
-  simp only [not_forall, exists_prop, aeval_C, Multiset.mem_toList, List.mem_map, aeval_X,
-    exists_exists_and_eq_and, Multiset.mem_map, AlgHom.map_sub] at h 
-  rcases h with ⟨r, r_mem, r_nu⟩
-  exact ⟨r, by rwa [mem_iff, ← IsUnit.sub_iff], by rwa [← is_root.def, ← mem_roots hp]⟩
-#align spectrum.exists_mem_of_not_is_unit_aeval_prod spectrum.exists_mem_of_not_isUnit_aeval_prod
-
 end ScalarRing
 
 section ScalarField
@@ -416,97 +395,6 @@ protected theorem map_inv (a : Aˣ) : (σ (a : A))⁻¹ = σ (↑a⁻¹ : A) :=
     simpa only [Units.val_inv_eq_inv_val] using inv_mem_iff.mp hk
 #align spectrum.map_inv spectrum.map_inv
 
-open Polynomial
-
-/-- Half of the spectral mapping theorem for polynomials. We prove it separately
-because it holds over any field, whereas `spectrum.map_polynomial_aeval_of_degree_pos` and
-`spectrum.map_polynomial_aeval_of_nonempty` need the field to be algebraically closed. -/
-theorem subset_polynomial_aeval (a : A) (p : 𝕜[X]) : (fun k => eval k p) '' σ a ⊆ σ (aeval a p) :=
-  by
-  rintro _ ⟨k, hk, rfl⟩
-  let q := C (eval k p) - p
-  have hroot : is_root q k := by simp only [eval_C, eval_sub, sub_self, is_root.def]
-  rw [← mul_div_eq_iff_is_root, ← neg_mul_neg, neg_sub] at hroot 
-  have aeval_q_eq : ↑ₐ (eval k p) - aeval a p = aeval a q := by
-    simp only [aeval_C, AlgHom.map_sub, sub_left_inj]
-  rw [mem_iff, aeval_q_eq, ← hroot, aeval_mul]
-  have hcomm := (Commute.all (C k - X) (-(q / (X - C k)))).map (aeval a)
-  apply mt fun h => (hcomm.is_unit_mul_iff.mp h).1
-  simpa only [aeval_X, aeval_C, AlgHom.map_sub] using hk
-#align spectrum.subset_polynomial_aeval spectrum.subset_polynomial_aeval
-
-/-- The *spectral mapping theorem* for polynomials.  Note: the assumption `degree p > 0`
-is necessary in case `σ a = ∅`, for then the left-hand side is `∅` and the right-hand side,
-assuming `[nontrivial A]`, is `{k}` where `p = polynomial.C k`. -/
-theorem map_polynomial_aeval_of_degree_pos [IsAlgClosed 𝕜] (a : A) (p : 𝕜[X])
-    (hdeg : 0 < degree p) : σ (aeval a p) = (fun k => eval k p) '' σ a :=
-  by
-  -- handle the easy direction via `spectrum.subset_polynomial_aeval`
-  refine' Set.eq_of_subset_of_subset (fun k hk => _) (subset_polynomial_aeval a p)
-  -- write `C k - p` product of linear factors and a constant; show `C k - p ≠ 0`.
-  have hprod := eq_prod_roots_of_splits_id (IsAlgClosed.splits (C k - p))
-  have h_ne : C k - p ≠ 0 :=
-    ne_zero_of_degree_gt
-      (by rwa [degree_sub_eq_right_of_degree_lt (lt_of_le_of_lt degree_C_le hdeg)])
-  have lead_ne := leading_coeff_ne_zero.mpr h_ne
-  have lead_unit := (Units.map ↑ₐ.toMonoidHom (Units.mk0 _ lead_ne)).IsUnit
-  /- leading coefficient is a unit so product of linear factors is not a unit;
-    apply `exists_mem_of_not_is_unit_aeval_prod`. -/
-  have p_a_eq : aeval a (C k - p) = ↑ₐ k - aeval a p := by
-    simp only [aeval_C, AlgHom.map_sub, sub_left_inj]
-  rw [mem_iff, ← p_a_eq, hprod, aeval_mul, ((Commute.all _ _).map (aeval a)).isUnit_mul_iff,
-    aeval_C] at hk 
-  replace hk := exists_mem_of_not_is_unit_aeval_prod h_ne (not_and.mp hk lead_unit)
-  rcases hk with ⟨r, r_mem, r_ev⟩
-  exact ⟨r, r_mem, symm (by simpa [eval_sub, eval_C, sub_eq_zero] using r_ev)⟩
-#align spectrum.map_polynomial_aeval_of_degree_pos spectrum.map_polynomial_aeval_of_degree_pos
-
-/-- In this version of the spectral mapping theorem, we assume the spectrum
-is nonempty instead of assuming the degree of the polynomial is positive. -/
-theorem map_polynomial_aeval_of_nonempty [IsAlgClosed 𝕜] (a : A) (p : 𝕜[X])
-    (hnon : (σ a).Nonempty) : σ (aeval a p) = (fun k => eval k p) '' σ a :=
-  by
-  nontriviality A
-  refine' Or.elim (le_or_gt (degree p) 0) (fun h => _) (map_polynomial_aeval_of_degree_pos a p)
-  · rw [eq_C_of_degree_le_zero h]
-    simp only [Set.image_congr, eval_C, aeval_C, scalar_eq, Set.Nonempty.image_const hnon]
-#align spectrum.map_polynomial_aeval_of_nonempty spectrum.map_polynomial_aeval_of_nonempty
-
-/-- A specialization of `spectrum.subset_polynomial_aeval` to monic monomials for convenience. -/
-theorem pow_image_subset (a : A) (n : ℕ) : (fun x => x ^ n) '' σ a ⊆ σ (a ^ n) := by
-  simpa only [eval_pow, eval_X, aeval_X_pow] using subset_polynomial_aeval a (X ^ n : 𝕜[X])
-#align spectrum.pow_image_subset spectrum.pow_image_subset
-
-/-- A specialization of `spectrum.map_polynomial_aeval_of_nonempty` to monic monomials for
-convenience. -/
-theorem map_pow_of_pos [IsAlgClosed 𝕜] (a : A) {n : ℕ} (hn : 0 < n) :
-    σ (a ^ n) = (fun x => x ^ n) '' σ a := by
-  simpa only [aeval_X_pow, eval_pow, eval_X] using
-    map_polynomial_aeval_of_degree_pos a (X ^ n : 𝕜[X]) (by rw_mod_cast [degree_X_pow]; exact hn)
-#align spectrum.map_pow_of_pos spectrum.map_pow_of_pos
-
-/-- A specialization of `spectrum.map_polynomial_aeval_of_nonempty` to monic monomials for
-convenience. -/
-theorem map_pow_of_nonempty [IsAlgClosed 𝕜] {a : A} (ha : (σ a).Nonempty) (n : ℕ) :
-    σ (a ^ n) = (fun x => x ^ n) '' σ a := by
-  simpa only [aeval_X_pow, eval_pow, eval_X] using map_polynomial_aeval_of_nonempty a (X ^ n) ha
-#align spectrum.map_pow_of_nonempty spectrum.map_pow_of_nonempty
-
-variable (𝕜)
-
--- We will use this both to show eigenvalues exist, and to prove Schur's lemma.
-/-- Every element `a` in a nontrivial finite-dimensional algebra `A`
-over an algebraically closed field `𝕜` has non-empty spectrum. -/
-theorem nonempty_of_isAlgClosed_of_finiteDimensional [IsAlgClosed 𝕜] [Nontrivial A]
-    [I : FiniteDimensional 𝕜 A] (a : A) : ∃ k : 𝕜, k ∈ σ a :=
-  by
-  obtain ⟨p, ⟨h_mon, h_eval_p⟩⟩ := isIntegral_of_noetherian (IsNoetherian.iff_fg.2 I) a
-  have nu : ¬IsUnit (aeval a p) := by rw [← aeval_def] at h_eval_p ; rw [h_eval_p]; simp
-  rw [eq_prod_roots_of_monic_of_splits_id h_mon (IsAlgClosed.splits p)] at nu 
-  obtain ⟨k, hk, _⟩ := exists_mem_of_not_is_unit_aeval_prod (monic.ne_zero h_mon) nu
-  exact ⟨k, hk⟩
-#align spectrum.nonempty_of_is_alg_closed_of_finite_dimensional spectrum.nonempty_of_isAlgClosed_of_finiteDimensional
-
 end ScalarField
 
 end spectrum
@@ -515,7 +403,7 @@ namespace AlgHom
 
 section CommSemiring
 
-variable {F R A B : Type _} [CommRing R] [Ring A] [Algebra R A] [Ring B] [Algebra R B]
+variable {F R A B : Type _} [CommSemiring R] [Ring A] [Algebra R A] [Ring B] [Algebra R B]
 
 variable [AlgHomClass F R A B]
 

Mathbin/Algebra/Category/Module/Monoidal/Symmetric.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.symmetric
-! leanprover-community/mathlib commit 74403a3b2551b0970855e14ef5e8fd0d6af1bfc2
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! 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.Basic
 
 /-!
 # The symmetric monoidal structure on `Module R`.
+
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
 -/
 
 

Mathbin/Algebra/Lie/BaseChange.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.base_change
-! leanprover-community/mathlib commit 9264b15ee696b7ca83f13c8ad67c83d6eb70b730
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.Algebra.Lie.TensorProduct
 /-!
 # Extension and restriction of scalars for Lie algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Lie algebras have a well-behaved theory of extension and restriction of scalars.
 
 ## Main definitions

Mathbin/Algebra/Lie/Character.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.character
-! leanprover-community/mathlib commit 132328c4dd48da87adca5d408ca54f315282b719
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.LinearAlgebra.Dual
 /-!
 # Characters of Lie algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A character of a Lie algebra `L` over a commutative ring `R` is a morphism of Lie algebras `L → R`,
 where `R` is regarded as a Lie algebra over itself via the ring commutator. For an Abelian Lie
 algebra (e.g., a Cartan subalgebra of a semisimple Lie algebra) a character is just a linear form.

Mathbin/Algebra/Lie/DirectSum.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.direct_sum
-! leanprover-community/mathlib commit c0cc689babd41c0e9d5f02429211ffbe2403472a
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -16,6 +16,9 @@ import Mathbin.Algebra.Lie.Basic
 /-!
 # Direct sums of Lie algebras and Lie modules
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Direct sums of Lie algebras and Lie modules carry natural algebra and module structures.
 
 ## Tags

Mathbin/Algebra/Lie/Semisimple.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.semisimple
-! leanprover-community/mathlib commit 356447fe00e75e54777321045cdff7c9ea212e60
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! 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.Lie.Solvable
 /-!
 # Semisimple Lie algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 The famous Cartan-Dynkin-Killing classification of semisimple Lie algebras renders them one of the
 most important classes of Lie algebras. In this file we define simple and semisimple Lie algebras
 and prove some basic related results.

Mathbin/Algebra/Lie/SkewAdjoint.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.skew_adjoint
-! leanprover-community/mathlib commit 075b3f7d19b9da85a0b54b3e33055a74fc388dec
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.LinearAlgebra.Matrix.BilinearForm
 /-!
 # Lie algebras of skew-adjoint endomorphisms of a bilinear form
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 When a module carries a bilinear form, the Lie algebra of endomorphisms of the module contains a
 distinguished Lie subalgebra: the skew-adjoint endomorphisms. Such subalgebras are important
 because they provide a simple, explicit construction of the so-called classical Lie algebras.

Mathbin/Algebra/Lie/Solvable.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.solvable
-! leanprover-community/mathlib commit a50170a88a47570ed186b809ca754110590f9476
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.Order.Hom.Basic
 /-!
 # Solvable Lie algebras
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Like groups, Lie algebras admit a natural concept of solvability. We define this here via the
 derived series and prove some related results. We also define the radical of a Lie algebra and
 prove that it is solvable when the Lie algebra is Noetherian.

Mathbin/Algebra/Module/DedekindDomain.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Pierre-Alexandre Bazin
 
 ! This file was ported from Lean 3 source module algebra.module.dedekind_domain
-! leanprover-community/mathlib commit cdc34484a07418af43daf8198beaf5c00324bca8
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.RingTheory.DedekindDomain.Ideal
 /-!
 # Modules over a Dedekind domain
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 Over a Dedekind domain, a `I`-torsion module is the internal direct sum of its `p i ^ e i`-torsion
 submodules, where `I = ∏ i, p i ^ e i` is its unique decomposition in prime ideals.
 Therefore, as any finitely generated torsion module is `I`-torsion for some `I`, it is an internal

Mathbin/Algebra/Symmetrized.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Christopher Hoskin
 
 ! This file was ported from Lean 3 source module algebra.symmetrized
-! leanprover-community/mathlib commit 933547832736be61a5de6576e22db351c6c2fbfd
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.Algebra.Module.Basic
 /-!
 # Symmetrized algebra
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A commutative multiplication on a real or complex space can be constructed from any multiplication
 by "symmetrization" i.e
 $$

Mathbin/All.lean

@@ -1807,6 +1807,7 @@ import Mathbin.FieldTheory.IntermediateField
 import Mathbin.FieldTheory.IsAlgClosed.AlgebraicClosure
 import Mathbin.FieldTheory.IsAlgClosed.Basic
 import Mathbin.FieldTheory.IsAlgClosed.Classification
+import Mathbin.FieldTheory.IsAlgClosed.Spectrum
 import Mathbin.FieldTheory.KrullTopology
 import Mathbin.FieldTheory.Laurent
 import Mathbin.FieldTheory.Minpoly.Basic

Mathbin/Analysis/BoxIntegral/Partition/Measure.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 
 ! This file was ported from Lean 3 source module analysis.box_integral.partition.measure
-! leanprover-community/mathlib commit fd5edc43dc4f10b85abfe544b88f82cf13c5f844
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -14,6 +14,9 @@ import Mathbin.MeasureTheory.Measure.Lebesgue.Basic
 /-!
 # Box-additive functions defined by measures
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 In this file we prove a few simple facts about rectangular boxes, partitions, and measures:
 
 - given a box `I : box ι`, its coercion to `set (ι → ℝ)` and `I.Icc` are measurable sets;

Mathbin/Analysis/Calculus/FderivAnalytic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 
 ! This file was ported from Lean 3 source module analysis.calculus.fderiv_analytic
-! leanprover-community/mathlib commit 3bce8d800a6f2b8f63fe1e588fd76a9ff4adcebe
+! leanprover-community/mathlib commit 36938f775671ff28bea1c0310f1608e4afbb22e0
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -15,6 +15,9 @@ import Mathbin.Analysis.Calculus.ContDiffDef
 /-!
 # Frechet derivatives of analytic functions.
 
+> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
+> Any changes to this file require a corresponding PR to mathlib4.
+
 A function expressible as a power series at a point has a Frechet derivative there.
 Also the special case in terms of `deriv` when the domain is 1-dimensional.
 -/