(topological) quotient group

Stream: new members

[Daan van Gent]

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]

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

[Kevin Buzzard]

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

[Alex J. Best]

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]

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]

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]

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