left/right unification

Stream: Is there code for X?

[Damiano Testa]

Dear All,

I am testing out whether what is below could be a compromise between allowing a mixture of "order-like conditions" and "monotonicity" conditions in a general setting. This is motivated by trying to prove lemmas about nnreal by working with linear_ordered_comm_group_with_zero.

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/linear_ordered_*noncomm*_group.28_with_zero.29

Since there are a lot of assumptions implicit in linear_ordered_comm_group_with_zero and making the whole poset of weakinings into typeclasses does not seem reasonable, I am trying to see if I can tweak the definitions and make do with a single extra class.

If this is already available, I would be more than happy to know! Otherwise, below are my experiments: I would welcome any comment!

Thanks!

import data.real.nnreal

open_locale nnreal

namespace lo

/--  A general predicate on two Types `α β`, together with an "action" `μ : α → β`, a relation
`r : β → β`, asserting that if the relation holds for the pair `(b₁, b₂)`, then it also holds
for the pair `(μ a b₁, μ a b₂) "acted-upon-by `a`". `-/
@[protect_proj]
class is_rel_action (α β : Type*) (μ : α → β → β) (r : β → β → Prop) : Prop :=
(mix : ∀ (a b₁ b₂), r b₁ b₂ → r (μ a b₁) (μ a b₂))

/--  This lemma shortens the name and makes explicit/implicit arguments that I imagine would appear
in normal use. -/
lemma mix {α β : Type*} {μ : α → β → β} {r : β → β → Prop} (h : is_rel_action α β μ r)
  (a : α) {b₁ b₂ : β} (bb : r b₁ b₂) : r (μ a b₁) (μ a b₂) :=
is_rel_action.mix a b₁ b₂ bb

/--  An example, exponentiation by a fixed natural number is monotone on `ℝ≥0`. -/
lemma nat.nnreal_pow_mono : is_rel_action ℕ ℝ≥0 (λ n x, x ^ n) (≤) :=
{ mix := λ p x y xy, canonically_ordered_semiring.pow_le_pow_of_le_left xy p }

/--  An example, exponentiation by a fixed `pnat` is strictly monotone on `ℝ≥0`. -/
lemma pnat.nnreal_pow_strict_mono : is_rel_action pnat ℝ≥0 (λ n x, x ^ n.val) (<) :=
{ mix := λ p x y xy, pow_lt_pow_of_lt_left xy (zero_le x) p.property }

/--  The previous lemma can now be used for the natural numbers that are positive. -/
lemma nat.nnreal_pow_strict_mono_of_pos {n : ℕ} (n0 : 0 < n) {x y : ℝ≥0} (xy : x < y) :
  x ^ n < y ^ n :=
begin
  lift n to pnat using n0,
  exact mix pnat.nnreal_pow_strict_mono _ xy,
end

/-- This is really closer to my intended application. -/
variables {G : Type*} [group G] [preorder G]

namespace left

/--  Assume that the action is by left-multiplication and the relation is an arbitrary preorder
on the group. -/
variable [ρ : is_rel_action G G (*) (≤)]
include ρ

/--  You get that multiplication on the left is monotone. -/
example {a b c : G} (h : b ≤ c) : a * b ≤ a * c :=
mix ρ a h

end left

namespace right

/--  If you start assuming that the action is by right-multiplication... -/
variables [ρ : is_rel_action G G (function.swap (*)) (≤)]
include ρ

/--  ... then you get that multiplication on the right is monotone. -/
example {a b c : G} (h : b ≤ c) : b * a ≤ c * a :=
mix ρ a h

end right

end lo

[Kevin Buzzard]

Is this close to the concept of a congruence relation?

[Damiano Testa]

I do not know: congruence relation, for me, evokes congruence modulo an integer. I will google for it!

[Kevin Buzzard]

I guess μ : α → β → β is just an indexed family of functions β → β

[Damiano Testa]

My only source is this wikipedia page:

https://en.wikipedia.org/wiki/Congruence_relation

From that page, it seems that there is an underlying "equivalence" going about. In the context in which I would like to apply this, the relation would be more an order relation. However, if the r in is_rel_action is an equivalence, then it may be very close!

Thanks for the pointer, Kevin!

[Kevin Buzzard]

docs#add_con (see the documentation there, or the module docstring in group_theory.congruence)

[Kevin Buzzard]

But it looks different, like how smul differs from mul.

[Damiano Testa]

Thanks Kevin! It does look very close, indeed!

I will see what I can recycle from add_con. For the intended application, it appears that it might work for one of left (or right) multiplication, but not the other, I think.

It might still be neat to have a lemma establishing exactly the relationship between the two: something like if \mu is left-multiplication and r is an equivalence, then we get an add_con (or something, hopefully close to this, but correct!).

[Damiano Testa]

Kevin, this compiles and should be saying that you can get a is_rel_action out of a con:

import group_theory.congruence

lemma add_con_rel {M : Type*} [has_mul M] (c : con M) : lo.is_rel_action M M (*) c.r :=
{ mix := λ a b₁ b₂ bb, c.mul' (con.refl _ _) bb }

[Eric Wieser]

(deleted)

[Damiano Testa]

Ok, this should complete the relationship between is_rel_action and con:

lemma add_con_rel {M : Type*} [has_mul M] (c : con M) :
  lo.is_rel_action M M (*) c.r :=
{ mix := λ a b₁ b₂ bb, c.mul' (con.refl _ _) bb }

lemma add_con_rel' {M : Type*} [has_mul M] (c : con M) :
  lo.is_rel_action M M (λ (a b : M), b * a) c.r :=
{ mix := λ a b₁ b₂ bb, c.mul' bb (con.refl _ _) }

lemma add_con_rel_converse {M : Type*} [has_mul M] [setoid M]
  (h : lo.is_rel_action M M (*) setoid.r)
  (h' : lo.is_rel_action M M (λ (a b : M), b * a) setoid.r) :
  con M :=
{ r := setoid.r,
  iseqv := iseqv,
  mul' := λ w x y z wx yz, begin
    have r1 : r (w * y) (w * z) := lo.mix h _ yz,
    have r2 : r (w * z) (x * z) := lo.mix h' _ wx,
    exact trans r1 r2,
  end }

or, more succintly,

lemma con_rel {M : Type*} [has_mul M] (c : con M) :
  lo.is_rel_action M M (*) c.r ∧ lo.is_rel_action M M (λ (a b : M), b * a) c.r :=
⟨{ mix := λ a _ _ bb, c.mul' (con.refl _ _) bb }, { mix := λ a _ _ bb, c.mul' bb (con.refl _ _) }⟩

lemma con_rel_converse {M : Type*} [has_mul M] [setoid M]
  (h : lo.is_rel_action M M (*) setoid.r ∧ lo.is_rel_action M M (λ (a b : M), b * a) setoid.r) :
  con M :=
{ r := setoid.r,
  iseqv := iseqv,
  mul' := λ w x y z wx yz, trans (lo.mix h.1 _ yz) (lo.mix h.2 _ wx) }