Difference between submodules

Stream: Is there code for X?

[Eric Wieser]

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?

[Anne Baanen]

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

[Eric Wieser]

Does it exist for any other sub*objects?

[Anne Baanen]

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

[Eric Wieser]

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

[Eric Wieser]

Should submodule define that as has_sdiff?

[Anne Baanen]

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

[Sebastien Gouezel]

This is not a submodule in general...

[Sebastien Gouezel]

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

[Eric Wieser]

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

[Johan Commelin]

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

[Eric Wieser]

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

[Johan Commelin]

You need something like a grading to do that

[Eric Wieser]

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?

[Eric Wieser]

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

[Johan Commelin]

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

[Johan Commelin]

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.

[Johan Commelin]

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

[Eric Wieser]

Johan Commelin said:

But A \ B contains X and X + 1.

Ah, I see the problem now

[Johan Commelin]

A grading let's you do that

[Johan Commelin]

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

[Johan Commelin]

It's called the "associated graded"

[Eric Wieser]

Right, that's what I'm after

[Eric Wieser]

"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"

[Eric Wieser]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Eric Wieser]

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

[Johan Commelin]

F is a filtration on a module M

[Johan Commelin]

So F^i M is a submodule of M

[Eric Wieser]

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

[Eric Wieser]

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.

[Reid Barton]

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.

[Eric Wieser]

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

[Reid Barton]

Can you link to the docs/source?

[Reid Barton]

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

[Eric Wieser]

docs#submodule.has_div

[Reid Barton]

docs#submodule.quotient

[Eric Wieser]

(deleted)

[Eric Wieser]

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

[Kevin Buzzard]

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.

[Reid Barton]

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

[Eric Wieser]

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