Sync upstream mathlib4 (2026-05-11, +30 commits)

Mathlib.lean

@@ -635,6 +635,7 @@ public import Mathlib.Algebra.Homology.HomotopyCategory.KInjective
 public import Mathlib.Algebra.Homology.HomotopyCategory.KProjective
 public import Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
 public import Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
+public import Mathlib.Algebra.Homology.HomotopyCategory.Plus
 public import Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
 public import Mathlib.Algebra.Homology.HomotopyCategory.Shift
 public import Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
@@ -654,6 +655,7 @@ public import Mathlib.Algebra.Homology.Localization
 public import Mathlib.Algebra.Homology.ModelCategory.Lifting
 public import Mathlib.Algebra.Homology.Monoidal
 public import Mathlib.Algebra.Homology.Opposite
+public import Mathlib.Algebra.Homology.Precylinder
 public import Mathlib.Algebra.Homology.QuasiIso
 public import Mathlib.Algebra.Homology.Refinements
 public import Mathlib.Algebra.Homology.ShortComplex.Ab
@@ -812,6 +814,7 @@ public import Mathlib.Algebra.Module.SnakeLemma
 public import Mathlib.Algebra.Module.SpanRank
 public import Mathlib.Algebra.Module.SpanRankOperations
 public import Mathlib.Algebra.Module.StablyFree.Basic
+public import Mathlib.Algebra.Module.StablyFree.FreeOfInvertible
 public import Mathlib.Algebra.Module.Submodule.Basic
 public import Mathlib.Algebra.Module.Submodule.Bilinear
 public import Mathlib.Algebra.Module.Submodule.Defs
@@ -2972,6 +2975,7 @@ public import Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
 public import Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor
 public import Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives
 public import Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions
+public import Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
 public import Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived
 public import Mathlib.CategoryTheory.Localization.Equivalence
 public import Mathlib.CategoryTheory.Localization.FiniteProducts
@@ -4495,6 +4499,8 @@ public import Mathlib.Geometry.Convex.Cone.DualFinite
 public import Mathlib.Geometry.Convex.Cone.Pointed
 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.Diffeology.Basic
 public import Mathlib.Geometry.Euclidean.Altitude
 public import Mathlib.Geometry.Euclidean.Angle.Bisector
@@ -4895,8 +4901,6 @@ public import Mathlib.LinearAlgebra.Complex.FiniteDimensional
 public import Mathlib.LinearAlgebra.Complex.Module
 public import Mathlib.LinearAlgebra.Complex.Orientation
 public import Mathlib.LinearAlgebra.Contraction
-public import Mathlib.LinearAlgebra.ConvexSpace
-public import Mathlib.LinearAlgebra.ConvexSpace.AffineSpace
 public import Mathlib.LinearAlgebra.Countable
 public import Mathlib.LinearAlgebra.CrossProduct
 public import Mathlib.LinearAlgebra.DFinsupp

Mathlib/Algebra/Algebra/Tower.lean

@@ -76,6 +76,10 @@ def lsmul : A →ₐ[R] Module.End B M where
 @[simp]
 theorem lsmul_coe (a : A) : (lsmul R B M a : M → M) = (a • ·) := rfl
 
+lemma lsmul_apply (a : A) (m : M) : lsmul R B M a m = a • m := rfl
+
+lemma lsmul_eq_smul_one (a : A) : lsmul R R M a = a • 1 := rfl
+
 end Algebra
 
 namespace IsScalarTower

Mathlib/Algebra/Category/Grp/ForgetCorepresentable.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.Category.Grp.Basic
 public import Mathlib.CategoryTheory.Yoneda
+public import Mathlib.Algebra.Category.Grp.Preadditive
 
 /-!
 # The forget functor is corepresentable
@@ -79,3 +80,14 @@ instance AddGrpCat.forget_isCorepresentable :
 instance AddCommGrpCat.forget_isCorepresentable :
     (forget AddCommGrpCat.{u}).IsCorepresentable :=
   Functor.IsCorepresentable.mk' AddCommGrpCat.coyonedaObjIsoForget
+
+theorem uliftZMultiplesHom_apply_add (G : Type u) [AddCommGroup G] (x y : G) :
+    uliftZMultiplesHom G (x + y) = uliftZMultiplesHom G x + uliftZMultiplesHom G y := by
+  ext
+  simp_all only [uliftZMultiplesHom_apply_apply, smul_add, AddMonoidHom.add_apply]
+
+/-- The additive equivalence `(ℤ ⟶ G) ≃+ G` -/
+@[simps!]
+def AddCommGrpCat.uliftZMultiplesAddEquiv (G : AddCommGrpCat) : (of (ULift ℤ) ⟶ G) ≃+ G :=
+  AddCommGrpCat.homAddEquiv.trans
+    (AddEquiv.mk' (uliftZMultiplesHom G) (uliftZMultiplesHom_apply_add G)).symm

Mathlib/Algebra/GCDMonoid/FinsetLemmas.lean

@@ -9,6 +9,7 @@ public import Mathlib.Algebra.GCDMonoid.Finset
 public import Mathlib.Algebra.GCDMonoid.Nat
 public import Mathlib.Data.Nat.GCD.Basic
 public import Mathlib.RingTheory.Coprime.Lemmas
+public import Mathlib.Data.Nat.Factorization.Basic
 
 /-!
 # `Finset.lcm` lemmas
@@ -36,6 +37,14 @@ theorem lcm_eq_prod {s : Finset ι} {f : ι → ℕ} (h : Set.Pairwise s <| Nat.
   rw [show Nat.Coprime = IsRelPrime by ext; exact Nat.coprime_iff_isRelPrime] at h
   exact associated_lcm_prod h |>.eq_of_normalized (normalize_eq _) (normalize_eq _)
 
+/-- An analogue of `Nat.factorization_lcm` for `Finset.lcm`. -/
+theorem factorization_lcm {f : ι → ℕ} {s : Finset ι} (hf : ∀ k ∈ s, f k ≠ 0) (p : ℕ) :
+    (s.lcm f).factorization p = s.sup fun a ↦ (f a).factorization p := by
+  classical
+  induction s using Finset.induction with
+  | empty => simp
+  | insert _ _ _ _ => simp_all [lcm_eq_nat_lcm, Nat.factorization_lcm]
+
 namespace Rat
 
 theorem den_sum_dvd_lcm_den {ι : Type*} (s : Finset ι) (f : ι → ℚ) :

Mathlib/Algebra/Homology/HomologySequenceLemmas.lean

@@ -32,12 +32,12 @@ for `φ.τ₁` and `φ.τ₂` shall also be obtained (TODO).
 
 open CategoryTheory ComposableArrows Abelian
 
-namespace HomologicalComplex
-
 variable {C ι : Type*} [Category* C] [Abelian C] {c : ComplexShape ι}
   {S S₁ S₂ : ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂)
   (hS₁ : S₁.ShortExact) (hS₂ : S₂.ShortExact)
 
+namespace HomologicalComplex
+
 namespace HomologySequence
 
 /-- The morphism `snakeInput hS₁ i j hij ⟶ snakeInput hS₂ i j hij` induced by
@@ -176,3 +176,62 @@ lemma quasiIso_τ₃ (h₁ : QuasiIso φ.τ₁) (h₂ : QuasiIso φ.τ₂) :
 end HomologySequence
 
 end HomologicalComplex
+
+namespace CategoryTheory.ShortComplex.ShortExact
+
+open HomologicalComplex Limits
+
+lemma exactAt_X₁ (hS : S.ShortExact) (j : ι)
+    (h₁ : Mono (HomologicalComplex.homologyMap S.g j) := by infer_instance)
+    (h₂ : ∀ (i : ι), c.Rel i j → Epi (HomologicalComplex.homologyMap S.g i) := by infer_instance) :
+    S.X₁.ExactAt j := by
+  rw [exactAt_iff_isZero_homology]
+  by_cases! hj : ∃ i, c.Rel i j
+  · obtain ⟨i, hij⟩ := hj
+    have := h₂ i hij
+    apply (hS.homology_exact₁ i j hij).isZero_X₂
+    · simp [← cancel_epi (HomologicalComplex.homologyMap S.g i)]
+    · simp [← cancel_mono (HomologicalComplex.homologyMap S.g j),
+        ← HomologicalComplex.homologyMap_comp]
+  · have := hS.mono_f
+    have := HomologicalComplex.mono_homologyMap_of_mono_of_not_rel S.f j hj
+    rw [IsZero.iff_id_eq_zero,
+      ← cancel_mono (HomologicalComplex.homologyMap S.f j),
+      ← cancel_mono (HomologicalComplex.homologyMap S.g j)]
+    simp [← HomologicalComplex.homologyMap_comp]
+
+lemma exactAt_X₂ (hS : S.ShortExact) (i : ι) (h₁ : S.X₁.ExactAt i) (h₃ : S.X₃.ExactAt i) :
+    S.X₂.ExactAt i := by
+  rw [exactAt_iff_isZero_homology] at h₁ h₃ ⊢
+  exact (hS.homology_exact₂ i).isZero_X₂ (h₁.eq_of_src _ _) (h₃.eq_of_tgt _ _)
+
+lemma exactAt_X₃ (hS : S.ShortExact) (i : ι)
+    (h₁ : Epi (HomologicalComplex.homologyMap S.f i) := by infer_instance)
+    (h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j) := by infer_instance) :
+    S.X₃.ExactAt i := by
+  rw [exactAt_iff_isZero_homology]
+  by_cases! hi : ∃ j, c.Rel i j
+  · obtain ⟨j, hij⟩ := hi
+    have := h₂ j hij
+    apply (hS.homology_exact₃ i j hij).isZero_X₂
+    · simp [← cancel_epi (HomologicalComplex.homologyMap S.f i),
+        ← HomologicalComplex.homologyMap_comp]
+    · simp [← cancel_mono (HomologicalComplex.homologyMap S.f j)]
+  · have := hS.epi_g
+    have := HomologicalComplex.epi_homologyMap_of_epi_of_not_rel S.g i hi
+    rw [IsZero.iff_id_eq_zero,
+      ← cancel_epi (HomologicalComplex.homologyMap S.g i),
+      ← cancel_epi (HomologicalComplex.homologyMap S.f i)]
+    simp [← HomologicalComplex.homologyMap_comp]
+
+lemma acyclic_X₁ (hS : S.ShortExact) (hg : _root_.QuasiIso S.g) : S.X₁.Acyclic :=
+  fun j ↦ hS.exactAt_X₁ j
+
+lemma acyclic_X₂ (hS : S.ShortExact) (h₁ : S.X₁.Acyclic) (h₃ : S.X₃.Acyclic) :
+    S.X₂.Acyclic :=
+  fun i ↦ hS.exactAt_X₂ i (h₁ _) (h₃ _)
+
+lemma acyclic_X₃ (hS : S.ShortExact) (h : _root_.QuasiIso S.f) : S.X₃.Acyclic :=
+  fun i ↦ hS.exactAt_X₃ i
+
+end CategoryTheory.ShortComplex.ShortExact