mathlib documentation

algebra.covariant_and_contravariant

Covariants and contravariants #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. https://github.com/leanprover-community/mathlib4/pull/467 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

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
@[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
@[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
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)
@[protected, instance]
def group.covconv {N : Type u_2} {r : N N Prop} [group N] [covariant_class N N has_mul.mul r] :
@[protected, instance]
@[protected, instance]
@[protected, instance]
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] :
theorem covariant_le_iff_contravariant_lt (M : Type u_1) (N : Type u_2) (μ : M N N) [linear_order N] :
theorem covariant_lt_iff_contravariant_le (M : Type u_1) (N : Type u_2) (μ : M N N) [linear_order N] :
theorem covariant_flip_mul_iff (N : Type u_2) (r : N N Prop) [comm_semigroup N] :