Merge remote-tracking branch 'upstream/master' into bump/v4.23.0

Author: kim-em

Archive/Wiedijk100Theorems/InverseTriangleSum.lean

@@ -26,10 +26,11 @@ discrete_sum
 open Finset
 
 /-- **Sum of the Reciprocals of the Triangular Numbers** -/
-theorem Theorems100.inverse_triangle_sum :
-    ∀ n, ∑ k ∈ range n, (2 : ℚ) / (k * (k + 1)) = if n = 0 then 0 else 2 - (2 : ℚ) / n := by
-  refine sum_range_induction _ _ rfl ?_
+theorem Theorems100.inverse_triangle_sum (n : ℕ) :
+    ∑ k ∈ range n, (2 : ℚ) / (k * (k + 1)) = if n = 0 then 0 else 2 - (2 : ℚ) / n := by
+  apply sum_range_induction _ _ rfl
   rintro (_ | _)
   · norm_num
-  field_simp
-  ring
+  · field_simp
+    ring_nf
+    simp

Counterexamples/CliffordAlgebraNotInjective.lean

@@ -8,6 +8,7 @@ import Mathlib.Algebra.CharP.Quotient
 import Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
 import Mathlib.RingTheory.MvPolynomial.Basic
 import Mathlib.RingTheory.MvPolynomial.Ideal
+import Mathlib.Tactic.Ring.NamePolyVars
 
 /-! # `algebraMap R (CliffordAlgebra Q)` is not always injective.
 
@@ -34,36 +35,39 @@ noncomputable section
 open LinearMap (BilinForm)
 open LinearMap (BilinMap)
 
+name_poly_vars X, Y, Z over ZMod 2
+
 namespace Q60596
 
 open MvPolynomial
 
 /-- The monomial ideal generated by terms of the form $x_ix_i$. -/
 def kIdeal : Ideal (MvPolynomial (Fin 3) (ZMod 2)) :=
-  Ideal.span (Set.range fun i => (X i * X i : MvPolynomial (Fin 3) (ZMod 2)))
+  Ideal.span (Set.range fun i =>
+    (MvPolynomial.X i * MvPolynomial.X i : MvPolynomial (Fin 3) (ZMod 2)))
 
 theorem mem_kIdeal_iff (x : MvPolynomial (Fin 3) (ZMod 2)) :
     x ∈ kIdeal ↔ ∀ m : Fin 3 →₀ ℕ, m ∈ x.support → ∃ i, 2 ≤ m i := by
   have :
       kIdeal = Ideal.span ((monomial · (1 : ZMod 2)) '' Set.range (Finsupp.single · 2)) := by
-    simp_rw [kIdeal, X, monomial_mul, one_mul, ← Finsupp.single_add, ← Set.range_comp,
+    simp_rw [kIdeal, MvPolynomial.X, monomial_mul, one_mul, ← Finsupp.single_add, ← Set.range_comp,
       Function.comp_def]
   rw [this, mem_ideal_span_monomial_image]
   simp
 
-theorem X0_X1_X2_notMem_kIdeal : (X 0 * X 1 * X 2 : MvPolynomial (Fin 3) (ZMod 2)) ∉ kIdeal := by
+theorem X_Y_Z_notMem_kIdeal : (X * Y * Z : MvPolynomial (Fin 3) (ZMod 2)) ∉ kIdeal := by
   intro h
   simp_rw [mem_kIdeal_iff, support_mul_X, support_X, Finset.map_singleton, addRightEmbedding_apply,
     Finset.mem_singleton, forall_eq, ← Fin.sum_univ_three fun i => Finsupp.single i 1,
     ← Finsupp.equivFunOnFinite_symm_eq_sum] at h
   contradiction
 
-@[deprecated (since := "2025-05-23")] alias X0_X1_X2_not_mem_kIdeal := X0_X1_X2_notMem_kIdeal
+@[deprecated (since := "2025-05-23")] alias X_Y_Z_not_mem_kIdeal := X_Y_Z_notMem_kIdeal
 
-theorem mul_self_mem_kIdeal_of_X0_X1_X2_mul_mem {x : MvPolynomial (Fin 3) (ZMod 2)}
-    (h : X 0 * X 1 * X 2 * x ∈ kIdeal) : x * x ∈ kIdeal := by
+theorem mul_self_mem_kIdeal_of_X_Y_Z_mul_mem {x : MvPolynomial (Fin 3) (ZMod 2)}
+    (h : X * Y * Z * x ∈ kIdeal) : x * x ∈ kIdeal := by
   rw [mem_kIdeal_iff] at h
-  have : x ∈ Ideal.span ((X : Fin 3 → MvPolynomial _ (ZMod 2)) '' Set.univ) := by
+  have : x ∈ Ideal.span ((MvPolynomial.X : Fin 3 → MvPolynomial _ (ZMod 2)) '' Set.univ) := by
     rw [mem_ideal_span_X_image]
     intro m hm
     simp_rw [mul_assoc, support_X_mul, Finset.map_map, Finset.mem_map,
@@ -127,11 +131,11 @@ theorem sq_zero_of_αβγ_mul {x : K} : α * β * γ * x = 0 → x * x = 0 := by
   induction x using Quotient.inductionOn'
   change Ideal.Quotient.mk _ _ = 0 → Ideal.Quotient.mk _ _ = 0
   rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.Quotient.eq_zero_iff_mem]
-  exact mul_self_mem_kIdeal_of_X0_X1_X2_mul_mem
+  exact mul_self_mem_kIdeal_of_X_Y_Z_mul_mem
 
 /-- Though `αβγ` is not itself zero -/
 theorem αβγ_ne_zero : α * β * γ ≠ 0 := fun h =>
-  X0_X1_X2_notMem_kIdeal <| Ideal.Quotient.eq_zero_iff_mem.1 h
+  X_Y_Z_notMem_kIdeal <| Ideal.Quotient.eq_zero_iff_mem.1 h
 
 /-- The 1-form on $K^3$, the kernel of which we will take a quotient by.
 

Mathlib.lean

@@ -92,6 +92,7 @@ import Mathlib.Algebra.Category.CoalgCat.Basic
 import Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
 import Mathlib.Algebra.Category.CoalgCat.Monoidal
 import Mathlib.Algebra.Category.CommAlgCat.Basic
+import Mathlib.Algebra.Category.CommAlgCat.FiniteType
 import Mathlib.Algebra.Category.ContinuousCohomology.Basic
 import Mathlib.Algebra.Category.FGModuleCat.Basic
 import Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall
@@ -953,6 +954,7 @@ import Mathlib.Algebra.Polynomial.CoeffMem
 import Mathlib.Algebra.Polynomial.Degree.CardPowDegree
 import Mathlib.Algebra.Polynomial.Degree.Definitions
 import Mathlib.Algebra.Polynomial.Degree.Domain
+import Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
 import Mathlib.Algebra.Polynomial.Degree.Lemmas
 import Mathlib.Algebra.Polynomial.Degree.Monomial
 import Mathlib.Algebra.Polynomial.Degree.Operations
@@ -1904,6 +1906,7 @@ import Mathlib.CategoryTheory.Abelian.Pseudoelements
 import Mathlib.CategoryTheory.Abelian.Refinements
 import Mathlib.CategoryTheory.Abelian.RightDerived
 import Mathlib.CategoryTheory.Abelian.SerreClass.Basic
+import Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
 import Mathlib.CategoryTheory.Abelian.Subobject
 import Mathlib.CategoryTheory.Abelian.Transfer
 import Mathlib.CategoryTheory.Abelian.Yoneda
@@ -5081,6 +5084,7 @@ import Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
 import Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
 import Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
 import Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
+import Mathlib.RepresentationTheory.Homological.GroupCohomology.Shapiro
 import Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
 import Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
 import Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
@@ -5495,6 +5499,7 @@ import Mathlib.RingTheory.Regular.Category
 import Mathlib.RingTheory.Regular.Depth
 import Mathlib.RingTheory.Regular.IsSMulRegular
 import Mathlib.RingTheory.Regular.RegularSequence
+import Mathlib.RingTheory.RingHom.Etale
 import Mathlib.RingTheory.RingHom.Finite
 import Mathlib.RingTheory.RingHom.FinitePresentation
 import Mathlib.RingTheory.RingHom.FiniteType
@@ -5929,6 +5934,7 @@ import Mathlib.Tactic.Rify
 import Mathlib.Tactic.Ring
 import Mathlib.Tactic.Ring.Basic
 import Mathlib.Tactic.Ring.Compare
+import Mathlib.Tactic.Ring.NamePolyVars
 import Mathlib.Tactic.Ring.PNat
 import Mathlib.Tactic.Ring.RingNF
 import Mathlib.Tactic.Sat.FromLRAT

Mathlib/Algebra/Algebra/Bilinear.lean

@@ -89,7 +89,7 @@ def mul : A →ₗ[R] A →ₗ[R] A :=
 
 /-- The multiplication map on a non-unital algebra, as an `R`-linear map from `A ⊗[R] A` to `A`. -/
 -- TODO: upgrade to A-linear map if A is a semiring.
-noncomputable def mul' : A ⊗[R] A →ₗ[R] A :=
+def mul' : A ⊗[R] A →ₗ[R] A :=
   TensorProduct.lift (mul R A)
 
 variable {A}

Mathlib/Algebra/Algebra/Equiv.lean

@@ -758,3 +758,10 @@ def toAlgAut : G →* A ≃ₐ[R] A where
 end
 
 end MulSemiringAction
+
+/-- The algebra equivalence between `ULift A` and `A`. -/
+@[simps! -isSimp apply]
+def ULift.algEquiv {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] :
+    ULift.{w} A ≃ₐ[R] A where
+  __ := ULift.ringEquiv
+  commutes' _ := rfl

Mathlib/Algebra/Azumaya/Basic.lean

@@ -39,7 +39,7 @@ lemma AlgHom.mulLeftRight_bij [h : IsAzumaya R A] :
 
 /-- The "canonical" isomorphism between `R ⊗ Rᵒᵖ` and `End R R` which is equal
   to `AlgHom.mulLeftRight R R`. -/
-noncomputable abbrev tensorEquivEnd : R ⊗[R] Rᵐᵒᵖ ≃ₐ[R] Module.End R R :=
+abbrev tensorEquivEnd : R ⊗[R] Rᵐᵒᵖ ≃ₐ[R] Module.End R R :=
   Algebra.TensorProduct.lid R Rᵐᵒᵖ|>.trans <| .moduleEndSelf R
 
 lemma coe_tensorEquivEnd : tensorEquivEnd R = AlgHom.mulLeftRight R R := by

Mathlib/Algebra/Azumaya/Defs.lean

@@ -32,12 +32,12 @@ variable (R A : Type*) [CommSemiring R] [Semiring A] [Algebra R A]
 open TensorProduct MulOpposite
 
 /-- `A` as a `A ⊗[R] Aᵐᵒᵖ`-module (or equivalently, an `A`-`A` bimodule). -/
-noncomputable abbrev instModuleTensorProductMop :
+abbrev instModuleTensorProductMop :
   Module (A ⊗[R] Aᵐᵒᵖ) A := TensorProduct.Algebra.module
 
 /-- The canonical map from `A ⊗[R] Aᵐᵒᵖ` to `Module.End R A` where
   `a ⊗ b` maps to `f : x ↦ a * x * b`. -/
-noncomputable def AlgHom.mulLeftRight : (A ⊗[R] Aᵐᵒᵖ) →ₐ[R] Module.End R A :=
+def AlgHom.mulLeftRight : (A ⊗[R] Aᵐᵒᵖ) →ₐ[R] Module.End R A :=
   letI : Module (A ⊗[R] Aᵐᵒᵖ) A := TensorProduct.Algebra.module
   letI : IsScalarTower R (A ⊗[R] Aᵐᵒᵖ) A := {
     smul_assoc := fun r ab a ↦ by

Mathlib/Algebra/BigOperators/Finprod.lean

@@ -1145,4 +1145,24 @@ theorem finprod_emb_domain (f : α ↪ β) [DecidablePred (· ∈ Set.range f)]
     (∏ᶠ b : β, if h : b ∈ Set.range f then g (Classical.choose h) else 1) = ∏ᶠ a : α, g a :=
   finprod_emb_domain' f.injective g
 
+@[simp, norm_cast]
+lemma Nat.cast_finprod [Finite ι] {R : Type*} [CommSemiring R] (f : ι → ℕ) :
+    ↑(∏ᶠ x, f x : ℕ) = ∏ᶠ x, (f x : R) :=
+  (Nat.castRingHom R).map_finprod f.mulSupport.toFinite
+
+@[simp, norm_cast]
+lemma Nat.cast_finprod_mem {s : Set ι} (hs : s.Finite) {R : Type*} [CommSemiring R] (f : ι → ℕ) :
+    ↑(∏ᶠ x ∈ s, f x : ℕ) = ∏ᶠ x ∈ s, (f x : R) :=
+  (Nat.castRingHom R).map_finprod_mem _ hs
+
+@[simp, norm_cast]
+lemma Nat.cast_finsum [Finite ι] {M : Type*} [AddCommMonoidWithOne M]
+    (f : ι → ℕ) : ↑(∑ᶠ x, f x : ℕ) = ∑ᶠ x, (f x : M) :=
+  (Nat.castAddMonoidHom M).map_finsum f.support.toFinite
+
+@[simp, norm_cast]
+lemma Nat.cast_finsum_mem {s : Set ι} (hs : s.Finite) {M : Type*}
+    [AddCommMonoidWithOne M] (f : ι → ℕ) : ↑(∑ᶠ x ∈ s, f x : ℕ) = ∑ᶠ x ∈ s, (f x : M) :=
+  (Nat.castAddMonoidHom M).map_finsum_mem _ hs
+
 end type

Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

@@ -604,19 +604,22 @@ theorem prod_multiset_count_of_subset [DecidableEq M] (m : Multiset M) (s : Fins
   apply prod_list_count_of_subset l s
 
 /-- For any product along `{0, ..., n - 1}` of a commutative-monoid-valued function, we can verify
-that it's equal to a different function just by checking ratios of adjacent terms.
+that it's equal to a different function just by checking ratios of adjacent terms up to `n`.
 
 This is a multiplicative discrete analogue of the fundamental theorem of calculus. -/
 @[to_additive "For any sum along `{0, ..., n - 1}` of a commutative-monoid-valued function, we can
-verify that it's equal to a different function just by checking differences of adjacent terms.
+verify that it's equal to a different function just by checking differences of adjacent terms up to
+`n`.
 
 This is a discrete analogue of the fundamental theorem of calculus."]
 theorem prod_range_induction (f s : ℕ → M) (base : s 0 = 1)
-    (step : ∀ n, s (n + 1) = s n * f n) (n : ℕ) :
+    (n : ℕ) (step : ∀ k < n, s (k + 1) = s k * f k) :
     ∏ k ∈ Finset.range n, f k = s n := by
   induction n with
   | zero => rw [Finset.prod_range_zero, base]
-  | succ k hk => simp only [hk, Finset.prod_range_succ, step, mul_comm]
+  | succ k hk =>
+    rw [Finset.prod_range_succ, step _ (Nat.lt_succ_self _), hk]
+    exact fun _ hl ↦ step _ (Nat.lt_succ_of_lt hl)
 
 @[to_additive (attr := simp)]
 theorem prod_const (b : M) : ∏ _x ∈ s, b = b ^ #s :=
@@ -921,7 +924,7 @@ lemma sum_range_tsub {f : ℕ → M} (h : Monotone f) (n : ℕ) :
   apply sum_range_induction
   case base => apply tsub_eq_of_eq_add; rw [zero_add]
   case step =>
-    intro n
+    intro n _
     have h₁ : f n ≤ f (n + 1) := h (Nat.le_succ _)
     have h₂ : f 0 ≤ f n := h (Nat.zero_le _)
     rw [tsub_add_eq_add_tsub h₂, add_tsub_cancel_of_le h₁]

Mathlib/Algebra/Category/CommAlgCat/Basic.lean

@@ -5,6 +5,8 @@ Authors: Yaël Dillies, Christian Merten, Michał Mrugała, Andrew Yang
 -/
 import Mathlib.Algebra.Category.AlgCat.Basic
 import Mathlib.Algebra.Category.Ring.Under.Basic
+import Mathlib.CategoryTheory.Limits.Over
+import Mathlib.CategoryTheory.WithTerminal.Cone
 
 /-!
 # The category of commutative algebras over a commutative ring
@@ -17,7 +19,7 @@ namespace CategoryTheory
 
 open Limits
 
-universe v u
+universe w v u
 
 variable {R : Type u} [CommRing R]
 
@@ -165,6 +167,25 @@ instance reflectsIsomorphisms_forget : (forget (CommAlgCat.{u} R)).ReflectsIsomo
     let e : X ≃ₐ[R] Y := { f.hom, i.toEquiv with }
     exact (isoMk e).isIso_hom
 
+variable (R)
+
+/-- Universe lift functor for commutative algebras. -/
+def uliftFunctor : CommAlgCat.{v} R ⥤ CommAlgCat.{max v w} R where
+  obj A := .of R <| ULift A
+  map {A B} f := CommAlgCat.ofHom <|
+    ULift.algEquiv.symm.toAlgHom.comp <| f.hom.comp ULift.algEquiv.toAlgHom
+
+/-- The universe lift functor for commutative algebras is fully faithful. -/
+def fullyFaithfulUliftFunctor : (uliftFunctor R).FullyFaithful where
+  preimage {A B} f :=
+    CommAlgCat.ofHom <| ULift.algEquiv.toAlgHom.comp <| f.hom.comp ULift.algEquiv.symm.toAlgHom
+
+instance : (uliftFunctor R).Full :=
+  (fullyFaithfulUliftFunctor R).full
+
+instance : (uliftFunctor R).Faithful :=
+  (fullyFaithfulUliftFunctor R).faithful
+
 end CommAlgCat
 
 /-- The category of commutative algebras over a commutative ring `R` is the same as commutative
@@ -179,4 +200,12 @@ def commAlgCatEquivUnder (R : CommRingCat) : CommAlgCat R ≌ Under R where
     CommAlgCat.isoMk { toRingEquiv := .refl A, commutes' _ := rfl }
   counitIso := .refl _
 
+-- TODO: Generalize to `UnivLE.{u, v}` once `commAlgCatEquivUnder` is generalized.
+instance : HasColimits (CommAlgCat.{u} R) :=
+  Adjunction.has_colimits_of_equivalence (commAlgCatEquivUnder (.of R)).functor
+
+-- TODO: Generalize to `UnivLE.{u, v}` once `commAlgCatEquivUnder` is generalized.
+instance : HasLimits (CommAlgCat.{u} R) :=
+  Adjunction.has_limits_of_equivalence (commAlgCatEquivUnder (.of R)).functor
+
 end CategoryTheory