Merge branch 'master' into acmepjz_alg_indep_3

Mathlib.lean

@@ -1006,6 +1006,7 @@ import Mathlib.Analysis.BoxIntegral.Partition.Measure
 import Mathlib.Analysis.BoxIntegral.Partition.Split
 import Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction
 import Mathlib.Analysis.BoxIntegral.Partition.Tagged
+import Mathlib.Analysis.CStarAlgebra.ApproximateUnit
 import Mathlib.Analysis.CStarAlgebra.Basic
 import Mathlib.Analysis.CStarAlgebra.Classes
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
@@ -2261,6 +2262,7 @@ import Mathlib.Data.Fin.Tuple.Finset
 import Mathlib.Data.Fin.Tuple.NatAntidiagonal
 import Mathlib.Data.Fin.Tuple.Reflection
 import Mathlib.Data.Fin.Tuple.Sort
+import Mathlib.Data.Fin.Tuple.Take
 import Mathlib.Data.Fin.VecNotation
 import Mathlib.Data.FinEnum
 import Mathlib.Data.Finite.Card
@@ -2791,6 +2793,7 @@ import Mathlib.Dynamics.TopologicalEntropy.Semiconj
 import Mathlib.FieldTheory.AbelRuffini
 import Mathlib.FieldTheory.AbsoluteGaloisGroup
 import Mathlib.FieldTheory.Adjoin
+import Mathlib.FieldTheory.AlgebraicClosure
 import Mathlib.FieldTheory.AxGrothendieck
 import Mathlib.FieldTheory.Cardinality
 import Mathlib.FieldTheory.ChevalleyWarning
@@ -4088,8 +4091,11 @@ import Mathlib.RingTheory.Ideal.Over
 import Mathlib.RingTheory.Ideal.Pointwise
 import Mathlib.RingTheory.Ideal.Prime
 import Mathlib.RingTheory.Ideal.Prod
-import Mathlib.RingTheory.Ideal.Quotient
-import Mathlib.RingTheory.Ideal.QuotientOperations
+import Mathlib.RingTheory.Ideal.Quotient.Basic
+import Mathlib.RingTheory.Ideal.Quotient.Defs
+import Mathlib.RingTheory.Ideal.Quotient.Nilpotent
+import Mathlib.RingTheory.Ideal.Quotient.Noetherian
+import Mathlib.RingTheory.Ideal.Quotient.Operations
 import Mathlib.RingTheory.Ideal.Span
 import Mathlib.RingTheory.Idempotents
 import Mathlib.RingTheory.Int.Basic
@@ -4224,8 +4230,6 @@ import Mathlib.RingTheory.Prime
 import Mathlib.RingTheory.PrimeSpectrum
 import Mathlib.RingTheory.PrincipalIdealDomain
 import Mathlib.RingTheory.QuotSMulTop
-import Mathlib.RingTheory.QuotientNilpotent
-import Mathlib.RingTheory.QuotientNoetherian
 import Mathlib.RingTheory.Radical
 import Mathlib.RingTheory.ReesAlgebra
 import Mathlib.RingTheory.Regular.IsSMulRegular
@@ -4618,6 +4622,7 @@ import Mathlib.Topology.Algebra.Affine
 import Mathlib.Topology.Algebra.Algebra
 import Mathlib.Topology.Algebra.Algebra.Rat
 import Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
+import Mathlib.Topology.Algebra.ClopenNhdofOne
 import Mathlib.Topology.Algebra.ClosedSubgroup
 import Mathlib.Topology.Algebra.ConstMulAction
 import Mathlib.Topology.Algebra.Constructions

Mathlib/Algebra/CharP/MixedCharZero.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jon Eugster
 -/
 import Mathlib.Algebra.CharP.LocalRing
-import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.RingTheory.Ideal.Quotient.Basic
 import Mathlib.Tactic.FieldSimp
 
 /-!

Mathlib/Algebra/CharP/Quotient.lean

@@ -5,7 +5,7 @@ Authors: Kenny Lau, Eric Wieser
 -/
 import Mathlib.GroupTheory.OrderOfElement
 import Mathlib.RingTheory.Ideal.Maps
-import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.RingTheory.Ideal.Quotient.Defs
 
 /-!
 # Characteristic of quotients rings

Mathlib/Algebra/DirectLimit.lean

@@ -8,7 +8,7 @@ import Mathlib.Data.Finset.Order
 import Mathlib.LinearAlgebra.Quotient.Basic
 import Mathlib.RingTheory.FreeCommRing
 import Mathlib.RingTheory.Ideal.Maps
-import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.RingTheory.Ideal.Quotient.Defs
 import Mathlib.Tactic.SuppressCompilation
 
 /-!

Mathlib/Algebra/Module/Equiv/Defs.lean

@@ -391,6 +391,18 @@ theorem toLinearMap_symm_comp_eq (f : M₃ →ₛₗ[σ₃₁] M₁) (g : M₃ 
   · simp [← H, ← e₁₂.toEquiv.symm_comp_eq f g]
   · simp [H, e₁₂.toEquiv.symm_comp_eq f g]
 
+@[simp]
+theorem comp_toLinearMap_eq_iff (f g : M₃ →ₛₗ[σ₃₁] M₁) :
+    e₁₂.toLinearMap.comp f = e₁₂.toLinearMap.comp g ↔ f = g := by
+  refine ⟨fun h => ?_, congrArg e₁₂.comp⟩
+  rw [← (toLinearMap_symm_comp_eq g (e₁₂.toLinearMap.comp f)).mpr h, eq_toLinearMap_symm_comp]
+
+@[simp]
+theorem eq_comp_toLinearMap_iff (f g : M₂ →ₛₗ[σ₂₃] M₃) :
+    f.comp e₁₂.toLinearMap = g.comp e₁₂.toLinearMap ↔ f = g := by
+  refine ⟨fun h => ?_, fun a ↦ congrFun (congrArg LinearMap.comp a) e₁₂.toLinearMap⟩
+  rw [(eq_comp_toLinearMap_symm g (f.comp e₁₂.toLinearMap)).mpr h.symm, eq_comp_toLinearMap_symm]
+
 @[simp]
 theorem refl_symm [Module R M] : (refl R M).symm = LinearEquiv.refl R M :=
   rfl

Mathlib/Algebra/Polynomial/AlgebraMap.lean

@@ -568,6 +568,16 @@ lemma comp_X_add_C_eq_zero_iff : p.comp (X + C t) = 0 ↔ p = 0 :=
 
 lemma comp_X_add_C_ne_zero_iff : p.comp (X + C t) ≠ 0 ↔ p ≠ 0 := comp_X_add_C_eq_zero_iff.not
 
+lemma dvd_comp_X_sub_C_iff (p q : R[X]) (a : R) :
+    p ∣ q.comp (X - C a) ↔ p.comp (X + C a) ∣ q := by
+  convert (map_dvd_iff <| algEquivAevalXAddC a).symm using 2
+  rw [C_eq_algebraMap, algEquivAevalXAddC_apply, ← comp_eq_aeval]
+  simp [comp_assoc]
+
+lemma dvd_comp_X_add_C_iff (p q : R[X]) (a : R) :
+    p ∣ q.comp (X + C a) ↔ p.comp (X - C a) ∣ q := by
+  simpa using dvd_comp_X_sub_C_iff p q (-a)
+
 variable [IsDomain R]
 
 lemma units_coeff_zero_smul (c : R[X]ˣ) (p : R[X]) : (c : R[X]).coeff 0 • p = c * p := by

Mathlib/Algebra/Polynomial/Splits.lean

@@ -139,6 +139,27 @@ theorem splits_X_pow (n : ℕ) : (X ^ n).Splits i :=
 theorem splits_id_iff_splits {f : K[X]} : (f.map i).Splits (RingHom.id L) ↔ f.Splits i := by
   rw [splits_map_iff, RingHom.id_comp]
 
+theorem Splits.comp_X_sub_C {i : L →+* F} (a : L) {f : L[X]}
+    (h : f.Splits i) : (f.comp (X - C a)).Splits i := by
+  cases h with
+  | inl h0 =>
+    left
+    simp only [map_eq_zero] at h0 ⊢
+    exact h0.symm ▸ zero_comp
+  | inr h =>
+    right
+    intro g irr dvd
+    rw [map_comp, Polynomial.map_sub, map_X, map_C, dvd_comp_X_sub_C_iff] at dvd
+    have := h (irr.map (algEquivAevalXAddC _)) dvd
+    rw [degree_eq_natDegree irr.ne_zero]
+    rwa [algEquivAevalXAddC_apply, ← comp_eq_aeval,
+      degree_eq_natDegree (fun h => WithBot.bot_ne_one (h ▸ this)),
+      natDegree_comp, natDegree_X_add_C, mul_one] at this
+
+theorem Splits.comp_X_add_C {i : L →+* F} (a : L) {f : L[X]}
+    (h : f.Splits i) : (f.comp (X + C a)).Splits i := by
+  simpa only [map_neg, sub_neg_eq_add] using h.comp_X_sub_C (-a)
+
 theorem exists_root_of_splits' {f : K[X]} (hs : Splits i f) (hf0 : degree (f.map i) ≠ 0) :
     ∃ x, eval₂ i x f = 0 :=
   letI := Classical.decEq L

Mathlib/Algebra/RingQuot.lean

@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 import Mathlib.Algebra.Algebra.Hom
-import Mathlib.RingTheory.Ideal.Quotient
+import Mathlib.RingTheory.Congruence.Basic
+import Mathlib.RingTheory.Ideal.Quotient.Defs
+import Mathlib.RingTheory.Ideal.Span
 
 /-!
 # Quotients of non-commutative rings

Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean

@@ -808,7 +808,6 @@ lemma baseChange_polynomial : (W.baseChange B).toAffine.polynomial =
     (W.baseChange A).toAffine.polynomial.map (mapRingHom f) := by
   rw [← map_polynomial, map_baseChange]
 
-variable {g} in
 lemma baseChange_equation (hf : Function.Injective f) (x y : A) :
     (W.baseChange B).toAffine.Equation (f x) (f y) ↔ (W.baseChange A).toAffine.Equation x y := by
   erw [← map_equation _ hf, map_baseChange]

Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean

@@ -61,7 +61,7 @@ structure VariableChange (R : Type u) [CommRing R] where
 
 namespace VariableChange
 
-variable (C C' C'' : VariableChange R)
+variable (C C' : VariableChange R)
 
 /-- The identity linear change of variables given by the identity matrix. -/
 def id : VariableChange R :=

Mathlib/Analysis/Analytic/Basic.lean

@@ -1244,7 +1244,7 @@ protected theorem HasFPowerSeriesOnBall.continuousOn (hf : HasFPowerSeriesOnBall
 protected theorem HasFPowerSeriesWithinOnBall.continuousWithinAt_insert
     (hf : HasFPowerSeriesWithinOnBall f p s x r) :
     ContinuousWithinAt f (insert x s) x := by
-  apply (hf.continuousOn.continuousWithinAt (x := x) (by simp [hf.r_pos])).mono_of_mem
+  apply (hf.continuousOn.continuousWithinAt (x := x) (by simp [hf.r_pos])).mono_of_mem_nhdsWithin
   exact inter_mem_nhdsWithin _ (EMetric.ball_mem_nhds x hf.r_pos)
 
 protected theorem HasFPowerSeriesWithinOnBall.continuousWithinAt

Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean

@@ -0,0 +1,107 @@
+/-
+Copyright (c) 2024 Jireh Loreaux. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jireh Loreaux
+-/
+import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
+import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
+import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow
+
+/-! # Positive contractions in a C⋆-algebra form an approximate unit
+
+This file will show (although it does not yet) that the collection of positive contractions (of norm
+strictly less than one) in a possibly non-unital C⋆-algebra form an approximate unit. The key step
+is to show that this set is directed using the continuous functional calculus applied with the
+functions `fun x : ℝ≥0, 1 - (1 + x)⁻¹` and `fun x : ℝ≥0, x * (1 - x)⁻¹`, which are inverses on
+the interval `{x : ℝ≥0 | x < 1}`.
+
+## Main declarations
+
++ `CFC.monotoneOn_one_sub_one_add_inv`: the function `f := fun x : ℝ≥0, 1 - (1 + x)⁻¹` is
+  *operator monotone* on `Set.Ici (0 : A)` (i.e., `cfcₙ f` is monotone on `{x : A | 0 ≤ x}`).
++ `Set.InvOn.one_sub_one_add_inv`: the functions `f := fun x : ℝ≥0, 1 - (1 + x)⁻¹` and
+  `g := fun x : ℝ≥0, x * (1 - x)⁻¹` are inverses on `{x : ℝ≥0 | x < 1}`.
++ `CStarAlgebra.directedOn_nonneg_ball`: the set `{x : A | 0 ≤ x} ∩ Metric.ball 0 1` is directed.
+
+## TODO
+
++ Prove the approximate identity result by following Ken Davidson's proof in
+  "C*-Algebras by Example"
+
+-/
+
+variable {A : Type*} [NonUnitalCStarAlgebra A]
+
+local notation "σₙ" => quasispectrum
+local notation "σ" => spectrum
+
+open Unitization NNReal CStarAlgebra
+
+variable [PartialOrder A] [StarOrderedRing A]
+
+lemma CFC.monotoneOn_one_sub_one_add_inv :
+    MonotoneOn (cfcₙ (fun x : ℝ≥0 ↦ 1 - (1 + x)⁻¹)) (Set.Ici (0 : A)) := by
+  intro a ha b hb hab
+  simp only [Set.mem_Ici] at ha hb
+  rw [← inr_le_iff .., nnreal_cfcₙ_eq_cfc_inr a _, nnreal_cfcₙ_eq_cfc_inr b _]
+  rw [← inr_le_iff a b (.of_nonneg ha) (.of_nonneg hb)] at hab
+  rw [← inr_nonneg_iff] at ha hb
+  have h_cfc_one_sub (c : A⁺¹) (hc : 0 ≤ c := by cfc_tac) :
+      cfc (fun x : ℝ≥0 ↦ 1 - (1 + x)⁻¹) c = 1 - cfc (·⁻¹ : ℝ≥0 → ℝ≥0) (1 + c) := by
+    rw [cfc_tsub _ _ _ (fun x _ ↦ by simp) (hg := by fun_prop (disch := intro _ _; positivity)),
+      cfc_const_one ℝ≥0 c, cfc_comp' (·⁻¹) (1 + ·) c ?_, cfc_add .., cfc_const_one ℝ≥0 c,
+      cfc_id' ℝ≥0 c]
+    exact continuousOn_id.inv₀ (Set.forall_mem_image.mpr fun x _ ↦ by dsimp only [id]; positivity)
+  rw [h_cfc_one_sub (a : A⁺¹), h_cfc_one_sub (b : A⁺¹)]
+  gcongr
+  rw [← CFC.rpow_neg_one_eq_cfc_inv, ← CFC.rpow_neg_one_eq_cfc_inv]
+  exact rpow_neg_one_le_rpow_neg_one (add_nonneg zero_le_one ha) (by gcongr) <|
+    isUnit_of_le isUnit_one zero_le_one <| le_add_of_nonneg_right ha
+
+lemma Set.InvOn.one_sub_one_add_inv : Set.InvOn (fun x ↦ 1 - (1 + x)⁻¹) (fun x ↦ x * (1 - x)⁻¹)
+    {x : ℝ≥0 | x < 1} {x : ℝ≥0 | x < 1} := by
+  have : (fun x : ℝ≥0 ↦ x * (1 + x)⁻¹) = fun x ↦ 1 - (1 + x)⁻¹ := by
+    ext x : 1
+    field_simp
+    simp [tsub_mul, inv_mul_cancel₀]
+  rw [← this]
+  constructor <;> intro x (hx : x < 1)
+  · have : 0 < 1 - x := tsub_pos_of_lt hx
+    field_simp [tsub_add_cancel_of_le hx.le, tsub_tsub_cancel_of_le hx.le]
+  · field_simp [mul_tsub]
+
+lemma norm_cfcₙ_one_sub_one_add_inv_lt_one (a : A) :
+    ‖cfcₙ (fun x : ℝ≥0 ↦ 1 - (1 + x)⁻¹) a‖ < 1 :=
+  nnnorm_cfcₙ_nnreal_lt fun x _ ↦ tsub_lt_self zero_lt_one (by positivity)
+
+-- the calls to `fun_prop` with a discharger set off the linter
+set_option linter.style.multiGoal false in
+lemma CStarAlgebra.directedOn_nonneg_ball :
+    DirectedOn (· ≤ ·) ({x : A | 0 ≤ x} ∩ Metric.ball 0 1) := by
+  let f : ℝ≥0 → ℝ≥0 := fun x => 1 - (1 + x)⁻¹
+  let g : ℝ≥0 → ℝ≥0 := fun x => x * (1 - x)⁻¹
+  suffices ∀ a b : A, 0 ≤ a → 0 ≤ b → ‖a‖ < 1 → ‖b‖ < 1 →
+      a ≤ cfcₙ f (cfcₙ g a + cfcₙ g b) by
+    rintro a ⟨(ha₁ : 0 ≤ a), ha₂⟩ b ⟨(hb₁ : 0 ≤ b), hb₂⟩
+    simp only [Metric.mem_ball, dist_zero_right] at ha₂ hb₂
+    refine ⟨cfcₙ f (cfcₙ g a + cfcₙ g b), ⟨by simp, ?_⟩, ?_, ?_⟩
+    · simpa only [Metric.mem_ball, dist_zero_right] using norm_cfcₙ_one_sub_one_add_inv_lt_one _
+    · exact this a b ha₁ hb₁ ha₂ hb₂
+    · exact add_comm (cfcₙ g a) (cfcₙ g b) ▸ this b a hb₁ ha₁ hb₂ ha₂
+  rintro a b ha₁ - ha₂ -
+  calc
+    a = cfcₙ (f ∘ g) a := by
+      conv_lhs => rw [← cfcₙ_id ℝ≥0 a]
+      refine cfcₙ_congr (Set.InvOn.one_sub_one_add_inv.1.eqOn.symm.mono fun x hx ↦ ?_)
+      exact lt_of_le_of_lt (le_nnnorm_of_mem_quasispectrum hx) ha₂
+    _ = cfcₙ f (cfcₙ g a) := by
+      rw [cfcₙ_comp f g a ?_ (by simp [f, tsub_self]) ?_ (by simp [g]) ha₁]
+      · fun_prop (disch := intro _ _; positivity)
+      · have (x) (hx : x ∈ σₙ ℝ≥0 a) :  1 - x ≠ 0 := by
+          refine tsub_pos_of_lt ?_ |>.ne'
+          exact lt_of_le_of_lt (le_nnnorm_of_mem_quasispectrum hx) ha₂
+        fun_prop (disch := assumption)
+    _ ≤ cfcₙ f (cfcₙ g a + cfcₙ g b) := by
+      have hab' : cfcₙ g a ≤ cfcₙ g a + cfcₙ g b := le_add_of_nonneg_right cfcₙ_nonneg_of_predicate
+      exact CFC.monotoneOn_one_sub_one_add_inv cfcₙ_nonneg_of_predicate
+        (cfcₙ_nonneg_of_predicate.trans hab') hab'

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

@@ -386,6 +386,10 @@ lemma norm_le_norm_of_nonneg_of_le {a b : A} (ha : 0 ≤ a := by cfc_tac) (hab :
   rw [cfc_le_iff id (fun _ => ‖b‖) a] at h₂
   exact h₂ ‖a‖ <| norm_mem_spectrum_of_nonneg ha
 
+theorem nnnorm_le_nnnorm_of_nonneg_of_le {a : A} {b : A} (ha : 0 ≤ a := by cfc_tac) (hab : a ≤ b) :
+    ‖a‖₊ ≤ ‖b‖₊ :=
+  norm_le_norm_of_nonneg_of_le ha hab
+
 lemma conjugate_le_norm_smul {a b : A} (hb : IsSelfAdjoint b := by cfc_tac) :
     star a * b * a ≤ ‖b‖ • (star a * a) := by
   suffices ∀ a b : A⁺¹, IsSelfAdjoint b → star a * b * a ≤ ‖b‖ • (star a * a) by
@@ -421,3 +425,35 @@ lemma isClosed_nonneg : IsClosed {a : A | 0 ≤ a} := by
 end CStarAlgebra
 
 end CStar_nonunital
+
+section Pow
+
+namespace CStarAlgebra
+
+variable {A : Type*} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
+
+lemma pow_nonneg {a : A} (ha : 0 ≤ a := by cfc_tac) (n : ℕ) : 0 ≤ a ^ n := by
+  rw [← cfc_pow_id (R := ℝ≥0) a]
+  exact cfc_nonneg_of_predicate
+
+lemma pow_monotone {a : A} (ha : 1 ≤ a) : Monotone (a ^ · : ℕ → A) := by
+  have ha' : 0 ≤ a := zero_le_one.trans ha
+  intro n m hnm
+  simp only
+  rw [← cfc_pow_id (R := ℝ) a, ← cfc_pow_id (R := ℝ) a, cfc_le_iff ..]
+  rw [CFC.one_le_iff (R := ℝ) a] at ha
+  peel ha with x hx _
+  exact pow_le_pow_right₀ (ha x hx) hnm
+
+lemma pow_antitone {a : A} (ha₀ : 0 ≤ a := by cfc_tac) (ha₁ : a ≤ 1) :
+    Antitone (a ^ · : ℕ → A) := by
+  intro n m hnm
+  simp only
+  rw [← cfc_pow_id (R := ℝ) a, ← cfc_pow_id (R := ℝ) a, cfc_le_iff ..]
+  rw [CFC.le_one_iff (R := ℝ) a] at ha₁
+  peel ha₁ with x hx _
+  exact pow_le_pow_of_le_one (spectrum_nonneg_of_nonneg ha₀ hx) (ha₁ x hx) hnm
+
+end CStarAlgebra
+
+end Pow