Zulip Chat Archive

Stream: general

Topic: noncomputable card


view this post on Zulip 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.

view this post on Zulip Mario Carneiro (May 03 2020 at 12:33):

It should be easy work

view this post on Zulip 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

view this post on Zulip Reid Barton (May 03 2020 at 12:40):

What about an enat-valued card?

view this post on Zulip Mario Carneiro (May 03 2020 at 12:54):

I like that version the best if we ignore typing problems

view this post on Zulip Mario Carneiro (May 03 2020 at 12:54):

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

view this post on Zulip Kevin Buzzard (May 03 2020 at 12:54):

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

view this post on Zulip Mario Carneiro (May 03 2020 at 12:54):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 03 2020 at 12:56):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (May 03 2020 at 12:57):

would those theorems work with a predicate like I gave?

view this post on Zulip Mario Carneiro (May 03 2020 at 12:57):

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

view this post on Zulip Chris Hughes (May 03 2020 at 13:11):

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

view this post on Zulip Johan Commelin (May 03 2020 at 13:16):

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

view this post on Zulip Johan Commelin (May 03 2020 at 13:16):

Wouldn't the cardinal-valued version suffice?

view this post on Zulip Mario Carneiro (May 03 2020 at 13:24):

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

view this post on Zulip Chris Hughes (May 03 2020 at 13:26):

Are imports really that bad?

view this post on Zulip Jeremy Avigad (May 04 2020 at 01:37):

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.


Last updated: May 13 2021 at 23:16 UTC