Zulip Chat Archive

Stream: new members

Topic: (topological) quotient group


Daan van Gent (Jul 18 2020 at 16:07):

I am trying to define the topological group \R / \Z and I am running into some problems. First one has to construct the subgroup \Z of \R. Apparently this can be done in two ways, with add_subgroup and is_add_subgroup. The latter is deprecated, but the former has no quotient definition associated as far as I know. What should I do?

Heather Macbeth (Jul 18 2020 at 16:28):

The experts will answer you soon, but the short answer is that you have found a refactor-in-progress. #3321

Kevin Buzzard (Jul 18 2020 at 16:48):

I just got quotient_group.lean compiling with add_subgroup and no errors an hour ago :-)

Alex J. Best (Jul 18 2020 at 17:12):

Maybe you are doing this already but I'd recommend explcitly defining Z inside R as the image of the coercion map from Z to R. You might get more results for free that way

Kevin Buzzard (Jul 18 2020 at 17:21):

Before norm_cast I was considering making two typeclasses on real, both called something like is_int, one a predicate ("there exists an integer such that I'm the coercion of that integer") and one containing data (the integer plus a proof that the integer coerces to the real in question). Type class inference could be used to show that the sum of two real integers was a real integer etc

Daan van Gent (Jul 18 2020 at 18:08):

Alex J. Best said:

Maybe you are doing this already but I'd recommend explcitly defining Z inside R as the image of the coercion map from Z to R. You might get more results for free that way

I define Z as the subgroup generated by 1 in R. I'll see whether your suggestion turns out to be more useful when I get to working with it.

Daan van Gent (Jul 18 2020 at 18:09):

Thanks for your answers. I guess I'll wait a bit before playing around with groups some more.


Last updated: Dec 20 2023 at 11:08 UTC