## Stream: Is there code for X?

### Topic: Difference between submodules

#### 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?

#### 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.

#### Eric Wieser (Nov 10 2020 at 09:56):

Does it exist for any other sub*objects?

#### Anne Baanen (Nov 10 2020 at 09:56):

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

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

#### Eric Wieser (Nov 10 2020 at 09:57):

Should submodule define that as has_sdiff?

#### 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).

#### Sebastien Gouezel (Nov 10 2020 at 10:01):

This is not a submodule in general...

#### Sebastien Gouezel (Nov 10 2020 at 10:01):

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

#### 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.

#### Johan Commelin (Nov 10 2020 at 10:07):

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

#### Eric Wieser (Nov 10 2020 at 10:08):

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

#### Johan Commelin (Nov 10 2020 at 10:08):

You need something like a grading to do that

#### 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?

#### 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)

#### Johan Commelin (Nov 10 2020 at 10:09):

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

#### 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.

#### Johan Commelin (Nov 10 2020 at 10:11):

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

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

#### Johan Commelin (Nov 10 2020 at 10:11):

A grading let's you do that

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

#### Eric Wieser (Nov 10 2020 at 10:13):

Right, that's what I'm after

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

#### Eric Wieser (Nov 10 2020 at 10:16):

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

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

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

#### Johan Commelin (Nov 10 2020 at 10:19):

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

#### Eric Wieser (Nov 10 2020 at 10:21):

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

#### Johan Commelin (Nov 10 2020 at 10:24):

F is a filtration on a module M

#### Johan Commelin (Nov 10 2020 at 10:24):

So F^i M is a submodule of M

#### Eric Wieser (Nov 10 2020 at 10:25):

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

#### 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.

#### 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.

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

#### Reid Barton (Nov 10 2020 at 12:10):

Can you link to the docs/source?

#### 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?

#### Eric Wieser (Nov 10 2020 at 12:22):

docs#submodule.has_div

#### Reid Barton (Nov 10 2020 at 12:37):

docs#submodule.quotient

(deleted)

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


#### 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.

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

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