Trigger CI for leanprover-community/batteries#1811

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

Mathlib/Algebra/Group/Submonoid/Operations.lean

@@ -867,6 +867,11 @@ theorem submonoidMap_surjective (f : M →* N) (M' : Submonoid M) :
   rintro ⟨_, x, hx, rfl⟩
   exact ⟨⟨x, hx⟩, rfl⟩
 
+@[to_additive (attr := grind inj)]
+theorem submonoidMap_injective {f : M →* N} (hf : Injective f) (M' : Submonoid M) :
+    Injective (f.submonoidMap M') := by
+  grind [Injective, submonoidMap_apply_coe]
+
 end MonoidHom
 
 namespace Submonoid

Mathlib/Algebra/Homology/ExactSequence.lean

@@ -319,6 +319,11 @@ lemma exact_of_δlast {n : ℕ} (S : ComposableArrows C (n + 2))
   rw [exact_iff_δlast]
   constructor <;> assumption
 
+theorem natAddLEFunctor_obj_exact {n k l : ℕ} (h : k + l ≤ n) {R : ComposableArrows C n}
+    (hR : R.Exact) :
+    ((natAddLEFunctor h).obj R).Exact :=
+  ⟨⟨fun i _ => hR.1.1 (k + i)⟩, fun i _ => hR.exact (k + i)⟩
+
 lemma Exact.isIso_map' {C : Type*} [Category* C] [Preadditive C]
     [Balanced C] {n : ℕ} {S : ComposableArrows C n} (hS : S.Exact) (k : ℕ) (hk : k + 3 ≤ n)
     (h₀ : S.map' k (k + 1) = 0) (h₁ : S.map' (k + 2) (k + 3) = 0) :

Mathlib/Algebra/Lie/InvariantForm.lean

@@ -202,7 +202,7 @@ theorem isSemisimple_of_nondegenerate : IsSemisimple K L := by
   intro J hJ hJI
   rw [← lie_eq_self_of_isAtom_of_nonabelian J hJ (hL J hJ), lieIdeal_oper_eq_span, lieSpan_le]
   rintro _ ⟨x, y, rfl⟩
-  simp only [orthogonal_carrier, Φ.isOrtho_def, Set.mem_setOf_eq]
+  simp only [orthogonal_carrier, LinearMap.IsOrtho, Set.mem_setOf_eq]
   intro z hz
   rw [← neg_eq_zero, ← hΦ_inv]
   suffices ⁅(x : L), z⁆ = 0 by simp only [this, map_zero, LinearMap.zero_apply]

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/Submodule/Ker.lean

@@ -171,6 +171,8 @@ variable {f : M →ₛₗ[τ₁₂] M₂}
 
 open Submodule
 
+@[simp] theorem ker_neg (f : M →ₛₗ[τ₁₂] M₂) : (-f).ker = f.ker := by ext; simp
+
 theorem ker_toAddSubgroup (f : M →ₛₗ[τ₁₂] M₂) : (ker f).toAddSubgroup = f.toAddMonoidHom.ker :=
   rfl
 

Mathlib/Algebra/Module/Submodule/Map.lean

@@ -649,7 +649,10 @@ theorem submoduleComap_surjective_of_surjective (f : M →ₗ[R] M₁) (q : Subm
 /-- A linear map between two modules restricts to a linear map from any submodule p of the
 domain onto the image of that submodule.
 
-This is the linear version of `AddMonoidHom.addSubmonoidMap` and `AddMonoidHom.addSubgroupMap`. -/
+This is the linear version of `AddMonoidHom.addSubmonoidMap` and `AddMonoidHom.addSubgroupMap`.
+
+TODO: Consider making this an `abbrev`, dropping its API, and renaming to something like
+`restrictSubmodule`. -/
 def submoduleMap (f : M →ₗ[R] M₁) (p : Submodule R M) : p →ₗ[R] p.map f :=
   f.restrict fun x hx ↦ Submodule.mem_map.mpr ⟨x, hx, rfl⟩
 
@@ -660,6 +663,11 @@ theorem submoduleMap_coe_apply (f : M →ₗ[R] M₁) {p : Submodule R M} (x : p
 theorem submoduleMap_surjective (f : M →ₗ[R] M₁) (p : Submodule R M) :
     Function.Surjective (f.submoduleMap p) := f.toAddMonoidHom.addSubmonoidMap_surjective _
 
+@[grind inj]
+theorem submoduleMap_injective {f : M →ₗ[R] M₁} (hf : Injective f) (p : Submodule R M) :
+    Injective (f.submoduleMap p) :=
+  f.toAddMonoidHom.addSubmonoidMap_injective hf _
+
 variable [Semiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {σ₂₁ : R₂ →+* R}
 
 open Submodule

Mathlib/CategoryTheory/Abelian/DiagramLemmas/Four.lean

@@ -136,8 +136,8 @@ include hR₁ hR₂
 
 /-- The five lemma. -/
 theorem isIso_of_epi_of_isIso_of_isIso_of_mono (h₀ : Epi (app' φ 0)) (h₁ : IsIso (app' φ 1))
-    (h₂ : IsIso (app' φ 3)) (h₃ : Mono (app' φ 4)) : IsIso (app' φ 2) := by
-  dsimp at h₀ h₁ h₂ h₃
+    (h₃ : IsIso (app' φ 3)) (h₄ : Mono (app' φ 4)) : IsIso (app' φ 2) := by
+  dsimp at h₀ h₁ h₃ h₄
   have : Mono (app' φ 2) := by
     apply mono_of_epi_of_mono_of_mono (δlastFunctor.map φ) (R₁.exact_iff_δlast.1 hR₁).1
       (R₂.exact_iff_δlast.1 hR₂).1 <;> dsimp <;> infer_instance
@@ -148,6 +148,61 @@ theorem isIso_of_epi_of_isIso_of_isIso_of_mono (h₀ : Epi (app' φ 0)) (h₁ :
 
 end Five
 
+section Four
+
+variable {n k : ℕ} (h : k + 3 ≤ n) {R₁ R₂ : ComposableArrows C n}
+    (hR₁ : R₁.Exact) (hR₂ : R₂.Exact) (φ : R₁ ⟶ R₂)
+
+include hR₁ hR₂ in
+/-- Variant of the first 4-lemma for complexes of any size -/
+theorem mono_of_epi_of_mono_of_mono'' (k₀ k₁ k₂ k₃ : ℕ)
+    (hk₀ : k₀ = k) (hk₁ : k₁ = k + 1)
+    (hk₂ : k₂ = k + 2) (hk₃ : k₃ = k + 3)
+    (h₀ : Epi (app' φ k₀)) (h₁ : Mono (app' φ k₁))
+    (h₃ : Mono (app' φ k₃)) : Mono (app' φ k₂) := by
+  subst_vars
+  change Epi (app' φ (k₀ + 0)) at h₀
+  rw [← natAddLEFunctor_app' h] at h₀ h₁ h₃ ⊢
+  exact mono_of_epi_of_mono_of_mono _ (natAddLEFunctor_obj_exact h hR₁)
+    (natAddLEFunctor_obj_exact h hR₂) h₀ h₁ h₃
+
+include hR₁ hR₂ in
+/-- Variant of the second 4-lemma for complexes of any size -/
+theorem epi_of_epi_of_epi_of_mono'' (k₀ k₁ k₂ k₃ : ℕ)
+    (hk₀ : k₀ = k) (hk₁ : k₁ = k + 1)
+    (hk₂ : k₂ = k + 2) (hk₃ : k₃ = k + 3)
+    (h₀ : Epi (app' φ k₀)) (h₂ : Epi (app' φ k₂))
+    (h₃ : Mono (app' φ k₃)) : Epi (app' φ k₁) := by
+  subst_vars
+  change Epi (app' φ (k₀ + 0)) at h₀
+  rw [← natAddLEFunctor_app' h] at h₀ h₂ h₃ ⊢
+  exact epi_of_epi_of_epi_of_mono _ (natAddLEFunctor_obj_exact h hR₁)
+    (natAddLEFunctor_obj_exact h hR₂) h₀ h₂ h₃
+
+end Four
+
+section Five
+
+variable {n k : ℕ} (h : k + 4 ≤ n) {R₁ R₂ : ComposableArrows C n}
+    (hR₁ : R₁.Exact) (hR₂ : R₂.Exact) (φ : R₁ ⟶ R₂)
+
+include hR₁ hR₂ in
+/-- Variant of the 5-lemma for complexes of any size -/
+theorem isIso_of_epi_of_isIso_of_isIso_of_mono' (k₀ k₁ k₂ k₃ k₄ : ℕ)
+    (hk₀ : k₀ = k) (hk₁ : k₁ = k + 1)
+    (hk₂ : k₂ = k + 2) (hk₃ : k₃ = k + 3)
+    (hk₄ : k₄ = k + 4) (h₀ : Epi (app' φ k₀))
+    (h₁ : IsIso (app' φ k₁)) (h₃ : IsIso (app' φ k₃))
+    (h₄ : Mono (app' φ k₄)) :
+    IsIso (app' φ k₂) := by
+  subst_vars
+  change Epi (app' φ (k₀ + 0)) at h₀
+  rw [← natAddLEFunctor_app' h] at h₀ h₁ h₃ h₄ ⊢
+  exact isIso_of_epi_of_isIso_of_isIso_of_mono (natAddLEFunctor_obj_exact h hR₁)
+    (natAddLEFunctor_obj_exact h hR₂) _ h₀ h₁ h₃ h₄
+
+end Five
+
 /-! The following "three lemmas" for morphisms in `ComposableArrows C 2` are
 special cases of "four lemmas" applied to diagrams where some of the
 leftmost or rightmost maps (or objects) are zero. -/

Mathlib/CategoryTheory/Adjunction/ParametrizedLimits.lean

@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2026 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.CategoryTheory.Adjunction.Parametrized
+public import Mathlib.CategoryTheory.Limits.Opposites
+public import Mathlib.CategoryTheory.Limits.Preserves.Basic
+
+/-!
+# Parametrized adjunctions and limits
+
+Given bifunctors `F : C₁ ⥤ C₂ ⥤ C₃`, `G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂` and
+a paremetrized adjunction `adj₂ : F ⊣₂ G`, we show that for any `X₃ : C₃`,
+the functor `G.flip.obj X₃ : C₁ᵒᵖ ⥤ C₃` preserves limits of shape `J`
+if for any `X₂ : C₂`, the functor `F.flip.obj X₂ : C₁ ⥤ C₃`
+preserves colimits of shape `Jᵒᵖ`.
+
+-/
+
+@[expose] public section
+
+namespace CategoryTheory.ParametrizedAdjunction
+
+open Limits Opposite
+
+variable {C₁ C₂ C₃ : Type*} [Category* C₁] [Category* C₂] [Category* C₃]
+  {F : C₁ ⥤ C₂ ⥤ C₃} {G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂}
+  (adj₂ : F ⊣₂ G) {J : Type*} [Category* J]
+
+include adj₂
+
+set_option backward.isDefEq.respectTransparency false in
+lemma preservesLimit_flip_obj (P : J ⥤ C₁ᵒᵖ)
+    [∀ (X₂ : C₂), PreservesColimit P.leftOp (F.flip.obj X₂)] (X₃ : C₃) :
+    PreservesLimit P (G.flip.obj X₃) where
+  preserves {c} hc := ⟨by
+    let cocone (s : Cone (P ⋙ G.flip.obj X₃)) :
+        Cocone (P.leftOp ⋙ F.flip.obj s.pt) :=
+      { pt := X₃
+        ι.app j := adj₂.homEquiv.symm (s.π.app j.unop)
+        ι.naturality _ _ f := by
+          simp [← s.w f.unop, dsimp% adj₂.homEquiv_symm_naturality_one (P.map f.unop).unop] }
+    let hc' (s : Cone (P ⋙ G.flip.obj X₃)) :=
+      isColimitOfPreserves (F.flip.obj s.pt) (isColimitCoconeLeftOpOfCone _ hc)
+    exact {
+      lift s := adj₂.homEquiv ((hc' s).desc (cocone s))
+      fac s j := by
+        dsimp
+        rw [← dsimp% adj₂.homEquiv_naturality_one (c.π.app j).unop,
+          dsimp% (hc' s).fac (cocone s) (op j)]
+        simp [cocone]
+      uniq s m hm := adj₂.homEquiv.symm.injective (by
+        simp only [op_unop, Equiv.symm_apply_apply]
+        refine (hc' s).uniq (cocone s) _ (fun j ↦ ?_)
+        simp [cocone, ← hm,
+          dsimp% adj₂.homEquiv_symm_naturality_one (c.π.app j.unop).unop]) }⟩
+
+variable (J) in
+lemma preservesLimitsOfShape_flip_obj
+    [∀ (X₂ : C₂), PreservesColimitsOfShape Jᵒᵖ (F.flip.obj X₂)] (X₃ : C₃) :
+    PreservesLimitsOfShape J (G.flip.obj X₃) where
+  preservesLimit := preservesLimit_flip_obj adj₂ _ _
+
+end CategoryTheory.ParametrizedAdjunction

Mathlib/CategoryTheory/ComposableArrows/Basic.lean

@@ -474,6 +474,27 @@ def _root_.Fin.succFunctor (n : ℕ) : Fin n ⥤ Fin (n + 1) where
   obj i := i.succ
   map {_ _} hij := homOfLE (Fin.succ_le_succ_iff.2 (leOfHom hij))
 
+/-- The functor `Fin (l + 1) ⥤ Fin (n + 1)` which sends `i` to `k + i` -/
+@[simps!]
+def _root_.Fin.natAddLEFunctor {n k l : ℕ} (h : k + l ≤ n) : Fin (l + 1) ⥤ Fin (n + 1) where
+  obj := fun ⟨i, _⟩ => ⟨k + i , by lia⟩
+  map {_ _} hij := homOfLE (by rw [Fin.le_iff_val_le_val]; simpa using (leOfHom hij))
+
+/-- The functor `ComposableArrows C n ⥤ ComposableArrows C l` obtained by precomposition with
+the functor `Fin.natAddLEFunctor`. -/
+@[simps!]
+def natAddLEFunctor {n k l : ℕ} (h : k + l ≤ n) :
+    ComposableArrows C n ⥤ ComposableArrows C l :=
+  whiskerLeftFunctor (Fin.natAddLEFunctor h)
+
+lemma natAddLEFunctor_obj' {n k l i : ℕ} (h : k + l ≤ n) (R : ComposableArrows C n)
+    (_ : i ≤ l := by lia) :
+    ((natAddLEFunctor h).obj R).obj' i = R.obj' (k + i) := rfl
+
+lemma natAddLEFunctor_app' {n k l i : ℕ} (h : k + l ≤ n) {R₁ R₂ : ComposableArrows C n}
+    (φ : R₁ ⟶ R₂) (_ : i ≤ l := by lia) :
+    app' ((natAddLEFunctor h).map φ) i = app' φ (k + i) := rfl
+
 /-- The functor `ComposableArrows C (n + 1) ⥤ ComposableArrows C n` which forgets
 the first arrow. -/
 @[simps!]