Merge master into nightly-testing

Author: leanprover-community-mathlib4-bot

Mathlib.lean

@@ -585,6 +585,7 @@ public import Mathlib.Algebra.Homology.Homotopy
 public import Mathlib.Algebra.Homology.HomotopyCategory
 public import Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
 public import Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
+public import Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
 public import Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction
 public import Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
 public import Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor
@@ -1430,6 +1431,7 @@ public import Mathlib.AlgebraicTopology.SimplicialSet.Simplices
 public import Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
 public import Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
 public import Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
+public import Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits
 public import Mathlib.AlgebraicTopology.SingularHomology.Basic
 public import Mathlib.AlgebraicTopology.SingularSet
 public import Mathlib.AlgebraicTopology.TopologicalSimplex
@@ -2246,6 +2248,7 @@ public import Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
 public import Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
 public import Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
 public import Mathlib.CategoryTheory.Bicategory.Grothendieck
+public import Mathlib.CategoryTheory.Bicategory.InducedBicategory
 public import Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
 public import Mathlib.CategoryTheory.Bicategory.Kan.HasKan
 public import Mathlib.CategoryTheory.Bicategory.Kan.IsKan
@@ -2894,6 +2897,7 @@ public import Mathlib.CategoryTheory.Presentable.Basic
 public import Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
 public import Mathlib.CategoryTheory.Presentable.ColimitPresentation
 public import Mathlib.CategoryTheory.Presentable.Dense
+public import Mathlib.CategoryTheory.Presentable.Directed
 public import Mathlib.CategoryTheory.Presentable.Finite
 public import Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
 public import Mathlib.CategoryTheory.Presentable.Limits
@@ -2908,6 +2912,7 @@ public import Mathlib.CategoryTheory.Products.Unitor
 public import Mathlib.CategoryTheory.Quotient
 public import Mathlib.CategoryTheory.Quotient.Linear
 public import Mathlib.CategoryTheory.Quotient.Preadditive
+public import Mathlib.CategoryTheory.RepresentedBy
 public import Mathlib.CategoryTheory.Retract
 public import Mathlib.CategoryTheory.Shift.Adjunction
 public import Mathlib.CategoryTheory.Shift.Basic
@@ -5491,6 +5496,7 @@ public import Mathlib.Order.PrimeIdeal
 public import Mathlib.Order.PrimeSeparator
 public import Mathlib.Order.Prod.Lex.Hom
 public import Mathlib.Order.PropInstances
+public import Mathlib.Order.Quotient
 public import Mathlib.Order.Radical
 public import Mathlib.Order.Rel.GaloisConnection
 public import Mathlib.Order.RelClasses
@@ -5991,6 +5997,7 @@ public import Mathlib.RingTheory.Localization.Module
 public import Mathlib.RingTheory.Localization.NormTrace
 public import Mathlib.RingTheory.Localization.NumDen
 public import Mathlib.RingTheory.Localization.Pi
+public import Mathlib.RingTheory.Localization.Rat
 public import Mathlib.RingTheory.Localization.Submodule
 public import Mathlib.RingTheory.MatrixAlgebra
 public import Mathlib.RingTheory.MatrixPolynomialAlgebra

Mathlib/Algebra/Algebra/Basic.lean

@@ -156,6 +156,13 @@ abbrev semiringToRing (R : Type*) [CommRing R] [Semiring A] [Algebra R A] : Ring
     intCast_ofNat := fun z => by simp only [Int.cast_natCast, map_natCast]
     intCast_negSucc := fun z => by simp }
 
+/-- The `CommRing` structure on a `CommSemiring` induced by a ring morphism from a `CommRing`. -/
+abbrev _root_.RingHom.commSemiringToCommRing {R A : Type*} [CommRing R] [CommSemiring A]
+    (φ : R →+* A) : CommRing A :=
+  let _ : Algebra R A := RingHom.toAlgebra φ
+  { __ := Algebra.semiringToRing R
+    mul_comm := CommMonoid.mul_comm }
+
 instance {R : Type*} [Ring R] : Algebra (Subring.center R) R where
   algebraMap :=
   { toFun := Subtype.val

Mathlib/Algebra/Group/Pointwise/Set/Basic.lean

@@ -241,6 +241,16 @@ theorem inv_range {ι : Sort*} {f : ι → α} : (range f)⁻¹ = range fun i =>
   rw [← image_inv_eq_inv]
   exact (range_comp ..).symm
 
+@[to_additive (attr := simp)]
+theorem forall_inv_mem {p : α → Prop} : (∀ x, x⁻¹ ∈ s → p x) ↔ ∀ x ∈ s, p x⁻¹ := by
+  rw [← (Equiv.inv _).forall_congr_right]
+  simp
+
+@[to_additive (attr := simp)]
+theorem exists_inv_mem {p : α → Prop} : (∃ x, x⁻¹ ∈ s ∧ p x) ↔ ∃ x ∈ s, p x⁻¹ := by
+  rw [← (Equiv.inv _).exists_congr_right]
+  simp
+
 open MulOpposite
 
 @[to_additive]

Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean

@@ -704,6 +704,28 @@ def diff : Cocycle K K 1 :=
     simp only [Cochain.zero_v, δ_v 1 2 rfl _ p q hpq _ _ rfl rfl, Cochain.diff_v,
       HomologicalComplex.d_comp_d, smul_zero, add_zero])
 
+variable (L n) in
+/-- The inclusion `Cocycle K L n →+ Cochain K L n`. -/
+@[simps]
+def toCochainAddMonoidHom : Cocycle K L n →+ Cochain K L n where
+  toFun x := x
+  map_zero' := by simp
+  map_add' := by simp
+
+variable (L n) in
+/-- `Cocycle K L n` is the kernel of the differential on `HomComplex K L`. -/
+def isKernel (hm : n + 1 = m) :
+    IsLimit ((KernelFork.ofι (f := (HomComplex K L).d n m)
+      (AddCommGrpCat.ofHom (toCochainAddMonoidHom K L n))) (by cat_disch)) :=
+  Fork.IsLimit.mk _
+    (fun s ↦ AddCommGrpCat.ofHom
+      { toFun x := ⟨s.ι x, by
+          rw [mem_iff _ _ hm]
+          exact ConcreteCategory.congr_hom s.condition x⟩
+        map_zero' := by cat_disch
+        map_add' := by cat_disch })
+    (by cat_disch) (fun s l hl ↦ by ext : 3; simp [← hl])
+
 end Cocycle
 
 variable {F G}

Mathlib/Algebra/Homology/HomotopyCategory/HomComplexCohomology.lean

@@ -0,0 +1,163 @@
+/-
+Copyright (c) 2025 Joël Riou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joël Riou
+-/
+module
+
+public import Mathlib.Algebra.Homology.ShortComplex.Ab
+public import Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
+public import Mathlib.Algebra.Homology.HomotopyCategory.Shift
+
+/-!
+# Cohomology of the hom complex
+
+Given `ℤ`-indexed cochain complexes `K` and `L`, and `n : ℤ`, we introduce
+a type `HomComplex.CohomologyClass K L n` which is the quotient
+of `HomComplex.Cocycle K L n` which identifies cohomologous cocycles.
+We construct this type of cohomology classes instead of using
+the homology API because `Cochain K L` can be considered both
+as a complex of abelian groups or as a complex of `R`-modules
+when the category is `R`-linear. This also complements the API
+around `HomComplex` which is centered on terms in types
+`Cochain` or `Cocycle` which are suitable for computations.
+
+-/
+
+@[expose] public section
+
+assert_not_exists TwoSidedIdeal
+
+open CategoryTheory Category Limits Preadditive
+
+universe v u
+
+variable {C : Type u} [Category.{v} C] [Preadditive C] {R : Type*} [Ring R] [Linear R C]
+
+namespace CochainComplex
+
+variable (K L : CochainComplex C ℤ) (n m p : ℤ)
+
+namespace HomComplex
+
+/-- The subgroup of `Cocycle K L n` consisting of coboundaries. -/
+def coboundaries : AddSubgroup (Cocycle K L n) where
+  carrier := setOf (fun α ↦ ∃ (m : ℤ) (hm : m + 1 = n) (β : Cochain K L m), δ m n β = α)
+  zero_mem' := ⟨n - 1, by simp, 0, by simp⟩
+  add_mem' := by
+    rintro α₁ α₂ ⟨m, hm, β₁, hβ₁⟩ ⟨m', hm', β₂, hβ₂⟩
+    obtain rfl : m = m' := by cutsat
+    exact ⟨m, hm, β₁ + β₂, by aesop⟩
+  neg_mem' := by
+    rintro α ⟨m, hm, β, hβ⟩
+    exact ⟨m, hm, -β, by aesop⟩
+
+/-- The type of cohomology classes of degree `n` in the complex of morphisms
+from `K` to `L`. -/
+def CohomologyClass : Type v := Cocycle K L n ⧸ coboundaries K L n
+
+instance : AddCommGroup (CohomologyClass K L n) :=
+  inferInstanceAs (AddCommGroup (Cocycle K L n ⧸ coboundaries K L n))
+
+namespace CohomologyClass
+
+variable {K L n}
+
+/-- The cohomology class of a cocycle. -/
+def mk (x : Cocycle K L n) : CohomologyClass K L n :=
+  Quotient.mk _ x
+
+lemma mk_surjective : Function.Surjective (mk : Cocycle K L n → _) :=
+  Quotient.mk_surjective
+
+variable (K L n) in
+@[simp]
+lemma mk_zero :
+    mk (0 : Cocycle K L n) = 0 := rfl
+
+@[simp]
+lemma mk_add (x y : Cocycle K L n) :
+    mk (x + y) = mk x + mk y := rfl
+
+@[simp]
+lemma mk_sub (x y : Cocycle K L n) :
+    mk (x - y) = mk x - mk y := rfl
+
+@[simp]
+lemma mk_neg (x : Cocycle K L n) :
+    mk (-x) = - mk x := rfl
+
+lemma mk_eq_zero_iff (x : Cocycle K L n) :
+    mk x = 0 ↔ x ∈ coboundaries K L n :=
+  QuotientAddGroup.eq_zero_iff x
+
+variable (K L n) in
+/-- The projection map `Cocycle K L n →+ CohomologyClass K L n`. -/
+@[simps]
+def mkAddMonoidHom : Cocycle K L n →+ CohomologyClass K L n where
+  toFun := mk
+  map_zero' := by simp
+  map_add' := by simp
+
+section
+
+variable {G : Type*} [AddCommGroup G]
+  (f : Cocycle K L n →+ G) (hf : coboundaries K L n ≤ f.ker)
+
+/-- Constructor for additive morphisms from `CohomologyClass K L n`. -/
+def descAddMonoidHom :
+    CohomologyClass K L n →+ G :=
+  QuotientAddGroup.lift _ f hf
+
+@[simp]
+lemma descAddMonoidHom_cohomologyClass (x : Cocycle K L n) :
+    descAddMonoidHom f hf (mk x) = f x := rfl
+
+end
+
+end CohomologyClass
+
+/-- `CohomologyClass K L m` identifies to the cohomology of the complex `HomComplex K L`
+in degree `m`. -/
+@[simps]
+def leftHomologyData' (hm : n + 1 = m) (hp : m + 1 = p) :
+    ((HomComplex K L).sc' n m p).LeftHomologyData where
+  K := .of (Cocycle K L m)
+  H := .of (CohomologyClass K L m)
+  i := AddCommGrpCat.ofHom (Cocycle.toCochainAddMonoidHom K L m)
+  π := AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)
+  wi := by cat_disch
+  hi := Cocycle.isKernel K L _ _ hp
+  wπ := by
+    ext x
+    dsimp
+    rw [CohomologyClass.mk_eq_zero_iff]
+    exact ⟨n, hm, x, rfl⟩
+  hπ :=
+    Cofork.IsColimit.mk _
+      (fun s ↦ AddCommGrpCat.ofHom (CohomologyClass.descAddMonoidHom s.π.hom
+        (by
+          rintro ⟨_, _⟩ ⟨q, hq, y, rfl⟩
+          obtain rfl : n = q := by cutsat
+          simpa only [zero_comp] using ConcreteCategory.congr_hom s.condition y)))
+      (fun s ↦ rfl)
+      (fun s l hl ↦ by
+        ext x
+        obtain ⟨y, rfl⟩ := x.mk_surjective
+        simpa using ConcreteCategory.congr_hom hl y)
+
+/-- `CohomologyClass K L m` identifies to the cohomology of the complex `HomComplex K L`
+in degree `m`. -/
+@[simps!]
+noncomputable def leftHomologyData :
+    ((HomComplex K L).sc n).LeftHomologyData :=
+  leftHomologyData' K L _ n _ (by simp) (by simp)
+
+/-- The homology of `HomComplex K L` in degree `n` identifies to `CohomologyClass K L n`. -/
+noncomputable def homologyAddEquiv :
+    (HomComplex K L).homology n ≃+ CohomologyClass K L n :=
+  (leftHomologyData K L n).homologyIso.addCommGroupIsoToAddEquiv
+
+end HomComplex
+
+end CochainComplex

Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean

@@ -68,6 +68,9 @@ variable [LE α]
 theorem mul_le_mul_right [MulLeftMono α] {b c : α} (bc : b ≤ c) (a : α) : a * b ≤ a * c :=
   CovariantClass.elim _ bc
 
+@[deprecated (since := "2025-11-27")]
+alias mul_le_mul_left' := mul_le_mul_right
+
 @[to_additive le_of_add_le_add_left]
 theorem le_of_mul_le_mul_left' [MulLeftReflectLE α] {a b c : α}
     (bc : a * b ≤ a * c) :
@@ -78,6 +81,9 @@ theorem le_of_mul_le_mul_left' [MulLeftReflectLE α] {a b c : α}
 theorem mul_le_mul_left [i : MulRightMono α] {b c : α} (bc : b ≤ c) (a : α) : b * a ≤ c * a :=
   i.elim a bc
 
+@[deprecated (since := "2025-11-27")]
+alias mul_le_mul_right' := mul_le_mul_left
+
 @[to_additive le_of_add_le_add_right]
 theorem le_of_mul_le_mul_right' [i : MulRightReflectLE α] {a b c : α}
     (bc : b * a ≤ c * a) :

Mathlib/Algebra/Polynomial/Bivariate.lean

@@ -293,7 +293,7 @@ lemma equivMvPolynomial_symm_X_1 : (equivMvPolynomial R).symm (.X 1) = X := by
 lemma equivMvPolynomial_symm_C (a : R) : (equivMvPolynomial R).symm (.C a) = C (C a) := by
   simp [equivMvPolynomial]
 
-lemma Polynomial.Bivariate.pderiv_zero_equivMvPolynomial {R : Type*} [CommRing R] (p : R[X][Y]) :
+lemma pderiv_zero_equivMvPolynomial {R : Type*} [CommRing R] (p : R[X][Y]) :
     (equivMvPolynomial R p).pderiv 0 = equivMvPolynomial R
       (PolynomialModule.equivPolynomialSelf (derivative'.mapCoeffs p)) := by
   induction p using Polynomial.induction_on' with
@@ -305,7 +305,7 @@ lemma Polynomial.Bivariate.pderiv_zero_equivMvPolynomial {R : Type*} [CommRing R
     simp_rw [← Polynomial.C_mul_X_pow_eq_monomial]
     simp [map_nsmul]
 
-lemma Polynomial.Bivariate.pderiv_one_equivMvPolynomial (p : R[X][Y]) :
+lemma pderiv_one_equivMvPolynomial (p : R[X][Y]) :
     (equivMvPolynomial R p).pderiv 1 = equivMvPolynomial R (derivative p) := by
   induction p using Polynomial.induction_on' with
   | add p q _ _ => aesop

Mathlib/Algebra/Polynomial/Coeff.lean

@@ -148,7 +148,7 @@ theorem coeff_C_mul_X_pow (x : R) (k n : ℕ) :
 theorem coeff_C_mul_X (x : R) (n : ℕ) : coeff (C x * X : R[X]) n = if n = 1 then x else 0 := by
   rw [← pow_one X, coeff_C_mul_X_pow]
 
-@[simp]
+@[simp, grind =]
 theorem coeff_C_mul (p : R[X]) : coeff (C a * p) n = a * coeff p n := by
   rcases p with ⟨p⟩
   simp_rw [← monomial_zero_left, ← ofFinsupp_single, ← ofFinsupp_mul, coeff]
@@ -182,7 +182,7 @@ theorem coeff_mul_C (p : R[X]) (n : ℕ) (a : R) : coeff (p * C a) n = coeff p n
 @[simp] lemma coeff_intCast_mul [Ring S] {p : S[X]} {a : ℤ} {k : ℕ} :
     coeff ((a : S[X]) * p) k = a * coeff p k := coeff_C_mul _
 
-@[simp]
+@[simp, grind =]
 theorem coeff_X_pow (k n : ℕ) : coeff (X ^ k : R[X]) n = if n = k then 1 else 0 := by
   simp only [one_mul, map_one, ← coeff_C_mul_X_pow]
 
@@ -225,7 +225,7 @@ end Fewnomials
 theorem coeff_mul_X_pow (p : R[X]) (n d : ℕ) :
     coeff (p * Polynomial.X ^ n) (d + n) = coeff p d := by
   rw [coeff_mul, Finset.sum_eq_single (d, n), coeff_X_pow, if_pos rfl, mul_one]
-  all_goals grind [mem_antidiagonal, coeff_X_pow, mul_zero]
+  all_goals grind [mem_antidiagonal, mul_zero]
 
 @[simp]
 theorem coeff_X_pow_mul (p : R[X]) (n d : ℕ) :

Mathlib/Algebra/Polynomial/Reverse.lean

@@ -58,7 +58,7 @@ def revAt (N : ℕ) : Function.Embedding ℕ ℕ where
 theorem revAtFun_eq (N i : ℕ) : revAtFun N i = revAt N i :=
   rfl
 
-@[simp]
+@[simp, grind =]
 theorem revAt_invol {N i : ℕ} : (revAt N) (revAt N i) = i :=
   revAtFun_invol
 
@@ -93,7 +93,7 @@ theorem reflect_support (N : ℕ) (f : R[X]) :
   ext1
   simp only [reflect, support_ofFinsupp, support_embDomain, Finset.mem_map, Finset.mem_image]
 
-@[simp]
+@[simp, grind =]
 theorem coeff_reflect (N : ℕ) (f : R[X]) (i : ℕ) : coeff (reflect N f) i = f.coeff (revAt N i) := by
   rcases f with ⟨f⟩
   simp only [reflect, coeff]
@@ -122,14 +122,8 @@ theorem reflect_C_mul (f : R[X]) (r : R) (N : ℕ) : reflect N (C r * f) = C r *
 
 theorem reflect_C_mul_X_pow (N n : ℕ) {c : R} : reflect N (C c * X ^ n) = C c * X ^ revAt N n := by
   ext
-  rw [reflect_C_mul, coeff_C_mul, coeff_C_mul, coeff_X_pow, coeff_reflect]
-  split_ifs with h
-  · rw [h, revAt_invol, coeff_X_pow_self]
-  · rw [notMem_support_iff.mp]
-    intro a
-    rw [← one_mul (X ^ n), ← C_1] at a
-    apply h
-    rw [← mem_support_C_mul_X_pow a, revAt_invol]
+  grind
+
 
 @[simp]
 theorem reflect_C (r : R) (N : ℕ) : reflect N (C r) = C r * X ^ N := by

Mathlib/Algebra/Ring/Subring/Basic.lean

@@ -925,6 +925,19 @@ theorem ofLeftInverse_symm_apply {g : S → R} {f : R →+* S} (h : Function.Lef
 def subringMap (e : R ≃+* S) : s ≃+* s.map e.toRingHom :=
   e.subsemiringMap s.toSubsemiring
 
+/-- A ring isomorphism `e : R ≃+* S` descends to subrings `s' ≃+* s` provided
+`x ∈ s' ↔ e x ∈ s`. -/
+@[simps!]
+def restrict {R : Type u} {S : Type v} [NonAssocSemiring R] [NonAssocSemiring S]
+    {σR : Type*} {σS : Type*} [SetLike σR R] [SetLike σS S] [SubsemiringClass σR R]
+    [SubsemiringClass σS S] (e : R ≃+* S) (s' : σR) (s : σS) (h : ∀ x, x ∈ s' ↔ e x ∈ s) :
+    s' ≃+* s where
+  __ := RingHom.restrict e _ _ fun _ ↦ (h _).1
+  invFun := RingHom.restrict e.symm _ _ fun y hy ↦ by
+    obtain ⟨x, rfl⟩ := e.surjective y; simp [(h _).2 hy]
+  left_inv y := by simp [← Subtype.val_inj]
+  right_inv x := by simp [← Subtype.val_inj]
+
 end RingEquiv
 
 namespace Subring