Zulip Chat Archive

Stream: maths

Topic: completion of module wrt ideal

Kenny Lau (Jul 14 2020 at 06:12):

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

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

Kenny Lau (Jul 14 2020 at 06:27):

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

Johan Commelin (Jul 14 2020 at 06:28):

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

Johan Commelin (Jul 14 2020 at 06:28):

Things like that?

Kenny Lau (Jul 14 2020 at 06:29):

how do I supply the ideal?

Johan Commelin (Jul 14 2020 at 06:29):

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

Johan Commelin (Jul 14 2020 at 06:29):

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

Kenny Lau (Jul 14 2020 at 06:29):

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

Johan Commelin (Jul 14 2020 at 06:31):

Is for_mathlib/nonarchimedean/adic_topology.lean helpful?

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.

Kenny Lau (Jul 14 2020 at 06:32):

aha it isn't general enough

Kenny Lau (Jul 14 2020 at 06:32):

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

Kenny Lau (Jul 14 2020 at 06:32):

instead of any module

Kenny Lau (Jul 14 2020 at 06:32):

also I think we might need a newtype?

Kenny Lau (Jul 14 2020 at 06:33):

or just jump straight to the completion

Johan Commelin (Jul 14 2020 at 06:33):

No, I would rather have a property

Johan Commelin (Jul 14 2020 at 06:33):

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

Kenny Lau (Jul 14 2020 at 06:33):

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

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 :=

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]

Kenny Lau (Jul 14 2020 at 06:34):

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

Kenny Lau (Jul 14 2020 at 06:34):

lim M/I^nM

Johan Commelin (Jul 14 2020 at 06:35):

We need that construction, of course.

Johan Commelin (Jul 14 2020 at 06:35):

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

Kenny Lau (Jul 14 2020 at 06:36):

oh I'll have the predicate for sure

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.

Kenny Lau (Jul 14 2020 at 06:37):

I'll leave that for later

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: Dec 20 2023 at 11:08 UTC