mathlib3 documentation

algebra.covariant_and_contravariant

Covariants and contravariants #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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, covariant_class and contravariant_class:

Since co(ntra)variant_class 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 [ordered_cancel_monoid M], into three typeclasses, e.g. [left_cancel_semigroup M] [partial_order M] [covariant_class 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)variant_class assumptions together. Indeed, the usual ordered typeclasses arise from assuming the pair [covariant_class M M (*) (≤)] [contravariant_class M M (*) (<)] on top of order/algebraic assumptions.

A formal remark is that normally covariant_class uses the (≤)-relation, while contravariant_class 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

[semigroup α] [partial_order α] [contravariant_class α α (*) (≤)] => left_cancel_semigroup α

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.

source
def covariant (M : Type u_1) (N : Type u_2) (μ : M → N → N) (r : N → N → Prop) :
Prop

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 covariant_class doc-string for its meaning.

Equations
  • covariant M N μ r = ∀ (m : M) {n₁ n₂ : N}, r n₁ n₂ → r (μ m n₁) (μ m n₂)
source
def contravariant (M : Type u_1) (N : Type u_2) (μ : M → N → N) (r : N → N → Prop) :
Prop

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 contravariant_class doc-string for its meaning.

Equations
source
@[class]
structure covariant_class (M : Type u_1) (N : Type u_2) (μ : M → N → N) (r : N → N → Prop) :
Prop

Given an action μ of a Type M on a Type N and a relation r on N, informally, the covariant_class says that "the action μ preserves the relation r."

More precisely, the covariant_class 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 covariant_class.elim m h : r (μ m n₁) (μ m n₂).

Instances of this typeclass
source
@[class]
structure contravariant_class (M : Type u_1) (N : Type u_2) (μ : M → N → N) (r : N → N → Prop) :
Prop

Given an action μ of a Type M on a Type N and a relation r on N, informally, the contravariant_class 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 contravariant_class 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 contravariant_class.elim m h : r n₁ n₂.

Instances of this typeclass
source
theorem rel_iff_cov (M : Type u_1) (N : Type u_2) (μ : M → N → N) (r : N → N → Prop) [covariant_class M N μ r] [contravariant_class M N μ r] (m : M) {a b : N} :
r (μ m a) (μ m b) ↔ r a b
source
theorem covariant.flip {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} (h : covariant M N μ r) :
covariant M N μ (flip r)
source
theorem contravariant.flip {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} (h : contravariant M N μ r) :
contravariant M N μ (flip r)
source
theorem act_rel_act_of_rel {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [covariant_class M N μ r] (m : M) {a b : N} (ab : r a b) :
r (μ m a) (μ m b)
source
theorem add_group.covariant_iff_contravariant {N : Type u_2} {r : N → N → Prop} [add_group N] :
covariant N N has_add.add r ↔ contravariant N N has_add.add r
source
theorem group.covariant_iff_contravariant {N : Type u_2} {r : N → N → Prop} [group N] :
covariant N N has_mul.mul r ↔ contravariant N N has_mul.mul r
source
@[protected, instance]
def group.covconv {N : Type u_2} {r : N → N → Prop} [group N] [covariant_class N N has_mul.mul r] :
contravariant_class N N has_mul.mul r
source
@[protected, instance]
def add_group.covconv {N : Type u_2} {r : N → N → Prop} [add_group N] [covariant_class N N has_add.add r] :
contravariant_class N N has_add.add r
source
theorem group.covariant_swap_iff_contravariant_swap {N : Type u_2} {r : N → N → Prop} [group N] :
covariant N N (function.swap has_mul.mul) r ↔ contravariant N N (function.swap has_mul.mul) r
source
theorem add_group.covariant_swap_iff_contravariant_swap {N : Type u_2} {r : N → N → Prop} [add_group N] :
covariant N N (function.swap has_add.add) r ↔ contravariant N N (function.swap has_add.add) r
source
@[protected, instance]
def group.covconv_swap {N : Type u_2} {r : N → N → Prop} [group N] [covariant_class N N (function.swap has_mul.mul) r] :
contravariant_class N N (function.swap has_mul.mul) r
source
@[protected, instance]
def add_group.covconv_swap {N : Type u_2} {r : N → N → Prop} [add_group N] [covariant_class N N (function.swap has_add.add) r] :
contravariant_class N N (function.swap has_add.add) r
source
theorem act_rel_of_rel_of_act_rel {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [covariant_class M N μ r] [is_trans N r] (m : M) {a b c : N} (ab : r a b) (rl : r (μ m b) c) :
r (μ m a) c
source
theorem rel_act_of_rel_of_rel_act {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [covariant_class M N μ r] [is_trans N r] (m : M) {a b c : N} (ab : r a b) (rr : r c (μ m a)) :
r c (μ m b)
source
theorem act_rel_act_of_rel_of_rel {N : Type u_2} {r : N → N → Prop} {mu : N → N → N} [is_trans N r] [covariant_class N N mu r] [covariant_class N N (function.swap mu) r] {a b c d : N} (ab : r a b) (cd : r c d) :
r (mu a c) (mu b d)
source
theorem rel_of_act_rel_act {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [contravariant_class M N μ r] (m : M) {a b : N} (ab : r (μ m a) (μ m b)) :
r a b
source
theorem act_rel_of_act_rel_of_rel_act_rel {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [contravariant_class M N μ r] [is_trans N r] (m : M) {a b c : N} (ab : r (μ m a) b) (rl : r (μ m b) (μ m c)) :
r (μ m a) c
source
theorem rel_act_of_act_rel_act_of_rel_act {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [contravariant_class M N μ r] [is_trans N r] (m : M) {a b c : N} (ab : r (μ m a) (μ m b)) (rr : r b (μ m c)) :
r a (μ m c)
source
theorem covariant.monotone_of_const {M : Type u_1} {N : Type u_2} {μ : M → N → N} [preorder N] [covariant_class M N μ has_le.le] (m : M) :
monotone (μ m)

The partial application of a constant to a covariant operator is monotone.

source
theorem monotone.covariant_of_const {M : Type u_1} {N : Type u_2} {μ : M → N → N} {α : Type u_3} [preorder α] [preorder N] {f : N → α} [covariant_class M N μ has_le.le] (hf : monotone f) (m : M) :
monotone (λ (n : N), f (μ m n))

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)).

source
theorem monotone.covariant_of_const' {N : Type u_2} {α : Type u_3} [preorder α] [preorder N] {f : N → α} {μ : N → N → N} [covariant_class N N (function.swap μ) has_le.le] (hf : monotone f) (m : N) :
monotone (λ (n : N), f (μ n m))

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)).

source
theorem antitone.covariant_of_const {M : Type u_1} {N : Type u_2} {μ : M → N → N} {α : Type u_3} [preorder α] [preorder N] {f : N → α} [covariant_class M N μ has_le.le] (hf : antitone f) (m : M) :
antitone (λ (n : N), f (μ m n))

Dual of monotone.covariant_of_const

source
theorem antitone.covariant_of_const' {N : Type u_2} {α : Type u_3} [preorder α] [preorder N] {f : N → α} {μ : N → N → N} [covariant_class N N (function.swap μ) has_le.le] (hf : antitone f) (m : N) :
antitone (λ (n : N), f (μ n m))

Dual of monotone.covariant_of_const'

source
theorem covariant_le_of_covariant_lt (M : Type u_1) (N : Type u_2) (μ : M → N → N) [partial_order N] :
covariant M N μ has_lt.lt → covariant M N μ has_le.le
source
theorem contravariant_lt_of_contravariant_le (M : Type u_1) (N : Type u_2) (μ : M → N → N) [partial_order N] :
contravariant M N μ has_le.le → contravariant M N μ has_lt.lt
source
theorem covariant_le_iff_contravariant_lt (M : Type u_1) (N : Type u_2) (μ : M → N → N) [linear_order N] :
covariant M N μ has_le.le ↔ contravariant M N μ has_lt.lt
source
theorem covariant_lt_iff_contravariant_le (M : Type u_1) (N : Type u_2) (μ : M → N → N) [linear_order N] :
covariant M N μ has_lt.lt ↔ contravariant M N μ has_le.le
source
theorem covariant_flip_mul_iff (N : Type u_2) (r : N → N → Prop) [comm_semigroup N] :
covariant N N (flip has_mul.mul) r ↔ covariant N N has_mul.mul r
source
theorem covariant_flip_add_iff (N : Type u_2) (r : N → N → Prop) [add_comm_semigroup N] :
covariant N N (flip has_add.add) r ↔ covariant N N has_add.add r
source
theorem contravariant_flip_mul_iff (N : Type u_2) (r : N → N → Prop) [comm_semigroup N] :
contravariant N N (flip has_mul.mul) r ↔ contravariant N N has_mul.mul r
source
theorem contravariant_flip_add_iff (N : Type u_2) (r : N → N → Prop) [add_comm_semigroup N] :
contravariant N N (flip has_add.add) r ↔ contravariant N N has_add.add r
source
@[protected, instance]
def contravariant_mul_lt_of_covariant_mul_le (N : Type u_2) [has_mul N] [linear_order N] [covariant_class N N has_mul.mul has_le.le] :
contravariant_class N N has_mul.mul has_lt.lt
source
@[protected, instance]
def contravariant_add_lt_of_covariant_add_le (N : Type u_2) [has_add N] [linear_order N] [covariant_class N N has_add.add has_le.le] :
contravariant_class N N has_add.add has_lt.lt
source
@[protected, instance]
def covariant_add_lt_of_contravariant_add_le (N : Type u_2) [has_add N] [linear_order N] [contravariant_class N N has_add.add has_le.le] :
covariant_class N N has_add.add has_lt.lt
source
@[protected, instance]
def covariant_mul_lt_of_contravariant_mul_le (N : Type u_2) [has_mul N] [linear_order N] [contravariant_class N N has_mul.mul has_le.le] :
covariant_class N N has_mul.mul has_lt.lt
source
@[protected, instance]
def covariant_swap_add_le_of_covariant_add_le (N : Type u_2) [add_comm_semigroup N] [has_le N] [covariant_class N N has_add.add has_le.le] :
covariant_class N N (function.swap has_add.add) has_le.le
source
@[protected, instance]
def covariant_swap_mul_le_of_covariant_mul_le (N : Type u_2) [comm_semigroup N] [has_le N] [covariant_class N N has_mul.mul has_le.le] :
covariant_class N N (function.swap has_mul.mul) has_le.le
source
@[protected, instance]
def contravariant_swap_mul_le_of_contravariant_mul_le (N : Type u_2) [comm_semigroup N] [has_le N] [contravariant_class N N has_mul.mul has_le.le] :
contravariant_class N N (function.swap has_mul.mul) has_le.le
source
@[protected, instance]
def contravariant_swap_add_le_of_contravariant_add_le (N : Type u_2) [add_comm_semigroup N] [has_le N] [contravariant_class N N has_add.add has_le.le] :
contravariant_class N N (function.swap has_add.add) has_le.le
source
@[protected, instance]
def contravariant_swap_add_lt_of_contravariant_add_lt (N : Type u_2) [add_comm_semigroup N] [has_lt N] [contravariant_class N N has_add.add has_lt.lt] :
contravariant_class N N (function.swap has_add.add) has_lt.lt
source
@[protected, instance]
def contravariant_swap_mul_lt_of_contravariant_mul_lt (N : Type u_2) [comm_semigroup N] [has_lt N] [contravariant_class N N has_mul.mul has_lt.lt] :
contravariant_class N N (function.swap has_mul.mul) has_lt.lt
source
@[protected, instance]
def covariant_swap_mul_lt_of_covariant_mul_lt (N : Type u_2) [comm_semigroup N] [has_lt N] [covariant_class N N has_mul.mul has_lt.lt] :
covariant_class N N (function.swap has_mul.mul) has_lt.lt
source
@[protected, instance]
def covariant_swap_add_lt_of_covariant_add_lt (N : Type u_2) [add_comm_semigroup N] [has_lt N] [covariant_class N N has_add.add has_lt.lt] :
covariant_class N N (function.swap has_add.add) has_lt.lt
source
@[protected, instance]
def left_cancel_semigroup.covariant_mul_lt_of_covariant_mul_le (N : Type u_2) [left_cancel_semigroup N] [partial_order N] [covariant_class N N has_mul.mul has_le.le] :
covariant_class N N has_mul.mul has_lt.lt
source
@[protected, instance]
def add_left_cancel_semigroup.covariant_add_lt_of_covariant_add_le (N : Type u_2) [add_left_cancel_semigroup N] [partial_order N] [covariant_class N N has_add.add has_le.le] :
covariant_class N N has_add.add has_lt.lt
source
@[protected, instance]
def right_cancel_semigroup.covariant_swap_mul_lt_of_covariant_swap_mul_le (N : Type u_2) [right_cancel_semigroup N] [partial_order N] [covariant_class N N (function.swap has_mul.mul) has_le.le] :
covariant_class N N (function.swap has_mul.mul) has_lt.lt
source
@[protected, instance]
def add_right_cancel_semigroup.covariant_swap_add_lt_of_covariant_swap_add_le (N : Type u_2) [add_right_cancel_semigroup N] [partial_order N] [covariant_class N N (function.swap has_add.add) has_le.le] :
covariant_class N N (function.swap has_add.add) has_lt.lt
source
@[protected, instance]
def add_left_cancel_semigroup.contravariant_add_le_of_contravariant_add_lt (N : Type u_2) [add_left_cancel_semigroup N] [partial_order N] [contravariant_class N N has_add.add has_lt.lt] :
contravariant_class N N has_add.add has_le.le
source
@[protected, instance]
def left_cancel_semigroup.contravariant_mul_le_of_contravariant_mul_lt (N : Type u_2) [left_cancel_semigroup N] [partial_order N] [contravariant_class N N has_mul.mul has_lt.lt] :
contravariant_class N N has_mul.mul has_le.le
source
@[protected, instance]
def add_right_cancel_semigroup.contravariant_swap_add_le_of_contravariant_swap_add_lt (N : Type u_2) [add_right_cancel_semigroup N] [partial_order N] [contravariant_class N N (function.swap has_add.add) has_lt.lt] :
contravariant_class N N (function.swap has_add.add) has_le.le
source
@[protected, instance]
def right_cancel_semigroup.contravariant_swap_mul_le_of_contravariant_swap_mul_lt (N : Type u_2) [right_cancel_semigroup N] [partial_order N] [contravariant_class N N (function.swap has_mul.mul) has_lt.lt] :
contravariant_class N N (function.swap has_mul.mul) has_le.le