Sync upstream mathlib4 (2026-08-01, +14 commits)

Counterexamples/CliffordAlgebraNotInjective.lean

@@ -163,10 +163,10 @@ def Q' : QuadraticForm K (Fin 3 → K) :=
   ∑ i, sq i
 
 theorem Q'_add (x y : Fin 3 → K) : Q' (x + y) = Q' x + Q' y := by
-  simp only [Q', QuadraticMap.sum_apply, sq_map_add_char_two, Finset.sum_add_distrib]
+  simp only [Q', sum_apply, sq_map_add_char_two, Finset.sum_add_distrib]
 
 theorem Q'_sub (x y : Fin 3 → K) : Q' (x - y) = Q' x - Q' y := by
-  simp only [Q', QuadraticMap.sum_apply, sq_map_sub_char_two, Finset.sum_sub_distrib]
+  simp only [Q', sum_apply, sq_map_sub_char_two, Finset.sum_sub_distrib]
 
 theorem Q'_apply (a : Fin 3 → K) : Q' a = a 0 * a 0 + a 1 * a 1 + a 2 * a 2 :=
   calc

Mathlib/Algebra/Category/FGModuleCat/EssentiallySmall.lean

@@ -21,7 +21,7 @@ recommended to use the standard `CategoryTheory.SmallModel (FGModuleCat R)` inst
 
 universe v w u
 
-variable (R : Type u) [CommRing R]
+variable (R : Type u) [Ring R]
 
 open CategoryTheory
 

Mathlib/Algebra/QuadraticAlgebra/Basic.lean

@@ -11,20 +11,22 @@ public import Mathlib.Algebra.Star.Unitary
 import Mathlib.Tactic.FieldSimp
 
 /-!
-# Quadratic algebras: involution and norm.
+# Quadratic algebras: involution, norm, and trace.
 
 Let `R` be a commutative ring. We define:
 
 * `QuadraticAlgebra.star`: the quadratic involution
 
 * `QuadraticAlgebra.norm`: the norm
 
+* `QuadraticAlgebra.trace`: the trace, as an `R`-linear map
+
 We prove:
 
 * `QuadraticAlgebra.isUnit_iff_norm_isUnit`:
   `w : QuadraticAlgebra R a b` is a unit iff `w.norm` is a unit in `R`.
 
-* `QuadraticAlgebra.norm_mem_nonZero_divisors_iff`:
+* `QuadraticAlgebra.norm_mem_nonZeroDivisors_iff`:
   `w : QuadraticAlgebra R a b` isn't a zero divisor iff
   `w.norm` isn't a zero divisor in `R`.
 
@@ -148,7 +150,7 @@ section star
 variable [CommRing R]
 
 /-- Conjugation in `QuadraticAlgebra R a b`.
-The conjugate of `x + y ω` is `x + y ω' = (x - a * y) - y ω`. -/
+The conjugate of `x + y ω` is `x + y ω' = (x + b * y) - y ω`. -/
 instance : Star (QuadraticAlgebra R a b) where
   star z := ⟨z.re + b * z.im, -z.im⟩
 
@@ -180,6 +182,11 @@ instance : StarRing (QuadraticAlgebra R a b) where
     simp only [re_star, re_mul, im_mul, im_star, mul_neg, neg_mul, neg_neg] <;> ring
   star_add _ _ := QuadraticAlgebra.ext (by simp only [re_star, re_add, im_add]; ring) (neg_add _ _)
 
+/-- `z - star z` is a multiple of the difference `ω - star ω`. -/
+theorem sub_star (z : QuadraticAlgebra R a b) :
+    z - star z = z.im • (ω - star ω) := by
+  ext <;> simp <;> ring
+
 end star
 
 section norm
@@ -302,6 +309,69 @@ theorem norm_mem_nonZeroDivisors_iff {z : QuadraticAlgebra R a b} :
 
 end norm
 
+section trace
+
+variable [CommRing R]
+
+attribute [local grind =] re_add im_add im_star re_star re_smul im_smul RingHom.id_apply
+  algebraMap_re algebraMap_im
+
+/-- The trace in a quadratic algebra, as an `R`-linear map. -/
+def trace : QuadraticAlgebra R a b →ₗ[R] R where
+  toFun z := 2 * z.re + b * z.im
+  map_add' := by grind
+  map_smul' := by grind [smul_eq_mul]
+
+variable (z : QuadraticAlgebra R a b)
+
+theorem trace_def : trace z = 2 * z.re + b * z.im := rfl
+
+@[simp]
+theorem trace_algebraMap (r : R) :
+    trace (algebraMap R (QuadraticAlgebra R a b) r) = 2 * r := by
+  grind [trace_def]
+
+@[simp]
+theorem trace_natCast (n : ℕ) : trace (n : QuadraticAlgebra R a b) = 2 * n := by
+  simp [trace_def, re_natCast, im_natCast]
+
+@[simp]
+theorem trace_intCast (n : ℤ) : trace (n : QuadraticAlgebra R a b) = 2 * n := by
+  simp [trace_def, re_intCast, im_intCast]
+
+@[simp]
+theorem trace_omega : trace (ω : QuadraticAlgebra R a b) = b := by
+  simp [trace_def]
+
+@[simp]
+theorem trace_one : trace (1 : QuadraticAlgebra R a b) = 2 := by
+  simp [trace_def]
+
+@[simp]
+theorem trace_star : trace (star z) = trace z := by
+  grind [trace_def]
+
+/-- `z + star z` is the trace of `z`. -/
+theorem algebraMap_trace_eq_add_star :
+    algebraMap R (QuadraticAlgebra R a b) (trace z) = z + star z := by
+  ext <;> grind [trace_def]
+
+/-- The conjugate of `z` is `trace z - z`. -/
+theorem star_eq :
+    star z = algebraMap R (QuadraticAlgebra R a b) (trace z) - z := by
+  rw [algebraMap_trace_eq_add_star, add_sub_cancel_left]
+
+/-- Every element of a quadratic algebra satisfies its characteristic equation. -/
+theorem sq_sub_trace_smul_add_norm_eq_zero :
+    z ^ 2 - trace z • z + algebraMap R _ (norm z) = 0 := by
+  rw [Algebra.smul_def, algebraMap_trace_eq_add_star, algebraMap_norm_eq_mul_star]; ring
+
+theorem sq_eq_trace_smul_sub_norm :
+    z ^ 2 = trace z • z - algebraMap R _ (norm z) := by
+  rw [← sub_eq_zero, ← sub_add, sq_sub_trace_smul_add_norm_eq_zero]
+
+end trace
+
 section field
 
 variable [Field K] {a b : K} [Hab : Fact (∀ r, r ^ 2 ≠ a + b * r)]

Mathlib/AlgebraicGeometry/Group/Affine.lean

@@ -298,7 +298,7 @@ def Spec.mapMulEquiv {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] [Bi
 
 /-- The adjunction between `Spec` and `Γ` as functors between commutative `R`-algebras and
 schemes over `Spec R`. -/
-def algΓAlgSpecAdjunction (R : CommRingCat) : algΓ R ⊣ algSpec R := by
+def algΓAlgSpecAdjunction (R : CommRingCat.{u}) : algΓ R ⊣ algSpec R := by
   have overAdjunction := Over.postAdjunctionRight (Y := .op <| R) ΓSpec.adjunction
   have overEquivAlg := ((Over.opEquivOpUnder R).trans (commAlgCatEquivUnder R).op.symm).toAdjunction
   simpa using! overAdjunction.comp overEquivAlg

Mathlib/Analysis/LocallyConvex/Basic.lean

@@ -6,7 +6,8 @@ Authors: Jean Lo, Bhavik Mehta, Yaël Dillies
 module
 
 public import Mathlib.Analysis.Convex.Hull
-public import Mathlib.Analysis.Normed.Module.Basic
+public import Mathlib.Analysis.Normed.Field.Lemmas
+public import Mathlib.Analysis.Normed.MulAction
 public import Mathlib.Topology.Bornology.Absorbs
 /-!
 # Local convexity
@@ -45,6 +46,8 @@ absorbent, balanced, locally convex, LCTVS
 
 @[expose] public section
 
+assert_not_exists NormedSpace
+
 open Set
 open scoped Pointwise Topology
 

Mathlib/Analysis/Seminorm.lean

@@ -977,7 +977,7 @@ end NormedField
 
 section Convex
 
-variable [NormedField 𝕜] [AddCommGroup E] [NormedSpace ℝ 𝕜] [Module 𝕜 E]
+variable [NormedField 𝕜] [AddCommGroup E] [SMul ℝ 𝕜] [NormSMulClass ℝ 𝕜] [Module 𝕜 E]
 
 section SMul
 
@@ -1018,7 +1018,7 @@ end Convex
 
 section RestrictScalars
 
-variable (𝕜) {𝕜' : Type*} [NormedField 𝕜] [SeminormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜']
+variable (𝕜) {𝕜' : Type*} [NormedField 𝕜] [SeminormedRing 𝕜'] [SMul 𝕜 𝕜'] [NormSMulClass 𝕜 𝕜']
   [NormOneClass 𝕜'] [AddCommGroup E] [Module 𝕜' E] [SMul 𝕜 E] [IsScalarTower 𝕜 𝕜' E]
 
 /-- Reinterpret a seminorm over a field `𝕜'` as a seminorm over a smaller field `𝕜`. This will

Mathlib/CategoryTheory/Adjunction/Basic.lean

@@ -79,8 +79,6 @@ Conversely `Equivalence.toAdjunction` recovers the underlying adjunction from an
   isomorphism `L ⋙ R ≅ 𝟭 C`, the unit is an isomorphism, and similarly for the counit.
 -/
 
-set_option backward.defeqAttrib.useBackward true
-
 @[expose] public section
 
 namespace CategoryTheory
@@ -314,7 +312,6 @@ def corepresentableBy (X : C) :
   homEquiv := adj.homEquiv _ _
   homEquiv_comp := by simp
 
-set_option backward.isDefEq.respectTransparency false in
 /-- If `adj : F ⊣ G`, and `Y : D`, then `G.obj Y` represents `X ↦ (F.obj X ⟶ Y)`. -/
 @[simps]
 def representableBy (Y : D) :
@@ -538,7 +535,6 @@ lemma homEquiv_ofNatIsoRight_symm_apply {F : C ⥤ D} {G H : D ⥤ C} (adj : F 
       (adj.homEquiv _ _).symm (f ≫ iso.inv.app _) := by
   simp
 
-set_option backward.isDefEq.respectTransparency.types false in
 /-- The isomorphism which an adjunction `F ⊣ G` induces on `G ⋙ yoneda`. This states that
 `Adjunction.homEquiv` is natural in both arguments. -/
 @[simps!]
@@ -547,7 +543,6 @@ def compYonedaIso {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.
     G ⋙ yoneda ≅ yoneda ⋙ (whiskeringLeft _ _ _).obj F.op :=
   NatIso.ofComponents fun X => NatIso.ofComponents fun Y => (adj.homEquiv Y.unop X).toIso.symm
 
-set_option backward.isDefEq.respectTransparency.types false in
 /-- The isomorphism which an adjunction `F ⊣ G` induces on `F.op ⋙ coyoneda`. This states that
 `Adjunction.homEquiv` is natural in both arguments. -/
 @[simps!]
@@ -556,7 +551,7 @@ def compCoyonedaIso {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Categor
     F.op ⋙ coyoneda ≅ coyoneda ⋙ (whiskeringLeft _ _ _).obj G :=
   NatIso.ofComponents fun X => NatIso.ofComponents fun Y => (adj.homEquiv X.unop Y).toIso
 
-set_option backward.isDefEq.respectTransparency.types false in
+set_option backward.defeqAttrib.useBackward true in
 /-- The isomorphism which an adjunction `F ⊣ G` induces on `F.op ⋙ uliftCoyoneda`.
 This states that `Adjunction.homEquiv` is natural in both arguments. -/
 @[simps!]
@@ -611,7 +606,7 @@ variable (e : ∀ X Y, (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y))
 a bijection `e` between `F_obj X ⟶ Y` and `X ⟶ G.obj Y` satisfying a naturality law
 `he : ∀ X Y Y' g h, e X Y' (h ≫ g) = e X Y h ≫ G.map g`.
 Dual to `rightAdjointOfEquiv`. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def leftAdjointOfEquiv (he : ∀ X Y Y' g h, e X Y' (h ≫ g) = e X Y h ≫ G.map g) : C ⥤ D where
   obj := F_obj
   map {X} {X'} f := (e X (F_obj X')).symm (f ≫ e X' (F_obj X') (𝟙 _))
@@ -624,7 +619,6 @@ def leftAdjointOfEquiv (he : ∀ X Y Y' g h, e X Y' (h ≫ g) = e X Y h ≫ G.ma
 
 variable (he : ∀ X Y Y' g h, e X Y' (h ≫ g) = e X Y h ≫ G.map g)
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Show that the functor given by `leftAdjointOfEquiv` is indeed left adjoint to `G`. Dual
 to `adjunctionOfEquivRight`. -/
 @[simps!]
@@ -653,7 +647,7 @@ private theorem he'' (he : ∀ X' X Y f g, e X' Y (F.map f ≫ g) = f ≫ e X Y
 a bijection `e` between `F.obj X ⟶ Y` and `X ⟶ G_obj Y` satisfying a naturality law
 `he : ∀ X' X Y f g, e X' Y (F.map f ≫ g) = f ≫ e X Y g`.
 Dual to `leftAdjointOfEquiv`. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def rightAdjointOfEquiv (he : ∀ X' X Y f g, e X' Y (F.map f ≫ g) = f ≫ e X Y g) : D ⥤ C where
   obj := G_obj
   map {Y} {Y'} g := (e (G_obj Y) Y') ((e (G_obj Y) Y).symm (𝟙 _) ≫ g)
@@ -664,7 +658,6 @@ def rightAdjointOfEquiv (he : ∀ X' X Y f g, e X' Y (F.map f ≫ g) = f ≫ e X
       rw [← assoc, he'' e he, comp_id, Equiv.symm_apply_apply]
     simp
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Show that the functor given by `rightAdjointOfEquiv` is indeed right adjoint to `F`. Dual
 to `adjunctionOfEquivLeft`. -/
 @[simps!]