Merge remote-tracking branch 'upstream/master' into bump/v4.28.0

Author: mathlib4-bot

.github/workflows/daily.yml

@@ -99,7 +99,7 @@ jobs:
   notify-lean4checker:
     runs-on: ubuntu-latest
     needs: check-lean4checker
-    if: always()
+    if: github.repository == 'leanprover-community/mathlib4' && always()
     strategy:
       fail-fast: false
       matrix:
@@ -218,7 +218,7 @@ jobs:
   notify-mathlib_test_executable:
     runs-on: ubuntu-latest
     needs: check-mathlib_test_executable
-    if: always()
+    if: github.repository == 'leanprover-community/mathlib4' && always()
     strategy:
       fail-fast: false
       matrix:

Cache/IO.lean

@@ -459,10 +459,10 @@ Return tuples of the form ("module name", "path to .lean file").
 
 The input string `arg` takes one of the following forms:
 
-1. `Mathlib.Algebra.Fields.Basic`: there exists such a Lean file
-2. `Mathlib.Algebra.Fields`: no Lean file exists but a folder (TODO)
-3. `Mathlib/Algebra/Fields/Basic.lean`: the file exists (note potentially `\` on Windows)
-4. `Mathlib/Algebra/Fields/`: the folder exists (TODO)
+1. `Mathlib.Algebra.Field.Basic`: there exists such a Lean file
+2. `Mathlib.Algebra.Field`: no Lean file exists but a folder (TODO)
+3. `Mathlib/Algebra/Field/Basic.lean`: the file exists (note potentially `\` on Windows)
+4. `Mathlib/Algebra/Field/`: the folder exists (TODO)
 
 Not supported yet:
 

Mathlib.lean

@@ -388,6 +388,7 @@ public import Mathlib.Algebra.Group.Int.Units
 public import Mathlib.Algebra.Group.Invertible.Basic
 public import Mathlib.Algebra.Group.Invertible.Defs
 public import Mathlib.Algebra.Group.Irreducible.Defs
+public import Mathlib.Algebra.Group.Irreducible.Indecomposable
 public import Mathlib.Algebra.Group.Irreducible.Lemmas
 public import Mathlib.Algebra.Group.MinimalAxioms
 public import Mathlib.Algebra.Group.Nat.Defs
@@ -608,6 +609,7 @@ public import Mathlib.Algebra.Homology.HomotopyCategory.Shift
 public import Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
 public import Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
 public import Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
+public import Mathlib.Algebra.Homology.HomotopyCategory.SpectralObject
 public import Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
 public import Mathlib.Algebra.Homology.HomotopyCofiber
 public import Mathlib.Algebra.Homology.ImageToKernel
@@ -1372,6 +1374,7 @@ public import Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit
 public import Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
 public import Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
 public import Mathlib.AlgebraicTopology.ModelCategory.Basic
+public import Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
 public import Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
 public import Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
 public import Mathlib.AlgebraicTopology.ModelCategory.Cylinder
@@ -1427,6 +1430,7 @@ public import Mathlib.AlgebraicTopology.SimplicialSet.Dimension
 public import Mathlib.AlgebraicTopology.SimplicialSet.Finite
 public import Mathlib.AlgebraicTopology.SimplicialSet.FiniteColimits
 public import Mathlib.AlgebraicTopology.SimplicialSet.FiniteProd
+public import Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
 public import Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
 public import Mathlib.AlgebraicTopology.SimplicialSet.Horn
 public import Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
@@ -2260,6 +2264,7 @@ public import Mathlib.CategoryTheory.Adjunction.Whiskering
 public import Mathlib.CategoryTheory.Balanced
 public import Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
 public import Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
+public import Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
 public import Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
 public import Mathlib.CategoryTheory.Bicategory.Basic
 public import Mathlib.CategoryTheory.Bicategory.CatEnriched
@@ -3249,6 +3254,7 @@ public import Mathlib.Combinatorics.SimpleGraph.Coloring
 public import Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
 public import Mathlib.Combinatorics.SimpleGraph.ConcreteColorings
 public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
+public import Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity
 public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
 public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
 public import Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting
@@ -5416,6 +5422,7 @@ public import Mathlib.Order.CompleteLattice.Finset
 public import Mathlib.Order.CompleteLattice.Group
 public import Mathlib.Order.CompleteLattice.Lemmas
 public import Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
+public import Mathlib.Order.CompleteLattice.PiLex
 public import Mathlib.Order.CompleteLattice.SetLike
 public import Mathlib.Order.CompleteLatticeIntervals
 public import Mathlib.Order.CompletePartialOrder

Mathlib/Algebra/BigOperators/Ring/Finset.lean

@@ -220,6 +220,11 @@ theorem prod_add_ordered [LinearOrder ι] (s : Finset ι) (f g : ι → R) :
       mul_left_comm]
     exact mt (fun ha => (mem_filter.1 ha).1) ha'
 
+theorem prod_one_add_ordered [LinearOrder ι] (s : Finset ι) (f : ι → R) :
+    ∏ i ∈ s, (1 + f i) = 1 + ∑ i ∈ s, f i * ∏ j ∈ s with j < i, (1 + f j) := by
+  rw [prod_add_ordered]
+  simp
+
 /-- Summing `a ^ #t * b ^ (n - #t)` over all finite subsets `t` of a finset `s`
 gives `(a + b) ^ #s`. -/
 theorem sum_pow_mul_eq_add_pow (a b : R) (s : Finset ι) :

Mathlib/Algebra/Group/Irreducible/Indecomposable.lean

@@ -0,0 +1,69 @@
+/-
+Copyright (c) 2025 Oliver Nash. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Nash
+-/
+module
+
+public import Mathlib.Algebra.Group.Irreducible.Defs
+public import Mathlib.Algebra.Group.Submonoid.Basic
+public import Mathlib.Algebra.Order.Monoid.Defs
+public import Mathlib.Order.Preorder.Finite
+
+/-!
+# Indecomposable elements of monoids
+-/
+
+@[expose] public section
+
+open Set
+
+variable {ι M : Type*} [Monoid M]
+
+/-- Given a family of elements of a monoid, a member is said to be indecomposable if it cannot be
+written as a product of two others in a non-trivial way. -/
+@[to_additive (attr := simp) /-- Given a family of elements of an additive monoid, a member is said
+to be indecomposable if it cannot be written as a sum of two others in a non-trivial way.-/]
+def IsMulIndecomposable (v : ι → M) (s : Set ι) (i : ι) : Prop :=
+  i ∈ s ∧ ∀ᵉ (j ∈ s) (k ∈ s), v i = v j * v k → v j = 1 ∨ v k = 1
+
+@[to_additive]
+lemma isMulIndecomposable_id_univ [Subsingleton Mˣ] {x : M} (hx : x ≠ 1) :
+    IsMulIndecomposable id univ x ↔ Irreducible x :=
+  ⟨fun h ↦ ⟨by simpa, by simpa using h⟩, fun h ↦ by simpa using h.isUnit_or_isUnit⟩
+
+/-- Given a finite family of points `v` in a monoid `M`, together with a morphism into a
+linearly-ordered monoid `f : M →* S`, the submonoid generated by those points of `v` which lie in
+the "half space" where `f > 1` is generated by the subset of such points which are indecomposable
+with respect to points in this half space. -/
+@[to_additive /-- Given a finite family of points `v` in an additive monoid `M`, together with a
+morphism into a linearly-ordered additive monoid `f : M →+ S`, the submonoid generated by those
+points of `v` which lie in the half space where `f > 0` is generated by the subset of such points
+which are indecomposable with respect to points in this half space.
+
+If `v` is the set of roots of a crystallographic root system and `S = ℚ`, then this is
+[serre1965](Ch. V, §9, Lemma 2) and it may be used to prove that the root system has a base. -/]
+lemma Submonoid.closure_image_one_lt_and_isMulIndecomposable [Finite ι]
+    {S : Type*} [CommMonoid S] [LinearOrder S] [IsOrderedCancelMonoid S]
+    (v : ι → M) (f : M →* S) :
+    closure (v '' {i | IsMulIndecomposable v {j | 1 < f (v j)} i}) =
+      closure (v '' {i | 1 < f (v i)}) := by
+  refine le_antisymm (closure_mono (image_mono <| by aesop)) (closure_le.mpr ?_)
+  rintro - ⟨i, hi : 1 < f (v i), rfl⟩
+  by_contra hi'
+  let t : Set ι := {i | IsMulIndecomposable v {j | 1 < f (v j)} i}
+  let s : Set ι := {j | 1 < f (v j) ∧ v j ∉ closure (v '' t)}
+  have hne : s.Nonempty := ⟨i, hi, hi'⟩
+  clear! i
+  obtain ⟨i, hi⟩ := s.toFinite.exists_minimalFor (f ∘ v) s hne
+  have ⟨(hi₀ : 1 < f (v i)), (hi₁ : v i ∉ _)⟩ : i ∈ s := hi.prop
+  have hi₂ (k : ι) (hk₀ : 1 < f (v k)) (hk₁ : f (v k) < f (v i)) : v k ∈ closure (v '' t) := by
+    by_contra hk₂; exact not_le.mpr hk₁ <| hi.le_of_le ⟨hk₀, hk₂⟩ hk₁.le
+  have hi₃ : i ∉ t := by contrapose! hi₁; exact subset_closure <| mem_image_of_mem v hi₁
+  obtain ⟨j, k, hj, hk, hjk⟩ : ∃ (j k : ι) (hj : 1 < f (v j)) (hk : 1 < f (v k)),
+      v i = v j * v k := by
+    grind [IsMulIndecomposable]
+  have hj' : v j ∈ closure (v '' t) := hi₂ j hj <| by aesop
+  have hk' : v k ∈ closure (v '' t) := hi₂ k hk <| by aesop
+  replace hjk : v i ∈ closure (v '' t) := hjk ▸ mul_mem hj' hk'
+  exact hi₁ hjk

Mathlib/Algebra/Homology/DerivedCategory/Ext/ExtClass.lean

@@ -85,7 +85,7 @@ noncomputable def extClass : Ext.{w} S.X₃ S.X₁ 1 := by
 lemma extClass_hom [HasDerivedCategory.{w'} C] : hS.extClass.hom = hS.singleδ := by
   change SmallShiftedHom.equiv W Q hS.extClass = _
   dsimp [extClass, SmallShiftedHom.equiv]
-  erw [SmallHom.equiv_comp, Iso.homToEquiv_apply]
+  erw [SmallHom.equiv_comp]
   rw [SmallHom.equiv_mkInv, SmallHom.equiv_mk]
   dsimp [singleδ, triangleOfSESδ]
   rw [Category.assoc, Category.assoc, Category.assoc,

Mathlib/Algebra/Homology/HomotopyCategory/SpectralObject.lean

@@ -0,0 +1,61 @@
+/-
+Copyright (c) 2024 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.HomotopyCategory.Triangulated
+public import Mathlib.CategoryTheory.Triangulated.SpectralObject
+
+/-!
+# The spectral object with values in the homotopy category
+
+Let `C` be an additive category. In this file, we show that the
+mapping cone defines a spectral object with values in the homotopy
+category of `ℤ`-indexed cochain complexes `C` that is indexed
+by the category `CochainComplex C ℤ`.
+(It follows that to any functor `ι ⥤ CochainComplex C ℤ` (e.g. a filtered
+complex), there is an associated spectral object indexed by `ι`.)
+
+-/
+
+@[expose] public section
+
+namespace HomotopyCategory
+
+open CategoryTheory Limits Triangulated CochainComplex.mappingCone
+
+variable (C : Type*) [Category* C] [Preadditive C]
+  [HasZeroObject C] [HasBinaryBiproducts C]
+
+/-- The functor `ComposableArrows (CochainComplex C ℤ) 1 ⥤ CochainComplex C ℤ` which
+sends a morphism of cochain complexes to its mapping cone. -/
+@[simps]
+noncomputable def composableArrowsFunctor :
+    ComposableArrows (CochainComplex C ℤ) 1 ⥤ CochainComplex C ℤ where
+  obj f := CochainComplex.mappingCone (f.map' 0 1)
+  map φ := map _ _ (φ.app 0) (φ.app 1) (ComposableArrows.naturality' φ 0 1)
+  map_id _ := map_id _
+  map_comp _ _ := map_comp _ _ _ _ _ _ _ _ _
+
+/-- The spectral object with values in `(HomotopyCategory C (.up ℤ)` that
+is indexed by `CochainComplex C ℤ`. -/
+@[simps]
+noncomputable def spectralObjectMappingCone :
+    SpectralObject (HomotopyCategory C (ComplexShape.up ℤ)) (CochainComplex C ℤ) where
+  ω₁ := composableArrowsFunctor C ⋙ HomotopyCategory.quotient _ _
+  δ'.app D := ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).mapTriangle.obj
+    (CochainComplex.mappingConeCompTriangle (D.map' 0 1) (D.map' 1 2))).mor₃
+  δ'.naturality D₁ D₂ φ := by
+    obtain ⟨_, _, _, f, g, rfl⟩ := ComposableArrows.mk₂_surjective D₁
+    obtain ⟨_, _, _, f', g', rfl⟩ := ComposableArrows.mk₂_surjective D₂
+    have eq := CochainComplex.mappingConeCompTriangle_mor₃_naturality f g f' g' φ
+    dsimp [ComposableArrows.Precomp.map] at eq ⊢
+    simp only [Category.assoc, ← Functor.map_comp_assoc]
+    simp [eq]
+  distinguished' D := by
+    obtain ⟨_, _, _, f, g, rfl⟩ := ComposableArrows.mk₂_surjective D
+    exact HomotopyCategory.mappingConeCompTriangleh_distinguished f g
+
+end HomotopyCategory

Mathlib/Algebra/Module/Submodule/Map.lean

@@ -595,11 +595,8 @@ theorem orderIsoMapComap_symm_apply' (e : M ≃ₛₗ[τ₁₂] M₂) (p : Submo
 
 theorem inf_comap_le_comap_add (f₁ f₂ : M →ₛₗ[τ₁₂] M₂) :
     comap f₁ q ⊓ comap f₂ q ≤ comap (f₁ + f₂) q := by
-  rw [SetLike.le_def]
-  intro m h
-  change f₁ m + f₂ m ∈ q
-  change f₁ m ∈ q ∧ f₂ m ∈ q at h
-  apply q.add_mem h.1 h.2
+  simp only [SetLike.le_def, mem_comap, mem_inf, LinearMap.add_apply]
+  exact fun _ h ↦ add_mem h.1 h.2
 
 lemma surjOn_iff_le_map [RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {p : Submodule R M}
     {q : Submodule R₂ M₂} : Set.SurjOn f p q ↔ q ≤ p.map f :=
@@ -619,11 +616,8 @@ variable (p : Submodule R M) (q : Submodule R₂ M₂)
 variable (pₗ : Submodule R N) (qₗ : Submodule R N₂)
 
 theorem comap_le_comap_smul (fₗ : N →ₗ[R] N₂) (c : R) : comap fₗ qₗ ≤ comap (c • fₗ) qₗ := by
-  rw [SetLike.le_def]
-  intro m h
-  change c • fₗ m ∈ qₗ
-  change fₗ m ∈ qₗ at h
-  apply qₗ.smul_mem _ h
+  simp only [SetLike.le_def, mem_comap, LinearMap.smul_apply]
+  exact fun _ h ↦ smul_mem _ _ h
 
 /-- Given modules `M`, `M₂` over a commutative ring, together with submodules `p ⊆ M`, `q ⊆ M₂`,
 the set of maps $\{f ∈ Hom(M, M₂) | f(p) ⊆ q \}$ is a submodule of `Hom(M, M₂)`. -/

Mathlib/Algebra/Module/ZLattice/Basic.lean

@@ -104,9 +104,7 @@ theorem map_fundamentalDomain {F : Type*} [NormedAddCommGroup F] [NormedSpace K
 theorem fundamentalDomain_reindex {ι' : Type*} (e : ι ≃ ι') :
     fundamentalDomain (b.reindex e) = fundamentalDomain b := by
   ext
-  simp_rw [mem_fundamentalDomain, Basis.repr_reindex_apply]
-  rw [Equiv.forall_congr' e]
-  simp_rw [implies_true]
+  simp [e.forall_congr_left]
 
 variable [IsStrictOrderedRing K]
 

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

@@ -947,11 +947,6 @@ lemma zpow_pos (ha : 0 < a) : ∀ n : ℤ, 0 < a ^ n
   | (n : ℕ) => by rw [zpow_natCast]; exact pow_pos ha _
   | -(n + 1 : ℕ) => by rw [zpow_neg, inv_pos, zpow_natCast]; exact pow_pos ha _
 
-omit [ZeroLEOneClass G₀] in
-lemma zpow_left_strictMonoOn₀ [MulPosMono G₀] (hn : 0 < n) :
-    StrictMonoOn (fun a : G₀ ↦ a ^ n) {a | 0 ≤ a} := by
-  lift n to ℕ using hn.le; simpa using pow_left_strictMonoOn₀ (by lia)
-
 lemma zpow_right_mono₀ (ha : 1 ≤ a) : Monotone fun n : ℤ ↦ a ^ n := by
   refine monotone_int_of_le_succ fun n ↦ ?_
   rw [zpow_add_one₀ (zero_lt_one.trans_le ha).ne']
@@ -1048,6 +1043,24 @@ end ZPow
 
 end ZeroLEOneClass
 
+section MulPosMono
+
+variable [MulPosMono G₀] {n : ℤ}
+
+lemma zpow_left_monoOn₀ (hn : 0 ≤ n) : MonotoneOn (fun a : G₀ ↦ a ^ n) {a | 0 ≤ a} := by
+  lift n to ℕ using hn; simpa using pow_left_monotoneOn
+
+lemma zpow_left_strictMonoOn₀ (hn : 0 < n) : StrictMonoOn (fun a : G₀ ↦ a ^ n) {a | 0 ≤ a} := by
+  lift n to ℕ using hn.le; simpa using pow_left_strictMonoOn₀ (by lia)
+
+lemma zpow_le_zpow_left₀ (hn : 0 ≤ n) (ha : 0 ≤ a) (h : a ≤ b) : a ^ n ≤ b ^ n :=
+  zpow_left_monoOn₀ (G₀ := G₀) hn ha (by grind) h
+
+lemma zpow_lt_zpow_left₀ (hn : 0 < n) (ha : 0 ≤ a) (h : a < b) : a ^ n < b ^ n :=
+  zpow_left_strictMonoOn₀ (G₀ := G₀) hn ha (by grind) h
+
+end MulPosMono
+
 end PosMulReflectLT
 
 section MulPosReflectLT
@@ -1290,10 +1303,12 @@ lemma neg_of_div_neg_left (h : a / b < 0) (hb : 0 ≤ b) : a < 0 :=
 
 end PosMulMono
 
-variable [PosMulStrictMono G₀] {m n : ℤ}
+variable {m n : ℤ}
 
 section ZeroLEOne
 
+variable [PosMulStrictMono G₀]
+
 variable [ZeroLEOneClass G₀]
 
 lemma inv_lt_one_iff₀ : a⁻¹ < 1 ↔ a ≤ 0 ∨ 1 < a := by
@@ -1317,6 +1332,18 @@ lemma zpow_eq_one_iff_right₀ (ha₀ : 0 ≤ a) (ha₁ : a ≠ 1) {n : ℤ} : a
 
 end ZeroLEOne
 
+section MulPosMono
+
+variable [PosMulReflectLT G₀] [MulPosMono G₀]
+
+lemma zpow_le_zpow_iff_left₀ (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : 0 < n) : a ^ n ≤ b ^ n ↔ a ≤ b :=
+  (zpow_left_strictMonoOn₀ (G₀ := G₀) hn).le_iff_le ha hb
+
+lemma zpow_lt_zpow_iff_left₀ (ha : 0 ≤ a) (hb : 0 ≤ b) (hn : 0 < n) : a ^ n < b ^ n ↔ a < b :=
+  (zpow_left_strictMonoOn₀ (G₀ := G₀) hn).lt_iff_lt ha hb
+
+end MulPosMono
+
 variable [MulPosStrictMono G₀]
 
 end GroupWithZero.LinearOrder