Stream: general

Topic: noncomputable card

Kevin Buzzard (May 03 2020 at 12:24):

I'm going to have a summer student working with me on group theory and I wondered whether Sylow 2 and 3 was accessible to them. Talking to @Chris Hughes he seemed to think that a useful prerequisite would be a noncomputable card function which sent infinite types to 0, and claimed that this was @Mario Carneiro 's idea. Does this sound like a sensible thing? I guess that if I were to write it I'd do it in June, because I'd need it by July. I already have bundled normal subgroups and adding metric space examples to Patrick's tutorial project on my Lean pile, plus two more grant applications, so it's unlikely it will happen before then, but I thought I'd run it past the community in case anyone had any comments or tips.

Mario Carneiro (May 03 2020 at 12:33):

It should be easy work

Mario Carneiro (May 03 2020 at 12:34):

you will have a lot of finiteness assumptions though in the theorems, because that 0 garbage case will mess up the algebra

Reid Barton (May 03 2020 at 12:40):

What about an enat-valued card?

Mario Carneiro (May 03 2020 at 12:54):

I like that version the best if we ignore typing problems

Mario Carneiro (May 03 2020 at 12:54):

it's not clear to me how important it is that the value be a nat

Kevin Buzzard (May 03 2020 at 12:54):

@Chris Hughes would an enat-valued version be good enough for applications to Sylow 2/3?

Mario Carneiro (May 03 2020 at 12:54):

Is there a enat.to_nat function? We could compose through that when necessary

Mario Carneiro (May 03 2020 at 12:55):

You can still use the enat version for a predicate like card A = enat.of_nat n

Mario Carneiro (May 03 2020 at 12:56):

which asserts both finiteness and a particular cardinality without a fintype assumption

Chris Hughes (May 03 2020 at 12:56):

enat would be hideous for group theory because you're always raising to the power of the cardinality, and multiplying the cardinality etc.

Mario Carneiro (May 03 2020 at 12:57):

would those theorems work with a predicate like I gave?

Mario Carneiro (May 03 2020 at 12:57):

you have an assumption card A = (n : nat) and then use n in the theorem

Chris Hughes (May 03 2020 at 13:11):

Probably they would. Multiplicity was really bad, because I didn't state theorems like that.

Johan Commelin (May 03 2020 at 13:16):

Why would you need an enat valued card for such predicates?

Johan Commelin (May 03 2020 at 13:16):

Wouldn't the cardinal-valued version suffice?

Mario Carneiro (May 03 2020 at 13:24):

You don't need to import set_theory.cardinal to define the enat version

Chris Hughes (May 03 2020 at 13:26):

In Lean 2, we had a nonconstructive cast from set to finset which mapped any infinite set to the empty set. So we had set.card s = finset.card (s.to_finset). The cardinality of the empty set still comes out to zero, and it is easy to translate finset theorems (e.g. about card and sum) to set theorems.
The advantage to having card and sum map infinite sets to 0 is that lots of identities hold without preconditions. It makes it much more convenient to work with them. Isabelle follows that approach as well.