old_structure_cmd slowness/failure

Stream: general

[Yakov Pechersky]

In #8683, @Anne Baanen suggested having a general intermediate in the algebra hierarchy of div_inv_monoids with a lawful inv, such that is_unit x → x * x⁻¹ = 1. Here is my attempt at such a structure... Why is the elaboration slow? It seems like it can't infer the parent monoid structure, and chokes on is_unit. Is this related to https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Not.20finding.20typeclass.20in.20hypotheses

import algebra.group.units

set_option old_structure_cmd true

universe u

@[protect_proj, ancestor div_inv_monoid]
structure cancel_inv_monoid (G : Type u) extends div_inv_monoid G :=
(mul_inv_cancel' : ∀ (x : G), is_unit x → x * x⁻¹ = 1)

example {G : Type u} [cancel_inv_monoid G] : monoid G := by apply_instance -- fails

-- also not possible because `[monoid G]` isn't inferred, so `is_unit`, `⁻¹`, `*`, `1` all fail
lemma cancel_inv_monoid.inv_mul_cancel' {G : Type u} [cancel_inv_monoid G] (x : G) (h : is_unit x) :
  x⁻¹ * x = 1 := sorry

[Eric Wieser]

You missed class and wrote structure?

[Yury G. Kudryashov]

Is there any example we care about when we have cancel_inv_monoid but we don't have involutive has_inv.inv?

[Yury G. Kudryashov]

If not, what do you think about including this as an axiom of cancel_inv_monoid?

[Yakov Pechersky]

So the inverse that we have for matrices sends nonunit matrices to 0. Which means that inv is involutive on all matrices, but means that some properties are only true for unit matrices. The other possible definition could have been to send nonunit matrices to themselves. That also retains involutive inv, but constraints some other proofs.

[Yakov Pechersky]

That is to say, yes that is a good axiom to have. But I don't remember the details right now.

[Alex J. Best]

(one) good answer for the generalized inverse of a matrix is the Drazin inverse, https://en.wikipedia.org/wiki/Drazin_inverse?wprov=sfla1. Iirc this is a concept that makes sense in any semi group and coincides with the usual inverse for groups, the fun fact is that it is unique if it exists in any semigroup.

[Eric Wieser]

Doesn't this also give us a way to unify map_inv lemmas between field and group too?

[Yury G. Kudryashov]

@Eric Wieser No, because we still have to prove it for non-units.

[Yakov Pechersky]

I need to revise my previous statement. Inv sending nonunits to 0 is not involutive. But inv_inv_inv is equal to inv. I don't remember at the moment why 0 is the preferred way, but when I worked through it, it gave easier proofs iirc.