What should set.has_inv do?

Stream: general

[Eric Wieser]

Given the following setup

import linear_algebra.matrix.nonsingular_inverse
import algebra.pointwise
open_locale pointwise cardinal

and knowing that:

example : #↥(({0} : set ℚ)⁻¹) = 1 := by simp [set.inv_singleton]

What would you expect right choice of _ to be here?

example : #↥(({0} : set (matrix (fin 2) (fin 2) ℚ))⁻¹) = _ := sorry

[Eric Wieser]

/poll What should the _ be?

• 0
• 1
• ω

[Eric Wieser]

It's currently the preimage of inv not the image like * is...

[Yaël Dillies]

Having it be the preimage is nice, right? at least when it's involutive...

[Adam Topaz]

I think this operation should apply has_inv.inv to everything in the set.

[Reid Barton]

By default it should not exist unless someone has a use for it

[Adam Topaz]

Yeah, that too.

[Adam Topaz]

It's very common, e.g. in group theory, to write $S^{-1}$, $g \cdot S$, $S \cdot g$, $S \cdot S$, etc., where $S$ is a subset and g is an element of some group.

[Reid Barton]

Great, then give the instance a group constraint.

[Adam Topaz]

Can we make something like this work in Lean4?

variable (G : Type u) [Mul G]

instance (M : Type u → Type u) [Monad M] : Mul (M G) where
  mul a b := return (← a) * (← b)

instance (M : Type u → Type u) [Monad M] : HMul G (M G) (M G) where
  hMul a b := return a * (← b)

instance (M : Type u → Type u) [Monad M] : HMul (M G) G (M G) where
  hMul a b := return (← a) * b

This typechecks, but it is a good idea?

[Adam Topaz]

Anyway, I think this is a perfectly reasonable instance:

import data.set.basic
instance {α : Type*} [has_inv α] : has_inv (set α) := ⟨λ S, (λ t : α, t⁻¹) '' S⟩

[Yury G. Kudryashov]

Reid Barton said:

By default it should not exist unless someone has a use for it

You need to open_locale pointwise to have this and other instances.

[Adam Topaz]

Oh, I didn't know that existed.