new fashion ordered stuff

Stream: general

[Patrick Massot]

I'm trying to port old code from the perfectoid project and I need help from people who know how to handle the new ordered algebra lemmas. Nowadays, how do you prove:

import algebra.order.with_zero

variables (Γ : Type*) [linear_ordered_comm_group_with_zero Γ]

example (a : Γ) (γ γ' : units Γ) (vy_lt : a < γ'⁻¹ * γ) : (γ' : Γ) * a < γ :=
sorry

[Johan Commelin]

We are missing some lemmas :sad:

variables {Γ : Type*} [linear_ordered_comm_group_with_zero Γ]

variables {a b c : Γ}

lemma le_of_le_mul_left (h : c ≠ 0) (hab : c * a ≤ c * b) : a ≤ b :=
by simpa only [inv_mul_cancel_left₀ h] using (mul_le_mul_left' hab c⁻¹)

lemma mul_lt_left₀ (c : Γ) (h : a < b) (hc : c ≠ 0) : c * a < c * b :=
by { contrapose! h, exact le_of_le_mul_left hc h }

example (a : Γ) (γ γ' : units Γ) (vy_lt : a < γ'⁻¹ * γ) : (γ' : Γ) * a < γ :=
calc (γ' : Γ) * a < γ' * (γ'⁻¹ * γ) : mul_lt_left₀ _ vy_lt γ'.ne_zero
... = γ : mul_inv_cancel_left₀ γ'.ne_zero _

[Patrick Massot]

In the mean time I got away with

example (a : Γ) (γ γ' : units Γ) (vy_lt : a < γ'⁻¹ * γ) : (γ' : Γ) * a < γ :=
begin
  rw mul_comm at *,
  simpa using mul_inv_lt_of_lt_mul' vy_lt
end

[Patrick Massot]

But indeed it seems we are missing lemmas here.

[Patrick Massot]

And I'm a bit disappointed we don't have more general lemmas.

[Eric Wieser]

Do we have a lemma for

example (a : Γ) (γ γ' : units Γ) (vy_lt : a < γ'⁻¹ • γ) : γ' • a < γ :=
sorry

Which is defeq?

[Patrick Massot]

failed to synthesize type class instance for
Γ : Type u_1,
_inst_1 : linear_ordered_comm_group_with_zero Γ,
a : Γ,
γ γ' : units Γ,
vy_lt : a < γ'⁻¹ • ↑γ
⊢ has_scalar (units Γ) Γ

[Yaël Dillies]

I think you're past the current limit of the order refactor.

[Eric Wieser]

I think you're just missing an import for that action, group_theory.group_action.units

[Eric Wieser]

docs#units.mul_action

[Patrick Massot]

With this import, the statement makes sense but library_search founds nothing

[Eric Wieser]

I think it might make sense to have a typeclass along the lines of

class group.ordered_smul {G α : Type*} [group G] [has_scalar G α] :=
(smul_le_iff : g • x ≤ y ↔ x ≤ g⁻¹ • y)

Which is true for the pointwise action on sets and subobjects, as well as your case. Maybe @Damiano Testa can point out we already have that in one of the new co(ntra)variant_classes?

[Yaël Dillies]

Isn't it precisely the multiplicative scalar version of docs#has_ordered_sub?