Zulip Chat Archive

Stream: Is there code for X?

Topic: Difference between submodules


view this post on Zulip Eric Wieser (Nov 10 2020 at 09:53):

Is there a way to take two submodules A and B and construct the submodule that is A with all the elements of B (except 0) removed?

view this post on Zulip Anne Baanen (Nov 10 2020 at 09:55):

If it exists, I would call it sdiff. But I can't find any sdiff in module so probably no.

view this post on Zulip Eric Wieser (Nov 10 2020 at 09:56):

Does it exist for any other sub*objects?

view this post on Zulip Anne Baanen (Nov 10 2020 at 09:56):

How about submodule.span K (A \ B)?

view this post on Zulip Eric Wieser (Nov 10 2020 at 09:57):

For some reason I had in my head I was looking for \ not /. That looks like what I'm after

view this post on Zulip Eric Wieser (Nov 10 2020 at 09:57):

Should submodule define that as has_sdiff?

view this post on Zulip Anne Baanen (Nov 10 2020 at 09:57):

Doesn't look like it exists for any subobjects (except finset which is a subobject only very dubiously).

view this post on Zulip Sebastien Gouezel (Nov 10 2020 at 10:01):

This is not a submodule in general...

view this post on Zulip Sebastien Gouezel (Nov 10 2020 at 10:01):

submodule.span K (A \ B) is probably equal to A unless A is contained in B.

view this post on Zulip Eric Wieser (Nov 10 2020 at 10:07):

So, the case I'm thinking of is where A is polynomials of degree n + 1 and B is polynomials of degree n.

view this post on Zulip Johan Commelin (Nov 10 2020 at 10:07):

Sure, but take n = 0, what do you do with X and X + 1?

view this post on Zulip Eric Wieser (Nov 10 2020 at 10:08):

And I want to recover the space spanned by monomials of exactly degree n

view this post on Zulip Johan Commelin (Nov 10 2020 at 10:08):

You need something like a grading to do that

view this post on Zulip Eric Wieser (Nov 10 2020 at 10:09):

Johan Commelin said:

Sure, but take n = 0, what do you do with X and X + 1?

I can't match these words to my question - can you elaborate slightly? What are A and B here?

view this post on Zulip Eric Wieser (Nov 10 2020 at 10:09):

(What I'm trying to do is recover a grading from a filtering, https://en.wikipedia.org/wiki/Filtered_algebra#Associated_graded_algebra)

view this post on Zulip Johan Commelin (Nov 10 2020 at 10:09):

A = polys of degree le 1, and B = polys of degree le 0.

view this post on Zulip Johan Commelin (Nov 10 2020 at 10:10):

So B is the constants. But A \ B contains X and X + 1. Any submodule that contains X and X + 1 also contains 1, and hence all the constants.

view this post on Zulip Johan Commelin (Nov 10 2020 at 10:11):

So you need a way to say that X + 1 is bad, impure, nonhomogeneous.

view this post on Zulip Eric Wieser (Nov 10 2020 at 10:11):

Johan Commelin said:

But A \ B contains X and X + 1.

Ah, I see the problem now

view this post on Zulip Johan Commelin (Nov 10 2020 at 10:11):

A grading let's you do that

view this post on Zulip Johan Commelin (Nov 10 2020 at 10:12):

You can't recover a grading from a filtration. But you can define a graded object starting from a filtration. It's just that it will be on a completely different vector space/module

view this post on Zulip Johan Commelin (Nov 10 2020 at 10:12):

It's called the "associated graded"

view this post on Zulip Eric Wieser (Nov 10 2020 at 10:13):

Right, that's what I'm after

view this post on Zulip Eric Wieser (Nov 10 2020 at 10:14):

"it will be on a completely different vector space/module" - will it? Supposedly the vector spaces are isomorphic, which I take to mean "I can put them in the same type if I pull the right levers"

view this post on Zulip Eric Wieser (Nov 10 2020 at 10:16):

Perhaps I'm after the quotient of A by the relation "member of B"

view this post on Zulip Johan Commelin (Nov 10 2020 at 10:17):

Eric Wieser said:

"it will be on a completely different vector space/module" - will it? Supposedly the vector spaces are isomorphic, which I take to mean "I can put them in the same type if I pull the right levers"

Yes, but this is highly non-canonical. It's not functorial

view this post on Zulip Johan Commelin (Nov 10 2020 at 10:18):

Eric Wieser said:

Perhaps I'm after the quotient of A by the relation "member of B"

Yup, the quotient module A/B does what you want

view this post on Zulip Johan Commelin (Nov 10 2020 at 10:19):

In general, the associated graded is i(FiM/Fi+1M)\bigoplus_i \left(F^i M / F^{i+1}M\right)

view this post on Zulip Eric Wieser (Nov 10 2020 at 10:21):

Not sure I understand what the M is there, or what its adjacency to F signifies

view this post on Zulip Johan Commelin (Nov 10 2020 at 10:24):

F is a filtration on a module M

view this post on Zulip Johan Commelin (Nov 10 2020 at 10:24):

So F^i M is a submodule of M

view this post on Zulip Eric Wieser (Nov 10 2020 at 10:25):

Ok, cool - I have the F^i M already then

view this post on Zulip Eric Wieser (Nov 10 2020 at 11:20):

Johan Commelin said:
Yup, the quotient module A/B does what you want

Naturally, this is not sufficiently general for me... It requires the algebra to be commutative.

view this post on Zulip Reid Barton (Nov 10 2020 at 11:27):

Not sure what "the algebra" refers to, but quotient modules and the associated graded module of a filtered module work also for modules over a noncommutative ring. But mathlib might have unnecessary commutativity hypotheses of course.

view this post on Zulip Eric Wieser (Nov 10 2020 at 11:36):

Yeah, I'm referring specific to submodule.has_div [algebra R A] requiring comm_semiring A - so this is a mathlib limitation

view this post on Zulip Reid Barton (Nov 10 2020 at 12:10):

Can you link to the docs/source?

view this post on Zulip Reid Barton (Nov 10 2020 at 12:18):

I don't understand why an algebra is involved. Oh wait, what is submodule.has_div? maybe it's not the quotient module?

view this post on Zulip Eric Wieser (Nov 10 2020 at 12:22):

docs#submodule.has_div

view this post on Zulip Reid Barton (Nov 10 2020 at 12:37):

docs#submodule.quotient

view this post on Zulip Eric Wieser (Nov 10 2020 at 13:54):

(deleted)

view this post on Zulip Eric Wieser (Nov 10 2020 at 14:35):

Thanks @Reid Barton. I can't quite work out how to use that either - that takes the quotient of the entire module M by the submodule S : submodule R M, but I want to take the quotient of S1 : submodule R M by S2 : submodule R M.

Since I know that S1 ≤ S2, I suppose I ought to be able to convert S1 to S1' : submodule R S2, at which point I could use S1'.quotient.

Does mathlib already have something that can do this conversion?

example (S1 : submodule R M) (S2 : submodule R M) (h : S1  S2) : submodule R S2 := sorry

view this post on Zulip Kevin Buzzard (Nov 10 2020 at 14:43):

I experimented with a "subquotient object" at some point, consisting of a pair of submodules; I could define maps between them (a map from the first top object to the second top object sending the first bottom object into the second bottom object, maybe I even put some lattice structure on them; this was all in a student's MSc project, so nowhere near mathlib and it will probably not compile now. But I was never convinced this was the way to go -- for example I later on realised that I wanted an object equipped with a filtration having more than 2 nontrivial elements.

I am not sure I know a good solution to your problem. Maybe just bite the bullet and make S1'? :-/ Pain might be forthcoming though, or perhaps not, depending on what you're doing.

view this post on Zulip Reid Barton (Nov 10 2020 at 14:43):

I guess you can use docs#submodule.comap and docs#submodule.subtype; not sure if there is something more custom purpose in mathlib

view this post on Zulip Eric Wieser (Nov 10 2020 at 14:50):

I get the feeling that docs#direct_limit might overlap with what I need...


Last updated: May 16 2021 at 05:21 UTC