mathlib documentation

algebra.covariant_and_contravariant

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

covariant_class models the implication a ≤ b → c * a ≤ c * b (multiplication is monotone),
contravariant_class models the implication a * b < a * c → b < c.

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.

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

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

contravariant M N μ r = ∀ (m : M) {n₁ n₂ : N}, r (μ m n₁) (μ m n₂) → r n₁ n₂

@[class]

structure covariant_class (M : Type u_1) (N : Type u_2) (μ : M → N → N) (r : N → N → Prop) :

Prop

elim : covariant M N μ r

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

@[class]

structure contravariant_class (M : Type u_1) (N : Type u_2) (μ : M → N → N) (r : N → N → Prop) :

Prop

elim : contravariant M N μ r

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

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

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)

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)

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)

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

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

theorem 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

theorem 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

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

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)

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)

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

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

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)

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.

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

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

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

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'

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

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

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

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

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

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

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

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

@[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

@[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

@[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

@[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

@[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

@[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

@[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

@[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

@[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

@[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

@[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

@[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

@[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

@[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

@[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

@[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

@[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

@[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

@[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

@[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