# mathlibdocumentation

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
• 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
• μ 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 : 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 : μ 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) [ μ r] [ μ 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 : N μ r) :
N μ (flip r)
theorem contravariant.flip {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} (h : μ r) :
μ (flip r)
theorem act_rel_act_of_rel {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [ μ 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] :
r r
theorem group.covariant_iff_contravariant {N : Type u_2} {r : N → N → Prop} [group N] :
r r
theorem group.covconv {N : Type u_2} {r : N → N → Prop} [group N] [ r] :
theorem add_group.covconv {N : Type u_2} {r : N → N → Prop} [add_group N] [ r] :
theorem act_rel_of_rel_of_act_rel {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [ μ r] [ 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} [ μ r] [ 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} [ r] [ mu r] [ (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} [ μ 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} [ μ r] [ 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} [ μ r] [ r] (m : M) {a b c : N} (ab : r (μ m a) (μ m b)) (rr : r b (μ m c)) :
r a (μ m c)
theorem covariant_le_of_covariant_lt (M : Type u_1) (N : Type u_2) (μ : M → N → N)  :
N μ has_lt.lt N μ has_le.le
theorem contravariant_lt_of_contravariant_le (M : Type u_1) (N : Type u_2) (μ : M → N → N)  :
μ has_le.le μ has_lt.lt
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)  :
N r r
theorem covariant_flip_add_iff (N : Type u_2) (r : N → N → Prop)  :
N r r
theorem contravariant_flip_mul_iff (N : Type u_2) (r : N → N → Prop)  :
r r
theorem contravariant_flip_add_iff (N : Type u_2) (r : N → N → Prop)  :
r r
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]
@[instance]