Merge master into nightly-testing

Author: mathlib-nightly-testing[bot]

.github/actions/get-mathlib-ci/action.yml

@@ -10,7 +10,7 @@ inputs:
     # Default pinned commit used by workflows unless they explicitly override.
     # Update this ref as needed to pick up changes to mathlib-ci scripts
     # This is also updated automatically by .github/workflows/update_dependencies.yml
-    default: ca86f6900d53e503e28ec1cfa2bff2f505474553
+    default: e356ad9e608e88717854e578c6d898b43e37d3e2
   path:
     description: Checkout destination path.
     required: false

Mathlib.lean

@@ -235,6 +235,7 @@ public import Mathlib.Algebra.Category.Ring.LinearAlgebra
 public import Mathlib.Algebra.Category.Ring.Topology
 public import Mathlib.Algebra.Category.Ring.Under.Basic
 public import Mathlib.Algebra.Category.Ring.Under.Limits
+public import Mathlib.Algebra.Category.Ring.Under.Property
 public import Mathlib.Algebra.Category.Semigrp.Basic
 public import Mathlib.Algebra.Central.Basic
 public import Mathlib.Algebra.Central.Defs
@@ -1557,6 +1558,7 @@ public import Mathlib.AlgebraicTopology.SimplicialSet.PiZero
 public import Mathlib.AlgebraicTopology.SimplicialSet.Presentable
 public import Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
 public import Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplexOne
+public import Mathlib.AlgebraicTopology.SimplicialSet.PushoutProduct
 public import Mathlib.AlgebraicTopology.SimplicialSet.RegularEpi
 public import Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
 public import Mathlib.AlgebraicTopology.SimplicialSet.Simplices
@@ -2729,6 +2731,7 @@ public import Mathlib.CategoryTheory.LiftingProperties.Basic
 public import Mathlib.CategoryTheory.LiftingProperties.Limits
 public import Mathlib.CategoryTheory.LiftingProperties.Over
 public import Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
+public import Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
 public import Mathlib.CategoryTheory.Limits.Bicones
 public import Mathlib.CategoryTheory.Limits.ColimitLimit
 public import Mathlib.CategoryTheory.Limits.Comma
@@ -6725,6 +6728,7 @@ public import Mathlib.RingTheory.Regular.Category
 public import Mathlib.RingTheory.Regular.Depth
 public import Mathlib.RingTheory.Regular.Flat
 public import Mathlib.RingTheory.Regular.IsSMulRegular
+public import Mathlib.RingTheory.Regular.ProjectiveDimension
 public import Mathlib.RingTheory.Regular.RegularSequence
 public import Mathlib.RingTheory.RegularLocalRing.Defs
 public import Mathlib.RingTheory.RingHom.Bijective

Mathlib/Algebra/Azumaya/Matrix.lean

@@ -37,7 +37,7 @@ abbrev AlgHom.mulLeftRightMatrix_inv :
   toFun f := ∑ ⟨⟨i, j⟩, k, l⟩ : (n × n) × n × n,
     f (single j k 1) i l • (single i j 1) ⊗ₜ[R] op (single k l 1)
   map_add' f1 f2 := by simp [add_smul, Finset.sum_add_distrib]
-  map_smul' r f := by simp [SemigroupAction.mul_smul, Finset.smul_sum]
+  map_smul' r f := by simp [mul_smul, Finset.smul_sum]
 
 lemma AlgHom.mulLeftRightMatrix.inv_comp :
     (AlgHom.mulLeftRightMatrix_inv R n).comp

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

@@ -156,10 +156,10 @@ lemma prod_filter_not_mul_prod_filter (s : Finset ι) (p : ι → Prop) [Decidab
 set_option backward.isDefEq.respectTransparency false in
 @[to_additive]
 theorem prod_filter_xor (p q : ι → Prop) [DecidablePred p] [DecidablePred q] :
-    (∏ x ∈ s with (Xor' (p x) (q x)), f x) =
+    (∏ x ∈ s with (Xor (p x) (q x)), f x) =
       (∏ x ∈ s with (p x ∧ ¬ q x), f x) * (∏ x ∈ s with (q x ∧ ¬ p x), f x) := by
   classical rw [← prod_union (disjoint_filter_and_not_filter _ _), ← filter_or]
-  simp only [Xor']
+  simp only [Xor]
 
 @[to_additive]
 theorem _root_.IsCompl.prod_mul_prod [Fintype ι] {s t : Finset ι} (h : IsCompl s t) (f : ι → M) :

Mathlib/Algebra/Category/ModuleCat/Ext/Finite.lean

@@ -24,7 +24,6 @@ variable (R : Type u) [CommRing R]
 
 open CategoryTheory Abelian
 
-set_option backward.isDefEq.respectTransparency false in
 instance ModuleCat.finite_ext [Small.{v} R] [IsNoetherianRing R] (N M : ModuleCat.{v} R)
     [Module.Finite R N] [Module.Finite R M] (i : ℕ) : Module.Finite R (Ext N M i) := by
   induction i generalizing N with

Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean

@@ -65,7 +65,6 @@ theorem monoidalClosed_uncurry
     MonoidalClosed.uncurry f (x ⊗ₜ[R] y) = (f y).hom x :=
   rfl
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Describes the counit of the adjunction `M ⊗ - ⊣ Hom(M, -)`. Given an `R`-module `N` this
 should give a map `M ⊗ Hom(M, N) ⟶ N`, so we flip the order of the arguments in the identity map
 `Hom(M, N) ⟶ (M ⟶ N)` and uncurry the resulting map `M ⟶ Hom(M, N) ⟶ N.` -/
@@ -85,7 +84,6 @@ theorem ihom_coev_app (M N : ModuleCat.{u} R) :
     (ihom.coev M).app N = ModuleCat.ofHom₂ (TensorProduct.mk _ _ _).flip :=
   rfl
 
-set_option backward.isDefEq.respectTransparency false in
 theorem monoidalClosed_pre_app {M N : ModuleCat.{u} R} (P : ModuleCat.{u} R) (f : N ⟶ M) :
     (MonoidalClosed.pre f).app P = ofHom (homLinearEquiv.symm.toLinearMap ∘ₗ
       LinearMap.lcomp _ _ f.hom ∘ₗ homLinearEquiv.toLinearMap) :=

Mathlib/Algebra/Category/Ring/Limits.lean

@@ -8,7 +8,7 @@ module
 public import Mathlib.Algebra.Category.Grp.Limits
 public import Mathlib.Algebra.Category.Ring.Basic
 public import Mathlib.Algebra.Ring.Pi
-public import Mathlib.Algebra.Ring.Shrink
+public import Mathlib.Algebra.Ring.Shrink  -- shake: keep (Semiring (Shrink ...)), cf. lean#13417
 public import Mathlib.Algebra.Ring.Subring.Defs
 
 /-!

Mathlib/Algebra/Category/Ring/Under/Property.lean

@@ -0,0 +1,119 @@
+/-
+Copyright (c) 2025 Christian Merten. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Merten
+-/
+module
+
+public import Mathlib.Algebra.Category.Ring.Under.Limits
+public import Mathlib.CategoryTheory.Limits.MorphismProperty
+public import Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
+
+/-!
+# Properties of `P.Under ⊤ R` for `R : CommRingCat`
+
+In this file we translate ring theoretic properties of a property of ring homomorphisms
+`P` in properties of the category `P.Under ⊤ R`.
+
+## Main results
+
+- `CommRingCat.Under.hasFiniteLimits`: If `P` is stable under finite products and equalizers,
+  `P.Under ⊤ R` has finite limits.
+-/
+
+@[expose] public section
+
+universe u
+
+open CategoryTheory Limits
+
+variable {Q : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop}
+
+open MorphismProperty
+
+lemma RingHom.HasFiniteProducts.isClosedUnderLimitsOfShape (hQi : RespectsIso Q)
+    (hQp : HasFiniteProducts Q) (R : CommRingCat.{u}) :
+    (toMorphismProperty Q).underObj (X := R).IsClosedUnderFiniteProducts := by
+  refine .of_isClosedUnderLimitsOfShape fun (J : Type u) _ ↦ ⟨fun A ⟨pres, hpres⟩ ↦ ?_⟩
+  let e : A ≅ CommRingCat.mkUnder R (Π i, pres.diag.obj ⟨i⟩) :=
+    (limit.isoLimitCone ⟨_, pres.isLimit⟩).symm ≪≫
+      HasLimit.isoOfNatIso (Discrete.natIso fun i ↦ eqToIso <| by simp) ≪≫
+      limit.isoLimitCone ⟨CommRingCat.Under.piFan <| fun i ↦ (pres.diag.obj ⟨i⟩),
+        CommRingCat.Under.piFanIsLimit <| fun i ↦ (pres.diag.obj ⟨i⟩)⟩
+  have : (toMorphismProperty Q).RespectsIso := toMorphismProperty_respectsIso_iff.mp hQi
+  rw [underObj_iff, ← Under.w e.inv, (toMorphismProperty Q).cancel_right_of_respectsIso]
+  exact hQp _ fun i ↦ hpres _
+
+lemma RingHom.HasEqualizers.isClosedUnderLimitsOfShape (hQi : RespectsIso Q)
+    (hQe : HasEqualizers Q) (R : CommRingCat.{u}) :
+    (toMorphismProperty Q).underObj (X := R).IsClosedUnderLimitsOfShape WalkingParallelPair := by
+  refine ⟨fun A ⟨pres, hpres⟩ ↦ ?_⟩
+  let e : A ≅
+      CommRingCat.mkUnder R
+        (AlgHom.equalizer (R := R)
+          (CommRingCat.toAlgHom (pres.diag.map .left))
+          (CommRingCat.toAlgHom (pres.diag.map .right))) :=
+    (limit.isoLimitCone ⟨_, pres.isLimit⟩).symm ≪≫
+      HasLimit.isoOfNatIso (diagramIsoParallelPair _) ≪≫ limit.isoLimitCone
+        ⟨CommRingCat.Under.equalizerFork (pres.diag.map .left) (pres.diag.map .right),
+          CommRingCat.Under.equalizerForkIsLimit
+            (pres.diag.map .left) (pres.diag.map .right)⟩
+  have : (toMorphismProperty Q).RespectsIso := toMorphismProperty_respectsIso_iff.mp hQi
+  rw [underObj_iff, ← Under.w e.inv, (toMorphismProperty Q).cancel_right_of_respectsIso]
+  exact hQe _ _ (hpres .zero) (hpres .one)
+
+/-- If `Q` is stable under finite products, the inclusion from the subcategory of `Under R` defined
+by `Q` creates finite products. -/
+@[implicit_reducible]
+noncomputable def RingHom.HasFiniteProducts.createsFiniteProductsForget
+    (hQi : RespectsIso Q) (hQp : HasFiniteProducts Q) (R : CommRingCat.{u}) :
+    CreatesFiniteProducts (MorphismProperty.Under.forget (toMorphismProperty Q) ⊤ R) := by
+  refine .mk' _ fun (J : Type u) _ ↦ ?_
+  apply +allowSynthFailures Comma.forgetCreatesLimitsOfShapeOfClosed
+  have := hQp.isClosedUnderLimitsOfShape hQi R
+  exact inferInstanceAs <| (toMorphismProperty Q).underObj.IsClosedUnderLimitsOfShape _
+
+lemma RingHom.HasFiniteProducts.hasFiniteProducts (hQi : RespectsIso Q) (hQp : HasFiniteProducts Q)
+    (R : CommRingCat.{u}) :
+    Limits.HasFiniteProducts ((RingHom.toMorphismProperty Q).Under ⊤ R) := by
+  refine ⟨fun n ↦ ⟨fun D ↦ ?_⟩⟩
+  have := hQp.createsFiniteProductsForget hQi R
+  exact CategoryTheory.hasLimit_of_created D (Under.forget _ _ R)
+
+/-- If `Q` is stable under equalizers, the inclusion from the subcategory of `Under R` defined
+by `Q` creates equalizers. -/
+@[implicit_reducible]
+noncomputable def RingHom.HasEqualizers.createsLimitsWalkingParallelPair (hQi : RespectsIso Q)
+    (hQe : HasEqualizers Q) (R : CommRingCat.{u}) :
+    CreatesLimitsOfShape WalkingParallelPair
+      (MorphismProperty.Under.forget (toMorphismProperty Q) ⊤ R) := by
+  apply +allowSynthFailures Comma.forgetCreatesLimitsOfShapeOfClosed
+  exact hQe.isClosedUnderLimitsOfShape hQi _
+
+lemma RingHom.HasEqualizers.hasEqualizers (hQi : RespectsIso Q) (hQe : HasEqualizers Q)
+    (R : CommRingCat.{u}) :
+    Limits.HasEqualizers ((toMorphismProperty Q).Under ⊤ R) := by
+  refine ⟨fun D ↦ ?_⟩
+  have := hQe.createsLimitsWalkingParallelPair hQi R
+  exact hasLimit_of_created D (Under.forget _ _ R)
+
+namespace CommRingCat
+
+/-- If `Q` is stable under finite products and equalizers, the inclusion from the subcategory of
+`Under R` defined by `Q` creates finite limits. -/
+@[implicit_reducible]
+noncomputable def Under.createsFiniteLimitsForget (hQi : RingHom.RespectsIso Q)
+    (hQp : RingHom.HasFiniteProducts Q) (hQe : RingHom.HasEqualizers Q) (R : CommRingCat.{u}) :
+    CreatesFiniteLimits (Under.forget (RingHom.toMorphismProperty Q) ⊤ R) :=
+  letI := hQp.createsFiniteProductsForget hQi
+  letI := hQe.createsLimitsWalkingParallelPair hQi
+  createsFiniteLimitsOfCreatesEqualizersAndFiniteProducts _
+
+lemma Under.hasFiniteLimits (hQi : RingHom.RespectsIso Q)
+    (hQp : RingHom.HasFiniteProducts Q) (hQe : RingHom.HasEqualizers Q) (R : CommRingCat.{u}) :
+    HasFiniteLimits ((RingHom.toMorphismProperty Q).Under ⊤ R) :=
+  have := hQp.hasFiniteProducts hQi
+  have := hQe.hasEqualizers hQi
+  hasFiniteLimits_of_hasEqualizers_and_finite_products
+
+end CommRingCat