Zulip Chat Archive

Stream: general

Topic: What should set.has_inv do?


Eric Wieser (Feb 11 2022 at 21:53):

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 (Feb 11 2022 at 21:54):

/poll What should the _ be?

  • 0
  • 1
  • ω

Eric Wieser (Feb 11 2022 at 21:55):

Yaël Dillies (Feb 11 2022 at 21:56):

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

Adam Topaz (Feb 11 2022 at 22:08):

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

Reid Barton (Feb 11 2022 at 22:08):

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

Adam Topaz (Feb 11 2022 at 22:09):

Yeah, that too.

Adam Topaz (Feb 11 2022 at 22:12):

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

Reid Barton (Feb 11 2022 at 22:17):

Great, then give the instance a group constraint.

Adam Topaz (Feb 11 2022 at 22:18):

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 (Feb 11 2022 at 22:27):

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 (Feb 12 2022 at 00:01):

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 (Feb 12 2022 at 01:02):

Oh, I didn't know that existed.


Last updated: Dec 20 2023 at 11:08 UTC