From 715510c38214f1908b5414fd1b41f59e98900280 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Tue, 19 Dec 2023 11:53:01 +0000 Subject: [PATCH] =?UTF-8?q?feat:=20Monotonicity=20of=20`=E2=80=A2`=20on=20?= =?UTF-8?q?`Finsupp`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Mathlib/Data/DFinsupp/Order.lean | 37 +++++++++++++++++++++++++++++++ Mathlib/Data/Finsupp/Order.lean | 38 ++++++++++++++++++++++++++++++-- 2 files changed, 73 insertions(+), 2 deletions(-) diff --git a/Mathlib/Data/DFinsupp/Order.lean b/Mathlib/Data/DFinsupp/Order.lean index fa58b58413fd1..f0c4c51158c53 100644 --- a/Mathlib/Data/DFinsupp/Order.lean +++ b/Mathlib/Data/DFinsupp/Order.lean @@ -3,6 +3,7 @@ Copyright (c) 2021 Yaël Dillies. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Yaël Dillies -/ +import Mathlib.Algebra.Order.Module.Defs import Mathlib.Data.DFinsupp.Basic #align_import data.dfinsupp.order from "leanprover-community/mathlib"@"1d29de43a5ba4662dd33b5cfeecfc2a27a5a8a29" @@ -150,6 +151,42 @@ instance [∀ i, OrderedAddCommMonoid (α i)] [∀ i, ContravariantClass (α i) ContravariantClass (Π₀ i, α i) (Π₀ i, α i) (· + ·) (· ≤ ·) := ⟨fun _ _ _ H i ↦ le_of_add_le_add_left (H i)⟩ +section Module +variable {α : Type*} {β : ι → Type*} [Semiring α] [Preorder α] [∀ i, AddCommMonoid (β i)] + [∀ i, Preorder (β i)] [∀ i, Module α (β i)] + +instance instPosSMulMono [∀ i, PosSMulMono α (β i)] : PosSMulMono α (Π₀ i, β i) := + PosSMulMono.lift _ coe_le_coe coe_smul + +instance instSMulPosMono [∀ i, SMulPosMono α (β i)] : SMulPosMono α (Π₀ i, β i) := + SMulPosMono.lift _ coe_le_coe coe_smul coe_zero + +instance instPosSMulReflectLE [∀ i, PosSMulReflectLE α (β i)] : PosSMulReflectLE α (Π₀ i, β i) := + PosSMulReflectLE.lift _ coe_le_coe coe_smul + +instance instSMulPosReflectLE [∀ i, SMulPosReflectLE α (β i)] : SMulPosReflectLE α (Π₀ i, β i) := + SMulPosReflectLE.lift _ coe_le_coe coe_smul coe_zero + +end Module + +section Module +variable {α : Type*} {β : ι → Type*} [Semiring α] [PartialOrder α] [∀ i, AddCommMonoid (β i)] + [∀ i, PartialOrder (β i)] [∀ i, Module α (β i)] + +instance instPosSMulStrictMono [∀ i, PosSMulStrictMono α (β i)] : PosSMulStrictMono α (Π₀ i, β i) := + PosSMulStrictMono.lift _ coe_le_coe coe_smul + +instance instSMulPosStrictMono [∀ i, SMulPosStrictMono α (β i)] : SMulPosStrictMono α (Π₀ i, β i) := + SMulPosStrictMono.lift _ coe_le_coe coe_smul coe_zero + +-- Note: There is no interesting instance for `PosSMulReflectLT α (Π₀ i, β i)` that's not already +-- implied by the other instances + +instance instSMulPosReflectLT [∀ i, SMulPosReflectLT α (β i)] : SMulPosReflectLT α (Π₀ i, β i) := + SMulPosReflectLT.lift _ coe_le_coe coe_smul coe_zero + +end Module + section CanonicallyOrderedAddCommMonoid -- porting note: Split into 2 lines to satisfy the unusedVariables linter. diff --git a/Mathlib/Data/Finsupp/Order.lean b/Mathlib/Data/Finsupp/Order.lean index 9bed6cd3e4157..baa09ec25ec16 100644 --- a/Mathlib/Data/Finsupp/Order.lean +++ b/Mathlib/Data/Finsupp/Order.lean @@ -3,7 +3,8 @@ Copyright (c) 2021 Johan Commelin. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Johan Commelin, Aaron Anderson -/ -import Mathlib.Data.Finsupp.Defs +import Mathlib.Algebra.Order.Module.Defs +import Mathlib.Data.Finsupp.Basic #align_import data.finsupp.order from "leanprover-community/mathlib"@"1d29de43a5ba4662dd33b5cfeecfc2a27a5a8a29" @@ -30,7 +31,7 @@ open BigOperators open Finset -variable {ι α : Type*} +variable {ι α β : Type*} namespace Finsupp @@ -149,6 +150,39 @@ instance contravariantClass [OrderedAddCommMonoid α] [ContravariantClass α α ContravariantClass (ι →₀ α) (ι →₀ α) (· + ·) (· ≤ ·) := ⟨fun _f _g _h H x => le_of_add_le_add_left <| H x⟩ +section SMulZeroClass +variable [Zero α] [Preorder α] [Zero β] [Preorder β] [SMulZeroClass α β] + +instance instPosSMulMono [PosSMulMono α β] : PosSMulMono α (ι →₀ β) := + PosSMulMono.lift _ coe_le_coe coe_smul + +instance instSMulPosMono [SMulPosMono α β] : SMulPosMono α (ι →₀ β) := + SMulPosMono.lift _ coe_le_coe coe_smul coe_zero + +instance instPosSMulReflectLE [PosSMulReflectLE α β] : PosSMulReflectLE α (ι →₀ β) := + PosSMulReflectLE.lift _ coe_le_coe coe_smul + +instance instSMulPosReflectLE [SMulPosReflectLE α β] : SMulPosReflectLE α (ι →₀ β) := + SMulPosReflectLE.lift _ coe_le_coe coe_smul coe_zero + +end SMulZeroClass + +section SMulWithZero +variable [Zero α] [PartialOrder α] [Zero β] [PartialOrder β] [SMulWithZero α β] + +instance instPosSMulStrictMono [PosSMulStrictMono α β] : PosSMulStrictMono α (ι →₀ β) := + PosSMulStrictMono.lift _ coe_le_coe coe_smul + +instance instSMulPosStrictMono [SMulPosStrictMono α β] : SMulPosStrictMono α (ι →₀ β) := + SMulPosStrictMono.lift _ coe_le_coe coe_smul coe_zero + +-- `PosSMulReflectLT α (ι →₀ β)` already follows from the other instances + +instance instSMulPosReflectLT [SMulPosReflectLT α β] : SMulPosReflectLT α (ι →₀ β) := + SMulPosReflectLT.lift _ coe_le_coe coe_smul coe_zero + +end SMulWithZero + section CanonicallyOrderedAddCommMonoid variable [CanonicallyOrderedAddCommMonoid α] {f g : ι →₀ α}