normed structures on quotients

Stream: Is there code for X?

[Jireh Loreaux]

What norm structures do we have on quotients? Specifically, I am interested in A ⧸ I where A is a normed_algebra over R and I is an ideal of A. For the moment, I am only interested in commutative A.

[Patrick Massot]

Do you know I is closed?

[Johan Commelin]

There should at least be a semi_normed_add_group on such a quotient.

[Anatole Dedecker]

(Slightly related: I have a not PR-ed proof that maximal ideals are closed, so tell me if you need it quickly)

[Anatole Dedecker]

Jireh Loreaux said:

What norm structures do we have on quotients? Specifically, I am interested in A ⧸ I where A is a normed_algebra over R and I is an ideal of A. For the moment, I am only interested in commutative A.

We have docs#add_subgroup.seminormed_add_comm_group_quotient and docs#add_subgroup.normed_add_comm_group_quotient but that's all I see

[Jireh Loreaux]

Thanks all. Anatole, I also have a proof that maximal ideals are closed that I am planning to put in analysis/normed_space/units. Patrick, I will often be closed so that we actually get a norm, but we will want the seminormed version too when I is not closed.

[Jireh Loreaux]

I will start PRing the relevant structures soon.

[Jireh Loreaux]

@Anatole Dedecker #16303 for the fact the maximal ideals are closed, in case you want to review and/or add anything.

[Jireh Loreaux]

I had a think about putting these norm structures on the quotient, and I have had several thoughts:

1. Given an ideal I (or more generally a submodule) of R, one cannot just pull back the norm structure of R / I.to_add_subgroup along add_monoid_hom.id _ to R / I. Or rather, you can do it, but you lose the definitional equality for the topological structure with the quotient topology.
2. I could just duplicate the approach in analysis.normed.group.quotient to get the right definitional equality, but the code would be nearly identical (we are still talking about additive cosets after all), so this seems unsatisfactory, but completely doable.
3. I had the idea that it would be nice if the quotient were defined for members of add_subgroup_class instead of subgroup. In this way it would unify the quotients and there would be no need to duplicate API. I glanced briefly over the quotient constructions, and it seems like it might be doable, although for technical reasons it might be easier if we switched to right cosets instead of left cosets (because docs#quotient_group.left_rel uses docs#subgroup.opposite, for which I don't think there will be any nice subgroup_class version).

Has anyone else thought about this at all? @Eric Wieser @Anne Baanen

[Eric Wieser]

Is the underlying question here "can we unify ring and (additive) subgroup quotients"? Because as types, I think they're now defeq

[Jireh Loreaux]

They are defeq, which is why that add_monoid_hom.id trick above semi-works. But since it's not a reducible defeq we don't get to share instances; in particular, I can't get the norm structure on R ⧸ I for free.

[Eric Wieser]

What makes it not reducible?

[Eric Wieser]

I'm surprised you even need to pull it back, can't you just copy over the existing instance?

[Jireh Loreaux]

Hmmm... let me try again. I thought I started with that and it didn't work.

[Jireh Loreaux]

aha, no that seems to work

[Eric Wieser]

The suggestion of generalizing to add_group_class is still reasonable, but it should be a low amount of effort to do it manually first

[Jireh Loreaux]

I didn't see a nice way around the docs#subgroup.opposite issue though, do you?

[Jireh Loreaux]

I will just do this manually for now, as I really need it for some other work.

[Eric Wieser]

I would guess s.opposite could be replaced with sᵐᵒᵖ, after adding some instances

[Anne Baanen]

Jireh Loreaux said:

3. I had the idea that it would be nice if the quotient were defined for members of add_subgroup_class instead of subgroup.
   [...]
   Has anyone else thought about this at all? Eric Wieser Anne Baanen

Definitely! In fact, my idea behind making R explicit in R / I was to allow better inference of the add_subgroup_class instance. Making the various quotient definitions equal was a slow process but I think there should be no technical obstacle anymore beyond the typical amount of fixes.