smul by invertible element.

Stream: Is there code for X?

[Christopher Hoskin]

Does a lemma like invOf_smul_eq_iff_eq_smul below already exist in Mathlib4? I looked expecting to find something like it, but failed.

import Mathlib.Algebra.Invertible.Defs
import Mathlib.Algebra.Module.Basic

variable {R : Type*} {M : Type*}

variable [Semiring R] [AddCommMonoid M] [Module R M]

@[simp]
theorem invOf_smul_self_smul (r : R) [Invertible r] {a : M} : ⅟r • r • a = a := by
  rw [← smul_assoc, smul_eq_mul, invOf_mul_self', one_smul]

-- c.f. mul_invOf_self_assoc
theorem smul_invOf_self_assoc (r : R) [Invertible r] {a : M} : r • (⅟ r • a) = a := by
  rw [← smul_assoc, smul_eq_mul, mul_invOf_self, one_smul]

-- c.f. mul_left_inj_of_invertible
theorem smul_inj_of_invertible (r : R) [Invertible r] {a b : M} : r • a = r • b ↔ a = b :=
  ⟨fun h => by simpa using congr_arg (⅟r • ·) h, congr_arg (_ • ·)⟩

-- c.f. invOf_mul_eq_iff_eq_mul_left
theorem invOf_smul_eq_iff_eq_smul (r : R) [Invertible r] {a b : M} :
    ⅟r • a = b ↔ a = r • b := by
  rw [← smul_inj_of_invertible (r := r), smul_invOf_self_assoc]

Thanks!

Christopher

[Jireh Loreaux]

We certainly have them for r : Rˣ which is the more canonical spelling. Is there a reason in particular you are opting for Invertible r?

[Christopher Hoskin]

[Invertible (2 : R)] is the formulation in the file I was working on:

https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/LinearAlgebra/QuadraticForm/Basic.lean#L986

[Jireh Loreaux]

in that case I would lift 2 to Rˣ.

[Eric Wieser]

We probably don't want the third one, because:

theorem smul_inj_of_invertible (r : R) [Invertible r] {a b : M} : r • a = r • b ↔ a = b :=
  IsUnit.smul_left_cancel (isUnit_of_invertible _)

[Eric Wieser]

I think all the ones about invOf are worth having

[Jireh Loreaux]

Then you have access to docs#inv_smul_smul and all the declarations around there.

[Eric Wieser]

Though there should be a one-lemma proof in terms of theUnits spelling

[Eric Wieser]

@[simp]
theorem invOf_smul_smul (r : R) [Invertible r] (a : M) : ⅟r • r • a = a :=
  inv_smul_smul (unitOfInvertible r) _

theorem smul_invOf_smul (r : R) [Invertible r] (a : M) : r • (⅟ r • a) = a :=
  smul_inv_smul (unitOfInvertible r) _

theorem invOf_smul_eq_iff (r : R) [Invertible r] {a b : M} :
    ⅟r • a = b ↔ a = r • b :=
  inv_smul_eq_iff (a := unitOfInvertible r)

[Eric Wieser]

do we not have docs#smul_inv_smul ?

[Christopher Hoskin]

Jireh Loreaux said:

in that case I would lift 2 to Rˣ.

Mathlib sees R as an additive monoid, but does it also see it as a multiplicative monoid?

[Jireh Loreaux]

Sure, it's a Semiring.

[Christopher Hoskin]

Jireh Loreaux said:

Sure, it's a Semiring.

I was trying variable [IsUnit (2 : R)]instead of [Invertible r] - but I must be barking up the wrong tree.

[Jireh Loreaux]

You can do #synth Monoid R (variable {R: Type*} [Semiring R] in scope) to check.

[Jireh Loreaux]

Note: docs#IsUnit and docs#Units are not the same thing (although they're closely related).

[Jireh Loreaux]

I'm not necessarily saying you should replace your [Invertible (2 : R)] hypotheses, just that in the proofs you can upgrade to Rˣ (as Eric has shown above) to get access to the fact that you have a group action.

[Christopher Hoskin]

Eric Wieser said:

@[simp]
theorem invOf_smul_smul (r : R) [Invertible r] (a : M) : ⅟r • r • a = a :=
  inv_smul_smul (unitOfInvertible r) _

theorem smul_invOf_smul (r : R) [Invertible r] (a : M) : r • (⅟ r • a) = a :=
  smul_inv_smul (unitOfInvertible r) _

theorem invOf_smul_eq_iff (r : R) [Invertible r] {a b : M} :
    ⅟r • a = b ↔ a = r • b :=
  inv_smul_eq_iff (a := unitOfInvertible r)

Would a PR adding these results into Algebra/Module/Basic be a worthwhile thing?

[Eric Wieser]

These should be stated about monoid actions not modules

[Eric Wieser]

Those lemmas probably belong next to the group lemmas

[Christopher Hoskin]

Eric Wieser said:

These should be stated about monoid actions not modules

Do you mean in GroupTheory/GroupAction/Group?

[Eric Wieser]

That sounds good to me

[Eric Wieser]

There may be other lemmas you can duplicate for invOf in the same file

[Christopher Hoskin]

How about this: https://github.com/leanprover-community/mathlib4/pull/9972 ?

[Eric Wieser]

Your new instance looks like it duplicates docs#Units.instMulAction