Using type classes in definitions

Stream: general

[Robert Maxton]

So, I have a theorem:

theorem class_equation (G: Type*) [fin_group G]:
  fintype.card G =
    fintype.card (center G)
      + (∑ x in (conjugacy_classes G), fintype.card x) :=
    sorry

and I have proofs that conjugacy_classes G coerces to a fintype, as are all sets in conjugacy_classes G. How do I tell Lean that those proofs exist, so I can use ∑ and fintype.card x in the statement of the theorem?

[Johan Commelin]

Do you have instance : fintype (conjugacy_classes G) somewhere?

[Johan Commelin]

I don't know what you mean by "coerces to a fintype"

[Johan Commelin]

Note that ∑ x in foo is summing over a finset, whereas ∑ x : foo is summing over a Type (and there must be an instance of fintype foo).

[Johan Commelin]

Note that there is also finset.card, if you are taking the cardinality of a finset.

[Robert Maxton]

Well, what I have is a proof that, under certain conditions, there exists an instance of fintype (conjugacy_classes G). I'm not entirely sure how to write a dependent instance like that; do I have to define a structure for it, maybe?

[Robert Maxton]

and by "coerces to a fintype" I just mean fintype ↥(conjugacy_classes G)

[Kevin Buzzard]

I don't understand the question. Are you asking how to make a term of that type, or saying you can make a term of that type?

[Robert Maxton]

I'm saying I can make a term of that type, but not always; so my ability to coherently state my theorem is conditional.

[Robert Maxton]

Which actually sounds pretty 'just make a dedicated structure'-ish to me, except that I seem to have accidentally gotten it working ...

[Robert Maxton]

but now I want to know why this works:

theorem class_equation (G: Type*) [fin_group G]:
  fintype.card G =
    fintype.card (center G)
      + (∑ s: ↥(conjugacy_classes G), fintype.card s) :=
begin
  sorry
end

[Johan Commelin]

We can't answer that without more context.

[Johan Commelin]

You'll need to link to a file with more code.

[Robert Maxton]

that's an mwe lol

[Robert Maxton]

or almost

[Robert Maxton]

import group_theory.subgroup
import group_theory.group_action
import data.fintype.basic
import algebra.big_operators

open subgroup
open_locale big_operators
open_locale classical

class fin_group (G: Type*) extends group G, fintype G

def conjugacy_classes (G: Type*) [group G]: set (set G) :=
  { s | ∃ a:G, s = group.conjugates a }

def nontrivial_conjugacy_classes (G: Type*) [group G]: set (set G) :=
  { s ∈ conjugacy_classes G | nontrivial s }

theorem class_equation (G: Type*) [fin_group G]:
  fintype.card G =
    fintype.card (center G)
      + (∑ s: (nontrivial_conjugacy_classes G), fintype.card s) :=
begin
  sorry
end

[Robert Maxton]

there, that's an mwe

[Robert Maxton]

I have no idea why this works and I'm vaguely suspicious it shouldn't

[Johan Commelin]

Lean knows that s : set X and [fintype X] implies [fintype s]

[Johan Commelin]

Are you using VS code?

[Johan Commelin]

If so, you can explore your statement with the widgets in the infoview.

[Johan Commelin]

Click on the \sum symbol, and then click on finset.univ

[Johan Commelin]

You'll see subtype.fintype show up in a pop-up window.

[Kevin Buzzard]

You put open_locale classical so now sanity prevails and everything which is obviously finite classically is known to be finite in lean

[Johan Commelin]

If you want it to break, add @[irreducible] before one of the defs.

[Robert Maxton]

@Kevin Buzzard ahh, okay. That would make sense. I had kind of gotten used to having it off

[Robert Maxton]

and yeah I've been wandering around my file in VS Code but wasn't really getting anywhere

[Mario Carneiro]

By the way, regarding your earlier question about proving that congugacy_classes is finite, you can express it as finset.image group.conjugates_finset finset.univ provided that G has decidable equality

[Mario Carneiro]

where group.conjugates_finset a is defined as finset.image (\lam g, g^-1 * a * g) finset.univ