Merge master into nightly-testing

Author: mathlib-nightly-testing[bot]

Mathlib.lean

@@ -2469,6 +2469,7 @@ public import Mathlib.CategoryTheory.Adjunction.Limits
 public import Mathlib.CategoryTheory.Adjunction.Mates
 public import Mathlib.CategoryTheory.Adjunction.Opposites
 public import Mathlib.CategoryTheory.Adjunction.Parametrized
+public import Mathlib.CategoryTheory.Adjunction.ParametrizedLimits
 public import Mathlib.CategoryTheory.Adjunction.PartialAdjoint
 public import Mathlib.CategoryTheory.Adjunction.Quadruple
 public import Mathlib.CategoryTheory.Adjunction.Reflective
@@ -2567,6 +2568,7 @@ public import Mathlib.CategoryTheory.CommSq
 public import Mathlib.CategoryTheory.Comma.Arrow
 public import Mathlib.CategoryTheory.Comma.Basic
 public import Mathlib.CategoryTheory.Comma.CardinalArrow
+public import Mathlib.CategoryTheory.Comma.CatCommSq
 public import Mathlib.CategoryTheory.Comma.Final
 public import Mathlib.CategoryTheory.Comma.LocallySmall
 public import Mathlib.CategoryTheory.Comma.Over.Basic
@@ -4509,6 +4511,7 @@ public import Mathlib.Geometry.Convex.Cone.Simplicial
 public import Mathlib.Geometry.Convex.Cone.TensorProduct
 public import Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
 public import Mathlib.Geometry.Convex.ConvexSpace.Defs
+public import Mathlib.Geometry.Convex.ConvexSpace.Prod
 public import Mathlib.Geometry.Diffeology.Basic
 public import Mathlib.Geometry.Euclidean.Altitude
 public import Mathlib.Geometry.Euclidean.Angle.Bisector
@@ -6609,6 +6612,7 @@ public import Mathlib.RingTheory.LocalProperties.Semilocal
 public import Mathlib.RingTheory.LocalProperties.Submodule
 public import Mathlib.RingTheory.LocalRing.Basic
 public import Mathlib.RingTheory.LocalRing.Defs
+public import Mathlib.RingTheory.LocalRing.Etale
 public import Mathlib.RingTheory.LocalRing.Length
 public import Mathlib.RingTheory.LocalRing.LocalSubring
 public import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic

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

@@ -216,6 +216,11 @@ theorem mul_prod_eraseIdx {i} (hlen : i < l.length) (hcomm : ∀ a' ∈ l.take i
       hcomm a' (by rwa [take_eraseIdx_eq_take_of_le l i i (Nat.le_refl i)] at a'_mem)),
     insertIdx_eraseIdx_getElem hlen]
 
+@[to_additive (attr := simp)]
+theorem prod_filter_bne_one [BEq M] [LawfulBEq M] (l : List M) :
+    (l.filter (· != 1)).prod = l.prod := by
+  classical induction l <;> grind
+
 end Monoid
 
 section CommMonoid

Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean

@@ -85,19 +85,21 @@ noncomputable def unitIsoAux (F : C ⥤ AddCommGrpCat.{v}) [PreservesFiniteLimit
   letI : (F ⋙ forget AddCommGrpCat).Braided := .ofChosenFiniteProducts _
   letI : F.Monoidal := .ofChosenFiniteProducts _
   refine CommGrp.mkIso Multiplicative.toAdd.toIso (by
-    erw [Functor.mapCommGrp_obj_grp_one]
+    rw [Functor.obj.η_def X (F := F ⋙ forget AddCommGrpCat)]
     cat_disch) ?_
   dsimp [-Functor.comp_map, -ConcreteCategory.forget_map_eq_ofHom]
   have : F.Additive := Functor.additive_of_preserves_binary_products _
   simp only [Category.id_comp]
-  erw [Functor.mapCommGrp_obj_grp_mul]
-  erw [Functor.comp_map, F.map_add, Functor.Monoidal.μ_comp F (forget AddCommGrpCat) X X,
+  rw [Functor.obj.μ_def X (F := F ⋙ forget AddCommGrpCat), Preadditive.mul_def X,
+    Functor.comp_map, F.map_add,
+    Functor.Monoidal.μ_comp F (forget AddCommGrpCat) X X,
     Category.assoc, ← Functor.map_comp, Preadditive.comp_add, Functor.Monoidal.μ_fst,
     Functor.Monoidal.μ_snd]
   ext
-  simp only [TypeCat.Fun.toFun_apply, CategoryTheory.comp_apply, Equiv.toIso_hom_hom_apply,
-    Preadditive.commGrpEquivalence_functor_obj_X, Functor.comp_obj, types_tensorObj_def, hom_add,
-    tensor_apply, TypeCat.hom_ofHom, TypeCat.Fun.coe_mk, AddMonoidHom.add_apply]
+  -- `simp [types_tensorObj_def]` says
+  simp only [types_tensorObj_def, TypeCat.Fun.toFun_apply, CategoryTheory.comp_apply,
+    Equiv.toIso_hom_hom_apply, Functor.comp_obj, hom_add, tensor_apply, TypeCat.hom_ofHom,
+    TypeCat.Fun.coe_mk, AddMonoidHom.add_apply]
   rw [dsimp% [types_tensorObj_def, types_tensorUnit_def] μ_forget_apply]
   rfl
 

Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafification.lean

@@ -127,10 +127,9 @@ noncomputable def sheafificationAdjunction :
     { homEquiv := fun _ _ ↦ sheafificationHomEquiv α
       homEquiv_naturality_left_symm := fun {P₀ Q₀ N} f g ↦ by
         apply (SheafOfModules.toSheaf _).map_injective
-        rw [Functor.map_comp]
-        erw [toSheaf_map_sheafificationHomEquiv_symm,
-          toSheaf_map_sheafificationHomEquiv_symm α g]
-        rw [Functor.map_comp]
+        simp only [Functor.comp_obj, Functor.map_comp]
+        rw [toSheaf_map_sheafificationHomEquiv_symm α (f ≫ g),
+          toSheaf_map_sheafificationHomEquiv_symm α g, Functor.map_comp]
         apply (CategoryTheory.sheafificationAdjunction J
           AddCommGrpCat.{v}).homEquiv_naturality_left_symm
       homEquiv_naturality_right := fun {P₀ M N} f g ↦ by

Mathlib/Algebra/Homology/ShortComplex/ModuleCat.lean

@@ -240,4 +240,44 @@ lemma ModuleCat.shortComplex_shortExact (S : ShortComplex (ModuleCat.{v} R))
   mono_f := (ModuleCat.mono_iff_injective _).mpr inj
   epi_g := (ModuleCat.epi_iff_surjective _).mpr surj
 
+variable {M' N' L' : Type*} [AddCommGroup M'] [AddCommGroup N'] [AddCommGroup L']
+  [Module R M'] [Module R N'] [Module R L']
+
+variable (eM : M ≃ₗ[R] M') (eN : N ≃ₗ[R] N') (eL : L ≃ₗ[R] L') (f : M' →ₗ[R] N') (g : N' →ₗ[R] L')
+
+/--
+Suppose that `f` and `g` are linear maps that compose to zero, and that `eM`, `eN`, and `eL`
+indicated in the diagram below are linear equivalences to modules that all belong to the same
+universe. Then this is the short complex in `ModuleCat` given by the bottom row in the diagram.
+M --f--> N --g--> L
+|        |        |
+eM       eN       eL
+|        |        |
+v        v        v
+M'-----> N'-----> L'
+This complex is exact when we have `Function.Exact f g`, see
+`ModuleCat.shortComplexOfConj_exact`.
+-/
+abbrev ModuleCat.shortComplexOfConj (eq0 : g ∘ₗ f = 0) :
+    ShortComplex (ModuleCat.{v} R) :=
+  ModuleCat.shortComplexOfCompEqZero ((eN.symm.comp f).comp eM.toLinearMap)
+    (eL.symm.comp (g.comp eN.toLinearMap)) (by
+      ext x
+      simpa using LinearMap.congr_fun eq0 (eM x))
+
+private lemma exact_conj_of_exact (exact : Function.Exact f g) : Function.Exact
+    ((eN.symm.comp f).comp eM.toLinearMap) (eL.symm.comp (g.comp eN.toLinearMap)) := by
+  rwa [LinearEquiv.precomp_exact_iff_exact, LinearEquiv.postcomp_exact_iff_exact,
+    LinearEquiv.conj_symm_exact_iff_exact]
+
+lemma ModuleCat.shortComplexOfConj_exact (exact : Function.Exact f g) :
+    (ModuleCat.shortComplexOfConj eM eN eL f g exact.linearMap_comp_eq_zero).Exact :=
+  ModuleCat.shortComplex_exact _ (exact_conj_of_exact eM eN eL f g exact)
+
+lemma ModuleCat.shortComplexOfConj_shortExact (exact : Function.Exact f g)
+    (inj : Function.Injective f) (surj : Function.Surjective g) :
+    (ModuleCat.shortComplexOfConj eM eN eL f g exact.linearMap_comp_eq_zero).ShortExact := by
+  refine ModuleCat.shortComplex_shortExact _ (exact_conj_of_exact eM eN eL f g exact) ?_ ?_
+  all_goals simpa
+
 end

Mathlib/Algebra/Lie/Submodule.lean

@@ -73,9 +73,6 @@ instance : Zero (LieSubmodule R L M) :=
 instance : Inhabited (LieSubmodule R L M) :=
   ⟨0⟩
 
-instance (priority := high) coeSort : CoeSort (LieSubmodule R L M) (Type w) where
-  coe N := { x : M // x ∈ N }
-
 instance (priority := mid) coeSubmodule : CoeOut (LieSubmodule R L M) (Submodule R M) :=
   ⟨toSubmodule⟩
 

Mathlib/Algebra/Module/StablyFree/Basic.lean

@@ -13,8 +13,8 @@ public import Mathlib.RingTheory.Finiteness.Small
 # Stably free modules
 
 ## Main definition
-* `IsStablyFree`: A module `M` over a commutative ring `R` is called stably free if there exists a
-  finite free module `N` over `R` such that `M ⊕ N` is free.
+* `IsStablyFree`: A module `M` over a ring `R` is called stably free if there exists a finite free
+  `R`-module `N` such that `M ⊕ N` is free.
 -/
 
 public section
@@ -23,8 +23,8 @@ universe u v w
 
 namespace Module
 
-/-- A module `M` over a commutative ring `R` is called stably free if there exists a
-  finite free module `N` over `R` such that `M ⊕ N` is free.
+/-- A module `M` over a ring `R` is called stably free if there exists a finite free `R`-module `N`
+such that `M ⊕ N` is free.
 
 The underlying constructor is marked as private. The intended constructor of `IsStablyFree` is
 `IsStablyFree.of_free_prod`, and use `IsStablyFree.exist_free_prod` to extract the property from

Mathlib/Algebra/MvPolynomial/Equiv.lean

@@ -99,6 +99,25 @@ theorem uniqueAlgEquiv_symm_monomial [Unique σ] {d : σ →₀ ℕ} {r : R} :
       = MvPolynomial.monomial d r := by
   simp [MvPolynomial.monomial_eq]
 
+/-- The coefficient of `X ^ n` in `uniqueAlgEquiv R σ P` is the coefficient of the unique
+monomial of degree `n` in `P`. -/
+theorem coeff_uniqueAlgEquiv [Unique σ] (P : MvPolynomial σ R) (n : ℕ) :
+    (MvPolynomial.uniqueAlgEquiv R σ P : Polynomial R).coeff n =
+      coeff (Finsupp.single default n) P := by
+  induction P using induction_on' with
+  | monomial d r =>
+      rw [uniqueAlgEquiv_monomial, Finsupp.unique_single d]
+      simp [Polynomial.coeff_monomial, MvPolynomial.coeff_monomial]
+  | add P Q hP hQ =>
+      simpa using congrArg₂ (· + ·) hP hQ
+
+/-- The coefficient of a monomial in `(uniqueAlgEquiv R σ).symm P` is the coefficient of the
+corresponding univariate monomial in `P`. -/
+theorem coeff_uniqueAlgEquiv_symm [Unique σ] (P : Polynomial R) (d : σ →₀ ℕ) :
+    coeff d ((MvPolynomial.uniqueAlgEquiv R σ).symm P) = P.coeff (d default) := by
+  rw [Finsupp.unique_single d, ← coeff_uniqueAlgEquiv R, AlgEquiv.apply_symm_apply,
+    Finsupp.single_eq_same]
+
 /-- The algebra isomorphism between multivariable polynomials in a single variable and
 polynomials over the ground ring. -/
 @[deprecated uniqueAlgEquiv (since := "2026-04-15")]

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean

@@ -313,7 +313,7 @@ def homogeneousLocalizationToStalk (x : ProjectiveSpectrum.top 𝒜) (y : at x)
 
 lemma homogeneousLocalizationToStalk_stalkToFiberRingHom (x z) :
     homogeneousLocalizationToStalk 𝒜 x (stalkToFiberRingHom 𝒜 x z) = z := by
-  obtain ⟨U, hxU, s, rfl⟩ := (Proj.structureSheaf 𝒜).presheaf.germ_exist x z
+  obtain ⟨U, hxU, s, rfl⟩ := (Proj.structureSheaf 𝒜).presheaf.exists_germ_eq z
   change homogeneousLocalizationToStalk 𝒜 x ((stalkToFiberRingHom 𝒜 x).hom
       (((Proj.structureSheaf 𝒜).presheaf.germ U x hxU) s)) =
     ((Proj.structureSheaf 𝒜).presheaf.germ U x hxU) s

Mathlib/AlgebraicGeometry/Properties.lean

@@ -85,7 +85,7 @@ instance isReduced_stalk_of_isReduced [IsReduced X] (x : X) :
     _root_.IsReduced (X.presheaf.stalk x) := by
   constructor
   rintro g ⟨n, e⟩
-  obtain ⟨U, hxU, s, (rfl : (X.presheaf.germ U x hxU) s = g)⟩ := X.presheaf.germ_exist x g
+  obtain ⟨U, hxU, s, (rfl : (X.presheaf.germ U x hxU) s = g)⟩ := X.presheaf.exists_germ_eq g
   rw [← map_pow, ← map_zero (X.presheaf.germ _ x hxU).hom] at e
   obtain ⟨V, hxV, iU, iV, (e' : (X.presheaf.map iU.op) (s ^ n) = (X.presheaf.map iV.op) 0)⟩ :=
     X.presheaf.germ_eq x hxU hxU _ 0 e