Odd Fintype

Stream: mathlib4

[Christian K]

I have a definition that only works in Odd rank (More Info in this thread. My idea was to define a separate OddFintype typeclass that only allows Fintypes with an odd cardinality.

class OddFintype (α : Type*) extends Fintype α where
  odd : Odd (Fintype.card α)

variable (n) (α) [Fintype n] [OddFintype n]

Is there a smarter way to do this (and if not, should something like this be in the mathlib?)

[Yaël Dillies]

In that specific case, @Scott Carnahan gave you a definition that works for all ranks, so I would formalise it instead of restricting your current definition

[Yaël Dillies]

Probably it is too hard for you, though. In that case, restrict to the 3D case and we can think about generality later

[Kyle Miller]

Here's a setup for a finite type with odd cardinality:

class OddCard (α : Type*) : Prop where
  odd : Odd (Nat.card α)

-- quickly written proof:
instance (α : Type*) [OddCard α] : Finite α := by
  have key : Odd (Nat.card α) := OddCard.odd
  by_contra h
  rw [not_finite_iff_infinite] at h
  have : Nat.card α = 0 := Nat.card_eq_zero_of_infinite
  rw [this] at key
  simp at key

variable (α : Type*) [OddCard α]

Many times you don't need Fintype, since instead you just need the mere fact that something is Finite. It's easier to work with a proposition (like Finite or OddCard) instead of data-carrying classes (like Fintype).

Here, I'm using a trick that Nat.card can only be nonzero if the type is finite.

[Kyle Miller]

You can also work with [Fintype α] [OddCard α] together without worrying that the OddCard will have any data that conflicts with the Fintype instance.

[Christian K]

Yeah, it is too hard... But the thing I'm trying to do here is to generalize SO and later equidecomposability to get it into mathlib. Were can I learn about the things I need to generalize equidecomposability? Or is it just too ambitious (at least for me, as a non - mathematictian)?

Yaël Dillies said:

Probably it is too hard for you, though. In that case, restrict to the 3D case and we can think about generality later

[Yaël Dillies]

I have no clue and I'm a master student, so :grimacing:

[Yaël Dillies]

Hopefully Scott can tell you

[Christian K]

Kyle Miller said:

You can also work with [Fintype α] [OddCard α] together without worrying that the OddCard will have any data that conflicts with the Fintype instance.

Ohhh, thank you, I did not know about OddCard, this is very nice

[Kyle Miller]

To be clear, I defined OddCard in my post

[Kyle Miller]

Also, I'm not sure this OddCard is good or bad to have around in mathlib, but in any case, if it's a good idea, then this is how I would probably go about designing it.

[Christian K]

Kyle Miller said:

To be clear, I defined OddCard in my post

Ok, I should have read better..... anyways, thank you. In my case, I think it is not worth bothering with using OddCard to define SU and SO, I'll just wait for someone smarter to do it ....

[Christian K]

Yaël Dillies said:

I have no clue and I'm a master student, so :grimacing:

Ok, I'm gonna just go back to studying for my high school math exam then..... :laughing: (maybe some day....)

[Kim Morrison]

Why not just assume 2 is invertible? (And then just be able to define SO as the kernel of the determinant.) That seems like a pretty reasonable assumption for getting started, and people who care about characteristic 2 can be responsible for switching from "kernel of determinant" to "kernel of Dickson" later, without it really needing to interact with anything @Christian K wants to do.

[Kim Morrison]

It seems like this might be a case where excessive generality from the beginning is discouraging a potential contributor. :-)

[Mitchell Lee]

Yes, you make a good point.

[Eric Wieser]

Regarding whether mathlib should have the typeclass; often for this type of one-off thing, we just use Fact (Odd <| Nat.card X)

[Eric Wieser]

It can always be promoted to a named typeclass later

[Christian K]

Ok thank you for your friendly help, I'll read up on what 2 being invertible means and define SO that way (I started it so I'm gonna finish it).

[Christian K]

I'm continuing this here because I think it makes the most sense. I added the requirement that 2 is invertible like this:

variable (n) (α : Type v) [CommRing α] [StarRing α] [Invertible (2 : α)] {A : Matrix n n α}

/--`Matrix.specialUnitaryGroup` is the group of unitary `n` by `n` matrices where the determinant
is 1-/
abbrev specialUnitaryGroup := (MonoidHom.restrict detMonoidHom (unitaryGroup n α)).ker

(link to PR)