Zulip Chat Archive

Stream: maths

Topic: completion of module wrt ideal


view this post on Zulip Kenny Lau (Jul 14 2020 at 06:12):

@Patrick Massot what do we know about completion of module wrt ideal?

view this post on Zulip Johan Commelin (Jul 14 2020 at 06:13):

I guess we know that you get a topological add group... but the module structure is probably missing

view this post on Zulip Kenny Lau (Jul 14 2020 at 06:27):

@Johan Commelin what's the command to get the completion?

view this post on Zulip Johan Commelin (Jul 14 2020 at 06:28):

/topology/algebra/group_completion.lean:instance [has_zero α] : has_zero (completion α) := ⟨(0 : α)⟩

view this post on Zulip Johan Commelin (Jul 14 2020 at 06:28):

Things like that?

view this post on Zulip Kenny Lau (Jul 14 2020 at 06:29):

how do I supply the ideal?

view this post on Zulip Johan Commelin (Jul 14 2020 at 06:29):

Aha, you need to turn it into a uniform structure first.

view this post on Zulip Johan Commelin (Jul 14 2020 at 06:29):

We had that stuff in the perfectoid project. not sure if it is already in mathlib

view this post on Zulip Kenny Lau (Jul 14 2020 at 06:29):

I'm trying to find it in the perfectoid project also

view this post on Zulip Johan Commelin (Jul 14 2020 at 06:31):

Is for_mathlib/nonarchimedean/adic_topology.lean helpful?

view this post on Zulip Johan Commelin (Jul 14 2020 at 06:32):

Hmmm... maybe we don't actually have it on the nose. But we are epsilon away from it. There should be some way of turning an ideal into a filter basis. I really thought we had it.

view this post on Zulip Kenny Lau (Jul 14 2020 at 06:32):

aha it isn't general enough

view this post on Zulip Kenny Lau (Jul 14 2020 at 06:32):

that file is for the I-adic topology on the ring

view this post on Zulip Kenny Lau (Jul 14 2020 at 06:32):

instead of any module

view this post on Zulip Kenny Lau (Jul 14 2020 at 06:32):

also I think we might need a newtype?

view this post on Zulip Kenny Lau (Jul 14 2020 at 06:33):

or just jump straight to the completion

view this post on Zulip Johan Commelin (Jul 14 2020 at 06:33):

No, I would rather have a property

view this post on Zulip Johan Commelin (Jul 14 2020 at 06:33):

Is Z_p the adic completion of Z? It won't fit your newtype...

view this post on Zulip Kenny Lau (Jul 14 2020 at 06:33):

as in, the I-adic topology on M cannot be an instance

view this post on Zulip Kenny Lau (Jul 14 2020 at 06:34):

-- Note: making the following an instance is useless, instance resolution would never guess I
def adic_basis (I : ideal R) : subgroups_basis R :=

view this post on Zulip Johan Commelin (Jul 14 2020 at 06:34):

{M : Type*} [add_group M] [topological_space M] [topological_module R M] [is_adic_topology I M]

view this post on Zulip Kenny Lau (Jul 14 2020 at 06:34):

you know what, I much prefer construct the direct limit directly

view this post on Zulip Kenny Lau (Jul 14 2020 at 06:34):

lim M/I^nM

view this post on Zulip Johan Commelin (Jul 14 2020 at 06:35):

We need that construction, of course.

view this post on Zulip Johan Commelin (Jul 14 2020 at 06:35):

But it shouldn't be the only way to talk about things being adically complete

view this post on Zulip Kenny Lau (Jul 14 2020 at 06:36):

oh I'll have the predicate for sure

view this post on Zulip Johan Commelin (Jul 14 2020 at 06:36):

What we actually need, is to show that the two ways of completing (algebraic and topological) give "the same" result.

view this post on Zulip Kenny Lau (Jul 14 2020 at 06:37):

I'll leave that for later

view this post on Zulip Patrick Massot (Jul 14 2020 at 06:55):

I'm sorry Kenny, I'm fully focused on my talk that will start in one hour so I won't elaborate. We don't have what you want out of the box but it's very close.


Last updated: May 11 2021 at 16:22 UTC