Working with `invertible`

Stream: general

[Eric Wieser]

Does anyone have any tips for working with invertible? I always find it really awkward to prove even the most basic facts, such as

import algebra.invertible

variables {R : Type*} [semiring R] (x y : R)

/-- `1 + ⅟x` is invertible if `x + 1` is -/
def invertible_one_add_inv_of [invertible x] [invertible (x + 1)] : invertible (1 + ⅟x) :=
begin
  suffices : invertible ((x + 1) * ⅟x),
  { refine this.copy _ _,
    rw [add_one_mul x, mul_inv_of_self], },
  letI : invertible ((x + 1) * ⅟x) := invertible_mul _ _,
  refine ((unit_of_invertible ((x + 1) * ⅟x)).copy _ rfl (x * ⅟(x + 1)) _).invertible,
  dsimp,
  rw [inv_of_mul, inv_of_inv_of],
end

lemma one_add_inv_of [invertible x] [invertible (x + 1)] [invertible (1 + ⅟x)] :
  ⅟(1 + ⅟x) = x*⅟(x + 1) :=
begin
  letI := invertible_one_add_inv_of x,
  convert (rfl : ⅟(1 + ⅟x) = _),
end

Going further and showing invertible (⅟x + 1) ≃ invertible (1 + x) (proof: it's just multiplication by the unit units_of_invertible x) is even more annoying

[Reid Barton]

Yeah type classes make things hard :shrug:

[Eric Wieser]

A slightly better statement might be

/-- `1 + u` is invertible if `u + 1` is -/
def units.invertible_one_add_inv_of (u : Rˣ) [invertible (u + 1 : R)] : invertible (1 + ↑u⁻¹ : R) :=
begin
  suffices : invertible ((u + 1) * ↑u⁻¹ : R),
  { refine this.copy _ _,
    rw [add_one_mul (u : R), units.mul_inv], },
  letI := (u⁻¹).invertible,
  letI : invertible ((u + 1) * ↑u⁻¹ : R) := invertible_mul _ _,
  refine ((unit_of_invertible ((u + 1) * ↑u⁻¹ : R)).copy _ rfl (u * ⅟(u + 1)) _).invertible,
  dsimp,
  rw [inv_of_mul, inv_of_units, inv_inv],
end

lemma units.one_add_inv_of (u : Rˣ) [invertible (u + 1 : R)] [invertible (1 + ↑u⁻¹ : R)] :
  ⅟(1 + ↑u⁻¹ : R) = u*⅟(u + 1) :=
begin
  letI := u.invertible_one_add_inv_of,
  convert (rfl : ⅟(1 + ↑u⁻¹ : R) = _),
end

but I don't see an obvious trick to help the proof

[Anne Baanen]

I believe the recommendation is to work in units and only at the last stage convert back to invertible. Since units has much more API, would that help here?

[Eric Wieser]

If I work with units, I need a hypothesis u2 = u + 1

[Eric Wieser]

So my statement becomes something like

example (h1 : ↑u2 = ↑u + 1) (h2 : ↑u3 = 1 + ↑u⁻¹) : ↑u3⁻¹ = ↑u * ↑u2⁻¹ := sorry

which no longer resembles ⅟(1 + ↑u⁻¹ : R) = u*⅟(u + 1) at all!

[Anne Baanen]

I see, and is_unit is not good if you want it to be computable.

[Eric Wieser]

That woul make the goal be ↑hu3.unit⁻¹ = ↑u * hu2.unit⁻¹ which seems almost as bad!

[Eric Wieser]

I guess you could prove it about ring.inverse; but then you need to separately prove that is_unit for the RHS implies is_unit for the LHS

[Eric Wieser]

The code around diagonal_invertible gives a demonstration of how invertible can be somewhat useful

[Eric Wieser]

In that it gives us is_unit (diagonal v) ↔ is_unit v and (diagonal v)⁻¹ = diagonal (ring.inverse v) mostly at the same time, without having to repeat the same algebra

[Eric Wieser]

#18849 is a somewhat nastier example

[Ruben Van de Velde]

Not sure if you like this better:

def invertible_one_add_inv_of [invertible x] [invertible (x + 1)] : invertible (1 + ⅟x) :=
begin
  refine ⟨x*⅟(x + 1), _, _⟩; nontriviality R,
  { rw [← (unit_of_invertible x)⁻¹.mul_right_inj, ← (unit_of_invertible x).mul_left_inj],
    simp only [coe_unit_of_invertible, mul_one, inv_of_mul_self, coe_inv_unit_of_invertible],
    calc ⅟ x * (x * ⅟ (x + 1) * (1 + ⅟ x)) * x
        = (⅟ x * x) * ⅟ (x + 1) * (x + ⅟ x * x) : by noncomm_ring
    ... = 1 : by simp },
  { rw [← mul_assoc, add_mul],
    simp },
end

[Kevin Buzzard]

import algebra.invertible

variables {R : Type*} [semiring R] (x y : R)

/-- `1 + ⅟x` is invertible if `x + 1` is -/
def invertible_one_add_inv_of [invertible x] [invertible (x + 1)] : invertible (1 + ⅟x) :=
begin
  convert invertible_mul (⅟x) (x + 1),
  simp [mul_add],
end

[Eric Wieser]

It doesn't count unless you also prove ⅟(1 + ⅟x) = x*⅟(x + 1)

[Kevin Buzzard]

lemma one_add_inv_of [invertible x] [invertible (x + 1)] [invertible (1 + ⅟x)] :
  ⅟(1 + ⅟x) = x*⅟(x + 1) :=
begin
  apply inv_of_eq_right_inv,
  simpa [add_mul] using mul_inv_of_self (x + 1),
end

[Kevin Buzzard]

a.k.a. "these things follow formally from properties of inverses"

[Eric Wieser]

I guess this works here because the proof is trivial in both cases, but in general you end up proving pretty much the same thing in the first and second declaration

[Filippo A. E. Nuccio]

Since we are discussing this, and since I have fought a bit with invertible, can I ask why being in Type rather than in Propmakes "computation easier"? Also, it seems to me tat the sentence in the doc "The intent of the typeclass is to provide a way to write e.g. ⅟2 in a ring like ℤ[1/2] where some inverses exist but there is no general ⁻¹ operator;" is a bit strange. is_unit does not need this inverse operator neither, is it an old piece of doc?

[Kevin Buzzard]

I think the point is that invertible actually carries around the inverse, even though mathematically this is daft because it's unique so you can just use classical.some

[Kevin Buzzard]

You never need to know what the inverse actually is in the calculations above, you are just formally using the fact that 1/x * x = 1

[Filippo A. E. Nuccio]

Ah, I see.

[Eric Wieser]

The benefit of carrying around the inverse is that you can prove it has an inverse, and what that inverse is all at once

[Filippo A. E. Nuccio]

OK ok, I see, it makes sense. And concerning the doc, do you agree that it is somewhat strange?

[Eric Wieser]

is_unit doesn't actually give you the inverse; are you thinking of docs#ring.inverse or docs#is_unit.unit?

[Filippo A. E. Nuccio]

At first reading one would imagine that unit or is_unit need an has_inv instance, but this is not the case.

[Filippo A. E. Nuccio]

Eric Wieser said:

is_unit doesn't actually give you the inverse; are you thinking of ring.inverse?

Well, as @Kevin Buzzard said it gives it through some, because it gives you a term of units M

[Eric Wieser]

Right, that's docs#is_unit.unit

[Kevin Buzzard]

The doc looks fine to me: what's the problem? classical.some + is_unit is arguably more inconvenient than invertible, just like we don't have an axiom in group theory in Lean saying "there exists an identity element", we have a field of the structure saying "this is the identity element".

[Eric Wieser]

Please don't use classical.some with is_unit, that's what docs#is_unit.unit is for! (edit: the latter has a nicer defeq that means you don't need some_spec)

[Filippo A. E. Nuccio]

Agreed, I simply want to say that is_unitseems to carry the inverse as well, because terms in units M do.

[Jireh Loreaux]

Eric, it seems to me like the solution to this:
Eric Wieser said:

I guess this works here because the proof is trivial in both cases, but in general you end up proving pretty much the same thing in the first and second declaration

might be something like an invertible.copy_inv where you provide an inverse and the proofs, and then another another inverse which you prove is equal to the first, then you put the second one as the data in the instance. Of course, you wouldn't actually be copying an existing invertible since its a class not a structure, but this seems like it addresses your "doing the same computation twice" complaint.

[Jireh Loreaux]

(Maybe copy_inv is a bad name)

[Eric Wieser]

Yes, I was leaning towards that too; indeed, that's why my proof goes through units.copy which was a way of doing that without writing more API

[Jireh Loreaux]

Meh, I think this is a reasonable constructor to have for invertible.

[Eric Wieser]

Maybe docs#invertible.copy is useless and should instead be the version you describe

[Filippo A. E. Nuccio]

Kevin Buzzard said:

The doc looks fine to me: what's the problem? classical.some + is_unit is arguably more inconvenient than invertible, just like we don't have an axiom in group theory in Lean saying "there exists an identity element", we have a field of the structure saying "this is the identity element".

My problem with the doc is probably that it makes no reference to docs#ring.inverse and it is therefore difficult to find a way through the several definitions (invertible, is_unit, unit, inverse, etc...)

[Eric Wieser]

@Filippo A. E. Nuccio, don't forget matrix.has_inv which is equal to ring.inverse everywhere but not defeq!

[Jireh Loreaux]

I don't think invertible.copy is useless. That allows you to transfer an invertible instance from one element to another, while preserving the inverse. The copy_inv proposal is different (because you aren't already given an invertible instance).

[Eric Wieser]

@Jireh Loreaux, do you mean this?

/-- This is defined such that `⅟y = yi` -/
def invertible.more_copy {M : Type*} [monoid M]
  (x : M) [invertible x] (y : M) (hxy : y = x) (yi : M) (hyi : yi = ⅟x) :
  invertible y :=
((unit_of_invertible x).copy _ hxy yi hyi).invertible

[Filippo A. E. Nuccio]

There is also a nice docs#mv_power_series.inv.aux that always creates an auxiliary (mv) power series depending of an element of the coefficient ring, and whenever this elements happens to be the inverse of the constant terms it really gives the inverse of the power series :eyes:

[Jireh Loreaux]

That's not what I meant, but maybe it would be handy if the existing docs#invertible.copy were changed to that (I'm not sure). What I meant was this (untested):

/-- This is defined so that `⅟x = xi'`. -/
def invertible.mk_inv {M : Type*} [monoid M]
  (x : M) (xi : M) (xi' : M) (hx : xi = xi') (hx_mul_inv : x * xi = 1) (hx_inv_mul : xi * x = 1) :
  invertible x :=
⟨xi', hx ▸ hx_mul_inv, hx ▸ hx_inv_mul⟩

But maybe I have misunderstood your original complaint?

[Eric Wieser]

I think that would be more convenient with x,xi, and the two hxs bundled... Which essentially gives you what I suggest above!

[Eric Wieser]

One thing I realized today is that invertible doesn't follow a pattern we've established elsewhere:

Existence	Explicit existence	sometimes-junk value	never-junk value
summable f	has_sum f a	tsum f	-
differentiable f	has_deriv_at f f ' a	deriv f a	-
is_unit x	invertible x	ring.inverse x	⅟x (inv_of)

Where the last row is the clear odd-one-out

[Eric Wieser]

Frankly I've found both has_sum and inv_of pretty irritating; the former forces you to use convert all the time when the a term is wrong, while the latter has equalities that you can rewrite but you have to build a bunch of typeclasses up front to use it.

[Kevin Buzzard]

has_sum is super-useful in teaching, especially before you've proved the theorem that says that a series has at most one sum.

[Eric Wieser]

Oh I completely agree it's way better than not having it at all!

[Eric Wieser]

My comment is more that the design constraints feel the same in both places, yet we've come up with two different solutions; is there a hybrid that is better than both?

[Kevin Buzzard]

I guess another example of "never junk value" would be the division function which demands a proof that the denominator is nonzero, and we don't have that either AFAIK.

[Jireh Loreaux]

docs#divp?

[Yury G. Kudryashov]

About has_sum/has_deriv_at/...: should we add congr_right lemmas like has_sum f x -> x = y -> has_sum f y to avoid convert?

[David Loeffler]

Talking of "existence vs. explicit existence", I've often wondered whether the integration library might benefit from introducing has_integral f μ a, analogous to has_sum f a.

[Eric Wieser]

I'm coming to the conclusion that what we probably want is a has_inverse x x_inv proposition; the reason we don't have it already is probably that it's mostly useless in commutative setting where you can just write x * x_inv = 1

[Jireh Loreaux]

I think you're right. I ran into this kind of headache on the way to proving the Gelfand formula for the spectral radius, but at the time I didn't recognize that this missing API was the problem. I think I got around it by defining a new Units term and then using that, but the details are a bit murky.

[Yury G. Kudryashov]

Should we introduce something between DivInvMonoid (fixed) and DivisionMonoid instead assuming just ∀ a b, a * b = 1 → b * a = 1 → a⁻¹ = b?

[Yury G. Kudryashov]

And use a⁻¹ everywhere?

[Eric Wieser]

I think we'd want has_inverse first

[Jireh Loreaux]

What is a docs4#DIvInvMonoid ?

[Eric Wieser]

It's a monoid with the obvious link between div and inv and nothing else integer powers

[Eric Wieser]

docs4#DivInvMonoid

[Yury G. Kudryashov]

Another approach is to add this axiom to DivInvMonoid.

[Yury G. Kudryashov]

I guess, this is true in all instances.

[Yaël Dillies]

We already had this discussion, and the upshot is that it's not so obvious.

[Yury G. Kudryashov]

Could you give a link (or an example), please?

[Kevin Buzzard]

Were n*n matrices a problem?

[Yury G. Kudryashov]

What's wrong with matrices? The Inv.inv (with any reasonable definition) agrees with Unit.val/Unit.inv.

[Eric Wieser]

Yury, I suspect the answer is that your generalization can't actually be used in many existing lemmas because it doesn't specify the junk value for non-invertible elements

[Yury G. Kudryashov]

But it can be used in all lemmas that only deal with invertible elements (e.g., smoothness of Ring.inverse).

[Alex J. Best]

I sketched some of the basic theory of the left inverse implies right inverse typeclass here https://github.com/leanprover-community/mathlib/pull/11376 but it is quite old!