Zulip Chat Archive

Stream: new members

Topic: Vector space over continuous functions


view this post on Zulip Nicolò Cavalleri (Jul 11 2020 at 14:22):

Oh ok I think I know an example of what you are talking about: it looks type class inference does not work very well for is_subring in the instance continuous_ring

view this post on Zulip Nicolò Cavalleri (Jul 11 2020 at 14:25):

In any case I guess then the file continuous_functions will be changed with definitions of subgroups instead of is_subgroup and all of this will be done over continuous bundled functions instead of the subtype of continuous functions as @Scott Morrison was suggesting

view this post on Zulip Nicolò Cavalleri (Jul 11 2020 at 14:25):

If I have time I can try to do it at some point

view this post on Zulip Nicolò Cavalleri (Jul 11 2020 at 14:27):

But for example it seems that the structure subring is not there yet so it's too early to do that

view this post on Zulip Alex J. Best (Jul 11 2020 at 14:32):

Theres also the possibility to use the theory of lattices with subgroup , we can set up an order on subgroups by containment (so far just like sets), and then take things like the least upper bound of two subgroups, which is the smallest subgroup containing both (the subgroup generated by their union rather than just taking the union as sets). I think that sort of thing was harder to arrange with is_subgroup.

view this post on Zulip Kevin Buzzard (Jul 11 2020 at 14:33):

subgroup G has a lattice structure, but the sup is not the one induced from sup on set G, as the union of two subgroups is typically not a subgroup.


Last updated: May 14 2021 at 12:18 UTC