feat: Finset.sup in a group (#19460)

Co-authored-by: Andrew Yang

Author: YaelDillies

Mathlib.lean

@@ -655,6 +655,7 @@ import Mathlib.Algebra.Order.Group.CompleteLattice
 import Mathlib.Algebra.Order.Group.Cone
 import Mathlib.Algebra.Order.Group.Defs
 import Mathlib.Algebra.Order.Group.DenselyOrdered
+import Mathlib.Algebra.Order.Group.Finset
 import Mathlib.Algebra.Order.Group.Indicator
 import Mathlib.Algebra.Order.Group.InjSurj
 import Mathlib.Algebra.Order.Group.Instances

Mathlib/Algebra/Order/Group/Finset.lean

@@ -0,0 +1,81 @@
+/-
+Copyright (c) 2024 Yaël Dillies, Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies, Andrew Yang
+-/
+import Mathlib.Algebra.Order.Group.OrderIso
+import Mathlib.Algebra.Order.Monoid.Canonical.Defs
+import Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
+import Mathlib.Algebra.Order.Monoid.Unbundled.Pow
+import Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
+import Mathlib.Data.Finset.Lattice.Fold
+
+/-!
+# `Finset.sup` in a group
+-/
+
+assert_not_exists MonoidWithZero
+
+namespace Finset
+variable {ι κ M G : Type*}
+
+lemma fold_max_add [LinearOrder M] [Add M] [AddRightMono M] (s : Finset ι) (a : WithBot M)
+    (f : ι → M) : s.fold max ⊥ (fun i ↦ ↑(f i) + a) = s.fold max ⊥ ((↑) ∘ f) + a := by
+  classical
+    induction' s using Finset.induction_on with a s _ ih <;> simp [*, max_add_add_right]
+
+@[to_additive nsmul_inf']
+lemma inf'_pow [LinearOrder M] [Monoid M] [MulLeftMono M] [MulRightMono M] (s : Finset ι)
+    (f : ι → M) (n : ℕ) (hs) : s.inf' hs f ^ n = s.inf' hs fun a ↦ f a ^ n :=
+  map_finset_inf' (OrderHom.mk _ <| pow_left_mono n) hs _
+
+@[to_additive nsmul_sup']
+lemma sup'_pow [LinearOrder M] [Monoid M] [MulLeftMono M] [MulRightMono M] (s : Finset ι)
+    (f : ι → M) (n : ℕ) (hs) : s.sup' hs f ^ n = s.sup' hs fun a ↦ f a ^ n :=
+  map_finset_sup' (OrderHom.mk _ <| pow_left_mono n) hs _
+
+section Group
+variable [Group G] [LinearOrder G]
+
+@[to_additive "Also see `Finset.sup'_add'` that works for canonically ordered monoids."]
+lemma sup'_mul [MulRightMono G] (s : Finset ι) (f : ι → G) (a : G) (hs) :
+    s.sup' hs f * a = s.sup' hs fun i ↦ f i * a := map_finset_sup' (OrderIso.mulRight a) hs f
+
+set_option linter.docPrime false in
+@[to_additive "Also see `Finset.add_sup''` that works for canonically ordered monoids."]
+lemma mul_sup' [MulLeftMono G] (s : Finset ι) (f : ι → G) (a : G) (hs) :
+    a * s.sup' hs f = s.sup' hs fun i ↦ a * f i := map_finset_sup' (OrderIso.mulLeft a) hs f
+
+end Group
+
+section CanonicallyLinearOrderedAddCommMonoid
+variable [CanonicallyLinearOrderedAddCommMonoid M] [Sub M] [AddLeftReflectLE M] [OrderedSub M]
+  {s : Finset ι} {t : Finset κ}
+
+/-- Also see `Finset.sup'_add` that works for ordered groups. -/
+lemma sup'_add' (s : Finset ι) (f : ι → M) (a : M) (hs : s.Nonempty) :
+    s.sup' hs f + a = s.sup' hs fun i ↦ f i + a := by
+  apply le_antisymm
+  · apply add_le_of_le_tsub_right_of_le
+    · exact Finset.le_sup'_of_le _ hs.choose_spec le_add_self
+    · exact Finset.sup'_le _ _ fun i hi ↦ le_tsub_of_add_le_right (Finset.le_sup' (f · + a) hi)
+  · exact Finset.sup'_le _ _ fun i hi ↦ add_le_add_right (Finset.le_sup' _ hi) _
+
+/-- Also see `Finset.add_sup'` that works for ordered groups. -/
+lemma add_sup'' (hs : s.Nonempty) (f : ι → M) (a : M) :
+    a + s.sup' hs f = s.sup' hs fun i ↦ a + f i := by simp_rw [add_comm a, Finset.sup'_add']
+
+protected lemma sup_add (hs : s.Nonempty) (f : ι → M) (a : M) :
+    s.sup f + a = s.sup fun i ↦ f i + a := by
+  rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, sup'_add']
+
+protected lemma add_sup (hs : s.Nonempty) (f : ι → M) (a : M) :
+    a + s.sup f = s.sup fun i ↦ a + f i := by
+  rw [← Finset.sup'_eq_sup hs, ← Finset.sup'_eq_sup hs, add_sup'']
+
+lemma sup_add_sup (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → M) (g : κ → M) :
+    s.sup f + t.sup g = (s ×ˢ t).sup fun ij ↦ f ij.1 + g ij.2 := by
+  simp only [Finset.sup_add hs, Finset.add_sup ht, Finset.sup_product_left]
+
+end CanonicallyLinearOrderedAddCommMonoid
+end Finset

Mathlib/Algebra/Polynomial/Basic.lean

@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes, Johannes Hölzl, Kim Morrison, Jens Wagemaker
 -/
 import Mathlib.Algebra.GroupWithZero.Divisibility
-import Mathlib.Data.Finset.Sort
 import Mathlib.Algebra.MonoidAlgebra.Defs
+import Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
+import Mathlib.Data.Finset.Sort
 import Mathlib.Order.OmegaCompletePartialOrder
 
 /-!

Mathlib/Data/Finset/Fold.lean

@@ -3,8 +3,6 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
-import Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
 import Mathlib.Data.Finset.Image
 import Mathlib.Data.Multiset.Fold
 
@@ -231,11 +229,6 @@ theorem fold_max_lt : s.fold max b f < c ↔ b < c ∧ ∀ x ∈ s, f x < c := b
 theorem lt_fold_max : c < s.fold max b f ↔ c < b ∨ ∃ x ∈ s, c < f x :=
   fold_op_rel_iff_or lt_max_iff
 
-theorem fold_max_add [Add β] [AddRightMono β] (n : WithBot β)
-    (s : Finset α) : (s.fold max ⊥ fun x : α => ↑(f x) + n) = s.fold max ⊥ ((↑) ∘ f) + n := by
-  classical
-    induction' s using Finset.induction_on with a s _ ih <;> simp [*, max_add_add_right]
-
 end Order
 
 end Fold

Mathlib/Data/Finset/Lattice/Fold.lean

@@ -3,7 +3,6 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Mathlib.Algebra.Order.Monoid.Unbundled.Pow
 import Mathlib.Data.Finset.Fold
 import Mathlib.Data.Finset.Pi
 import Mathlib.Data.Finset.Prod
@@ -819,13 +818,6 @@ theorem _root_.map_finset_sup' [SemilatticeSup β] [FunLike F α β] [SupHomClas
     f (s.sup' hs g) = s.sup' hs (f ∘ g) := by
   refine hs.cons_induction ?_ ?_ <;> intros <;> simp [*]
 
-lemma nsmul_sup' {α β : Type*} [AddMonoid β] [LinearOrder β]
-    [AddLeftMono β] [AddRightMono β]
-    {s : Finset α} (hs : s.Nonempty) (f : α → β) (n : ℕ) :
-    s.sup' hs (fun a => n • f a) = n • s.sup' hs f :=
-  let ns : SupHom β β := { toFun := (n • ·), map_sup' := fun _ _ => (nsmul_right_mono n).map_max }
-  (map_finset_sup' ns hs _).symm
-
 /-- To rewrite from right to left, use `Finset.sup'_comp_eq_image`. -/
 @[simp]
 theorem sup'_image [DecidableEq β] {s : Finset γ} {f : γ → β} (hs : (s.image f).Nonempty)
@@ -857,6 +849,11 @@ lemma sup'_comp_eq_map {s : Finset γ} {f : γ ↪ β} (g : β → α) (hs : s.N
 theorem sup'_mono {s₁ s₂ : Finset β} (h : s₁ ⊆ s₂) (h₁ : s₁.Nonempty) :
     s₁.sup' h₁ f ≤ s₂.sup' (h₁.mono h) f :=
   Finset.sup'_le h₁ _ (fun _ hb => le_sup' _ (h hb))
+
+@[gcongr]
+lemma sup'_mono_fun {hs : s.Nonempty} {f g : β → α} (h : ∀ b ∈ s, f b ≤ g b) :
+    s.sup' hs f ≤ s.sup' hs g := sup'_le _ _ fun b hb ↦ (h b hb).trans (le_sup' _ hb)
+
 end Sup'
 
 section Inf'
@@ -974,13 +971,6 @@ theorem _root_.map_finset_inf' [SemilatticeInf β] [FunLike F α β] [InfHomClas
     f (s.inf' hs g) = s.inf' hs (f ∘ g) := by
   refine hs.cons_induction ?_ ?_ <;> intros <;> simp [*]
 
-lemma nsmul_inf' {α β : Type*} [AddMonoid β] [LinearOrder β]
-    [AddLeftMono β] [AddRightMono β]
-    {s : Finset α} (hs : s.Nonempty) (f : α → β) (n : ℕ) :
-    s.inf' hs (fun a => n • f a) = n • s.inf' hs f :=
-  let ns : InfHom β β := { toFun := (n • ·), map_inf' := fun _ _ => (nsmul_right_mono n).map_min }
-  (map_finset_inf' ns hs _).symm
-
 /-- To rewrite from right to left, use `Finset.inf'_comp_eq_image`. -/
 @[simp]
 theorem inf'_image [DecidableEq β] {s : Finset γ} {f : γ → β} (hs : (s.image f).Nonempty)

Mathlib/Order/Filter/AtTopBot/Monoid.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import Mathlib.Algebra.Order.Monoid.OrderDual
+import Mathlib.Algebra.Order.Monoid.Unbundled.Pow
 import Mathlib.Order.Filter.AtTopBot
 
 /-!

Mathlib/RingTheory/HahnSeries/Basic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 -/
 import Mathlib.Algebra.Group.Support
+import Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
 import Mathlib.Order.WellFoundedSet
 
 /-!

Mathlib/Topology/Algebra/ConstMulAction.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alex Kontorovich, Heather Macbeth
 -/
 import Mathlib.Algebra.Module.ULift
+import Mathlib.Algebra.Order.Group.Synonym
 import Mathlib.Data.Set.Pointwise.SMul
 import Mathlib.GroupTheory.GroupAction.Defs
 import Mathlib.Topology.Algebra.Constructions