Built with doc-gen4, running Lean4.
Bubbles () indicate interactive fragments: hover for details, tap to reveal contents.
Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus.
On Mac, use Cmdinstead of Ctrl.
/-
Copyright (c) 2021 Damiano Testa. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Damiano Testa
! This file was ported from Lean 3 source module algebra.covariant_and_contravariant
! leanprover-community/mathlib commit 2258b40dacd2942571c8ce136215350c702dc78f
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Group.Defs
import Mathlib.Order.Basic
import Mathlib.Order.Monotone.Basic
/-!
# Covariants and contravariants
This file contains general lemmas and instances to work with the interactions between a relation and
an action on a Type.
The intended application is the splitting of the ordering from the algebraic assumptions on the
operations in the `Ordered[...]` hierarchy.
The strategy is to introduce two more flexible typeclasses, `CovariantClass` and
`ContravariantClass`:
* `CovariantClass` models the implication `a ≤ b → c * a ≤ c * b` (multiplication is monotone),
* `ContravariantClass` models the implication `a * b < a * c → b < c`.
Since `Co(ntra)variantClass` takes as input the operation (typically `(+)` or `(*)`) and the order
relation (typically `(≤)` or `(<)`), these are the only two typeclasses that I have used.
The general approach is to formulate the lemma that you are interested in and prove it, with the
`Ordered[...]` typeclass of your liking. After that, you convert the single typeclass,
say `[OrderedCancelMonoid M]`, into three typeclasses, e.g.
`[LeftCancelSemigroup M] [PartialOrder M] [CovariantClass M M (Function.swap (*)) (≤)]`
and have a go at seeing if the proof still works!
Note that it is possible to combine several `Co(ntra)variantClass` assumptions together.
Indeed, the usual ordered typeclasses arise from assuming the pair
`[CovariantClass M M (*) (≤)] [ContravariantClass M M (*) (<)]`
on top of order/algebraic assumptions.
A formal remark is that normally `CovariantClass` uses the `(≤)`-relation, while
`ContravariantClass` uses the `(<)`-relation. This need not be the case in general, but seems to be
the most common usage. In the opposite direction, the implication
```lean
[Semigroup α] [PartialOrder α] [ContravariantClass α α (*) (≤)] => LeftCancelSemigroup α
```
holds -- note the `Co*ntra*` assumption on the `(≤)`-relation.
# Formalization notes
We stick to the convention of using `Function.swap (*)` (or `Function.swap (+)`), for the
typeclass assumptions, since `Function.swap` is slightly better behaved than `flip`.
However, sometimes as a **non-typeclass** assumption, we prefer `flip (*)` (or `flip (+)`),
as it is easier to use.
-/
-- TODO: convert `ExistsMulOfLE`, `ExistsAddOfLE`?
-- TODO: relationship with `Con/AddCon`
-- TODO: include equivalence of `LeftCancelSemigroup` with
-- `Semigroup PartialOrder ContravariantClass α α (*) (≤)`?
-- TODO : use ⇒, as per Eric's suggestion? See
-- https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/ordered.20stuff/near/236148738
-- for a discussion.
open Function
section Variants
variable {
N)
/-- `Covariant` is useful to formulate succintly statements about the interactions between an
action of a Type on another one and a relation on the acted-upon Type.
See the `CovariantClass` doc-string for its meaning. -/
def
Covariant: (M : Type u_1) → (N : Type u_2) → (M → N → N) → (N → N → Prop) → Prop
Covariant
/-- `Contravariant` is useful to formulate succintly statements about the interactions between an
action of a Type on another one and a relation on the acted-upon Type.
See the `ContravariantClass` doc-string for its meaning. -/
def
Contravariant: (M : Type u_1) → (N : Type u_2) → (M → N → N) → (N → N → Prop) → Prop
Contravariant: (M : Type u_1) → (N : Type u_2) → (M → N → N) → (N → N → Prop) → Prop
Contravariant
/-- Given an action `μ` of a Type `M` on a Type `N` and a relation `r` on `N`, informally, the
`CovariantClass` says that "the action `μ` preserves the relation `r`."
More precisely, the `CovariantClass` is a class taking two Types `M N`, together with an "action"
`μ : M → N → N` and a relation `r : N → N → Prop`. Its unique field `elim` is the assertion that
for all `m ∈ M` and all elements `n₁, n₂ ∈ N`, if the relation `r` holds for the pair
`(n₁, n₂)`, then, the relation `r` also holds for the pair `(μ m n₁, μ m n₂)`,
obtained from `(n₁, n₂)` by acting upon it by `m`.
If `m : M` and `h : r n₁ n₂`, then `CovariantClass.elim m h : r (μ m n₁) (μ m n₂)`.
-/
class
CovariantClass: (M : Type u_1) → (N : Type u_2) → (M → N → N) → (N → N → Prop) → Prop
Propwhere
/-- For all `m ∈ M` and all elements `n₁, n₂ ∈ N`, if the relation `r` holds for the pair
`(n₁, n₂)`, then, the relation `r` also holds for the pair `(μ m n₁, μ m n₂)` -/
protected
CovariantClass: (M : Type u_1) → (N : Type u_2) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
/-- Given an action `μ` of a Type `M` on a Type `N` and a relation `r` on `N`, informally, the
`ContravariantClass` says that "if the result of the action `μ` on a pair satisfies the
relation `r`, then the initial pair satisfied the relation `r`."
More precisely, the `ContravariantClass` is a class taking two Types `M N`, together with an
"action" `μ : M → N → N` and a relation `r : N → N → Prop`. Its unique field `elim` is the
assertion that for all `m ∈ M` and all elements `n₁, n₂ ∈ N`, if the relation `r` holds for the
pair `(μ m n₁, μ m n₂)` obtained from `(n₁, n₂)` by acting upon it by `m`, then, the relation
`r` also holds for the pair `(n₁, n₂)`.
If `m : M` and `h : r (μ m n₁) (μ m n₂)`, then `ContravariantClass.elim m h : r n₁ n₂`.
-/
class
Propwhere
/-- For all `m ∈ M` and all elements `n₁, n₂ ∈ N`, if the relation `r` holds for the
pair `(μ m n₁, μ m n₂)` obtained from `(n₁, n₂)` by acting upon it by `m`, then, the relation
`r` also holds for the pair `(n₁, n₂)`. -/
protected
act_rel_act_of_rel: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [inst : CovariantClassMNμr] (m : M) {a b : N},
rab → r (μma) (μmb)
act_rel_act_of_rel: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [inst : CovariantClassMNμr] (m : M) {a b : N},
rab → r (μma) (μmb)
M: Type ?u.747 N: Type u_1 μ: M → N → N r: N → N → Prop inst✝¹: CovariantClassMNμr inst✝: GroupN h: CovariantNN (fun xx_1 => x*x_1) r a, b, c: N bc: r ((fun xx_1 => x*x_1) ab) ((fun xx_1 => x*x_1) ac)
M: Type ?u.747 N: Type u_1 μ: M → N → N r: N → N → Prop inst✝¹: CovariantClassMNμr inst✝: GroupN h: CovariantNN (fun xx_1 => x*x_1) r a, b, c: N bc: r ((fun xx_1 => x*x_1) ab) ((fun xx_1 => x*x_1) ac)
refine_1
rbc
M: Type ?u.747 N: Type u_1 μ: M → N → N r: N → N → Prop inst✝¹: CovariantClassMNμr inst✝: GroupN h: CovariantNN (fun xx_1 => x*x_1) r a, b, c: N bc: r ((fun xx_1 => x*x_1) ab) ((fun xx_1 => x*x_1) ac)
M: Type ?u.747 N: Type u_1 μ: M → N → N r: N → N → Prop inst✝¹: CovariantClassMNμr inst✝: GroupN h: CovariantNN (fun xx_1 => x*x_1) r a, b, c: N bc: r ((fun xx_1 => x*x_1) ab) ((fun xx_1 => x*x_1) ac)
refine_1
rbc
M: Type ?u.747 N: Type u_1 μ: M → N → N r: N → N → Prop inst✝¹: CovariantClassMNμr inst✝: GroupN h: CovariantNN (fun xx_1 => x*x_1) r a, b, c: N bc: r ((fun xx_1 => x*x_1) ab) ((fun xx_1 => x*x_1) ac)
M: Type ?u.747 N: Type u_1 μ: M → N → N r: N → N → Prop inst✝¹: CovariantClassMNμr inst✝: GroupN h: CovariantNN (fun xx_1 => x*x_1) r a, b, c: N bc: r ((fun xx_1 => x*x_1) ab) ((fun xx_1 => x*x_1) ac)
refine_1
rbc
M: Type ?u.747 N: Type u_1 μ: M → N → N r: N → N → Prop inst✝¹: CovariantClassMNμr inst✝: GroupN h: CovariantNN (fun xx_1 => x*x_1) r a, b, c: N bc: r ((fun xx_1 => x*x_1) ab) ((fun xx_1 => x*x_1) ac)
M: Type ?u.747 N: Type u_1 μ: M → N → N r: N → N → Prop inst✝¹: CovariantClassMNμr inst✝: GroupN h: CovariantNN (fun xx_1 => x*x_1) r a, b, c: N bc: r ((fun xx_1 => x*x_1) ab) ((fun xx_1 => x*x_1) ac)
M: Type ?u.747 N: Type u_1 μ: M → N → N r: N → N → Prop inst✝¹: CovariantClassMNμr inst✝: GroupN h: CovariantNN (fun xx_1 => x*x_1) r a, b, c: N bc: r ((fun xx_1 => x*x_1) ab) ((fun xx_1 => x*x_1) ac)
act_rel_of_rel_of_act_rel: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [inst : CovariantClassMNμr] [inst : IsTransNr]
(m : M) {a b c : N}, rab → r (μmb) c → r (μma) c
_root_.trans: ∀ {α : Type ?u.2752} {r : α → α → Prop} [inst : IsTransαr] {a b c : α}, rab → rbc → rac
_root_.trans (
act_rel_act_of_rel: ∀ {M : Type ?u.2783} {N : Type ?u.2782} {μ : M → N → N} {r : N → N → Prop} [inst : CovariantClassMNμr] (m : M)
{a b : N}, rab → r (μma) (μmb)
act_rel_act_of_rel
m: M
m
ab: rab
ab)
rl: r (μmb) c
rl#align act_rel_of_rel_of_act_rel
act_rel_of_rel_of_act_rel: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [inst : CovariantClassMNμr] [inst : IsTransNr]
(m : M) {a b c : N}, rab → r (μmb) c → r (μma) c
_root_.trans: ∀ {α : Type ?u.2905} {r : α → α → Prop} [inst : IsTransαr] {a b c : α}, rab → rbc → rac
_root_.trans
rr: rc (μma)
rr (
act_rel_act_of_rel: ∀ {M : Type ?u.2938} {N : Type ?u.2937} {μ : M → N → N} {r : N → N → Prop} [inst : CovariantClassMNμr] (m : M)
{a b : N}, rab → r (μma) (μmb)
act_rel_act_of_rel
_: ?m.2939
_
ab: rab
ab)
#align rel_act_of_rel_of_rel_act
rel_act_of_rel_of_rel_act: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [inst : CovariantClassMNμr] [inst : IsTransNr]
(m : M) {a b c : N}, rab → rc (μma) → rc (μmb)
rel_act_of_rel_of_rel_actend Trans
end Covariant
-- Lemma with 4 elements.
section MEqN
variable {
_root_.trans: ∀ {α : Type ?u.3184} {r : α → α → Prop} [inst : IsTransαr] {a b c : α}, rab → rbc → rac
_root_.trans (@
act_rel_act_of_rel: ∀ {M : Type ?u.3215} {N : Type ?u.3214} {μ : M → N → N} {r : N → N → Prop} [inst : CovariantClassMNμr] (m : M)
{a b : N}, rab → r (μma) (μmb)
act_rel_act_of_rel: ∀ {M : Type ?u.3276} {N : Type ?u.3275} {μ : M → N → N} {r : N → N → Prop} [inst : CovariantClassMNμr] (m : M)
{a b : N}, rab → r (μma) (μmb)
act_rel_act_of_rel
b: N
b
cd: rcd
cd)
#align act_rel_act_of_rel_of_rel
act_rel_act_of_rel_of_rel: ∀ {N : Type u_1} {r : N → N → Prop} {mu : N → N → N} [inst : IsTransNr] [i : CovariantClassNNmur]
[i' : CovariantClassNN (swapmu) r] {a b c d : N}, rab → rcd → r (muac) (mubd)
rel_of_act_rel_act: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [inst : ContravariantClassMNμr] (m : M)
{a b : N}, r (μma) (μmb) → rab
rel_of_act_rel_act: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [inst : ContravariantClassMNμr] (m : M)
{a b : N}, r (μma) (μmb) → rab
act_rel_of_act_rel_of_rel_act_rel: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [inst : ContravariantClassMNμr]
[inst : IsTransNr] (m : M) {a b c : N}, r (μma) b → r (μmb) (μmc) → r (μma) c
_root_.trans: ∀ {α : Type ?u.3568} {r : α → α → Prop} [inst : IsTransαr] {a b c : α}, rab → rbc → rac
_root_.trans
ab: r (μma) b
ab (
rel_of_act_rel_act: ∀ {M : Type ?u.3601} {N : Type ?u.3600} {μ : M → N → N} {r : N → N → Prop} [inst : ContravariantClassMNμr] (m : M)
{a b : N}, r (μma) (μmb) → rab
rel_of_act_rel_act
m: M
m
rl: r (μmb) (μmc)
rl)
#align act_rel_of_act_rel_of_rel_act_rel
act_rel_of_act_rel_of_rel_act_rel: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [inst : ContravariantClassMNμr]
[inst : IsTransNr] (m : M) {a b c : N}, r (μma) b → r (μmb) (μmc) → r (μma) c
act_rel_of_act_rel_of_rel_act_reltheorem
rel_act_of_act_rel_act_of_rel_act: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [inst : ContravariantClassMNμr]
[inst : IsTransNr] (m : M) {a b c : N}, r (μma) (μmb) → rb (μmc) → ra (μmc)
_root_.trans: ∀ {α : Type ?u.3725} {r : α → α → Prop} [inst : IsTransαr] {a b c : α}, rab → rbc → rac
_root_.trans (
rel_of_act_rel_act: ∀ {M : Type ?u.3756} {N : Type ?u.3755} {μ : M → N → N} {r : N → N → Prop} [inst : ContravariantClassMNμr] (m : M)
{a b : N}, r (μma) (μmb) → rab
rel_of_act_rel_act
m: M
m
ab: r (μma) (μmb)
ab)
rr: rb (μmc)
rr#align rel_act_of_act_rel_act_of_rel_act
rel_act_of_act_rel_act_of_rel_act: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [inst : ContravariantClassMNμr]
[inst : IsTransNr] (m : M) {a b c : N}, r (μma) (μmb) → rb (μmc) → ra (μmc)
rel_act_of_act_rel_act_of_rel_actend Trans
end Contravariant
section Monotone
variable {
Covariant.monotone_of_const: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} [inst : PreorderN] [inst_1 : CovariantClassMNμfun xx_1 => x≤x_1]
(m : M), Monotone (μm)
Covariant.monotone_of_const
/-- A monotone function remains monotone when composed with the partial application
of a covariant operator. E.g., `∀ (m : ℕ), Monotone f → Monotone (λ n, f (m + n))`. -/
theorem
Covariant.monotone_of_const: ∀ {M : Type ?u.4211} {N : Type ?u.4212} {μ : M → N → N} [inst : PreorderN]
[inst_1 : CovariantClassMNμfun xx_1 => x≤x_1] (m : M), Monotone (μm)
Covariant.monotone_of_const
m: M
m
x: ?m.4202
x)
#align monotone.covariant_of_const
Monotone.covariant_of_const: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {α : Type u_3} [inst : Preorderα] [inst_1 : PreorderN] {f : N → α}
[inst_2 : CovariantClassMNμfun xx_1 => x≤x_1], Monotonef → ∀ (m : M), Monotonefun n => f (μmn)
Monotone.covariant_of_const
/-- Same as `Monotone.covariant_of_const`, but with the constant on the other side of
the operator. E.g., `∀ (m : ℕ), Monotone f → Monotone (λ n, f (n + m))`. -/
theorem
M: Type u_2 N: Type u_1 μ: M → N → N r: N → N → Prop inst✝: PartialOrderN h: ContravariantMNμfun xx_1 => x≤x_1 a: M b, c: N bc: (fun xx_1 => x<x_1) (μab) (μac)
covariant_lt_iff_contravariant_le
-- Porting note: `covariant_flip_mul_iff` used to use the `IsSymmOp` typeclass from Lean 3 core.
-- To avoid it, we prove the relevant lemma here.
@[