LinearAlgebra.UnitaryGroup and special unitary groups

Stream: mathlib4

[Chris Henson]

I am interested in working with special unitary groups of matrices. I have seen LinearAlgebra.UnitaryGroup and thought I might be able to define them as a subgroup.

However I was confused to find that Matrix.unitaryGroup has type Submonoid (Matrix n n α), while I expected it to be a group. I also don't see a Group typeclass instance in the source file. Am I overlooking them, or maybe they are defined somewhere else?

(Also if there is a better approach to defining special unitary groups of matrices, I would welcome any advice. I am new to using Mathlib and Lean.)

[Jireh Loreaux]

In this case, the module documentation explains the situation:

docs#Matrix.unitaryGroup is the submonoid of matrices where the star-transpose is the inverse; the group structure (under multiplication) is inherited from a more general docs#unitary construction.

[Jireh Loreaux]

In particular, the group structure comes from:
docs#unitary.instGroupSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitary

[Chris Henson]

Thanks! I did see that note but wasn't sure where/what it was referring to. I still don't quite understand how to use that to define a special unitary group. My first thought is something like:

import Mathlib.Algebra.Star.Unitary
import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Complex.Basic
import Mathlib.LinearAlgebra.UnitaryGroup

instance SU_ℂ (n: ℕ) : @Subgroup (unitary (Matrix (Fin n) (Fin n) ℂ)) unitary.instGroupSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidUnitary where
  carrier := { A | Matrix.det A = 1}
  mul_mem' := sorry
  one_mem' := sorry
  inv_mem' := sorry

but that is definitely wrong because A does not have a matrix type. Is there a way to make this kind of approach work or do I need to find a different way?

[Kevin Buzzard]

What happens if you just remove the @ and the silly instance name?

One thing you might want to consider is that if someone "unwraps" an element of the special unitary group, what do you expect them to find? I would expect either a matrix or an invertible matrix, not an element of the unitary matrix group which I can unwrap further

[Chris Henson]

Is something like

instance SU_ℂ' (n: ℕ) : Subgroup (Matrix (Fin n) (Fin n) ℂ) where
  carrier := { A | Matrix.det A = 1}
  mul_mem' := sorry
  one_mem' := sorry
  inv_mem' := sorry

what you mean to try? I definitely agree that the type is more natural to unwrap, but there's no existing instance of Group (Matrix (Fin n) (Fin n) ℂ). Something like

instance SU (n: ℕ) : Group {A : (Matrix (Fin n) (Fin n) ℂ) | Matrix.det A = 1 /\ Matrix.conjTranspose A = A} where
  mul := sorry
  mul_assoc := sorry
  one := sorry
  one_mul := sorry
  mul_one := sorry
  inv := sorry
  mul_left_inv := sorry

is what I would reach for in Coq, but I wasn't sure if is idiomatic Lean or fits well with connecting to what Mathlib has for the general linear and unitary groups.