Artin-Rees and friends

Stream: mathlib4

[Christian Merten]

One way to show that smooth ring homomorphisms are flat uses that the I-adic completion of a noetherian ring R with respect to an ideal I is flat over R. A few questions:

• The proof I know uses the Artin-Rees lemma. As far as I can tell, this does not exist yet, but docs#reesAlgebra exists. @Andrew Yang: Since you defined the Rees algebra, are you working on the Artin-Rees lemma? By any chance, do you know a direct way to show flatness of the I-adic completion?
• Why is docs#adicCompletion defined as an explicit submodule of ∀ n : ℕ, M ⧸ (I ^ n • ⊤ : Submodule R M) as opposed to the categorical limit over a suitable diagram?

[Andrew Yang]

@loogle "Artin-Rees"

[loogle]

:shrug: nothing found

[Andrew Yang]

I thought loogle searched in docstrings as well?

[Andrew Yang]

docs#Ideal.exists_pow_inf_eq_pow_smul Is this what you are looking for?

[Christian Merten]

Thanks!

[Christian Merten]

Could I raise attention to my second question?
Christian Merten said:

• Why is docs#adicCompletion defined as an explicit submodule of ∀ n : ℕ, M ⧸ (I ^ n • ⊤ : Submodule R M) as opposed to the categorical limit over a suitable diagram?

I am wondering, because I'll have to work on exactness properties of I-adic completions for which having the limit version seems to come in handy.

[Johan Commelin]

I wouldn't be surprised if the answer is in large part: "history". I think this was developed a long time ago by Kenny Lau. The category library was much more in flux back then. And Kenny was on a constructive streak, so he didn't want to "choose" a limit.

[Andrew Yang]

I don't have a strong opinion here, but a possible deficiency of using the category theory library is that it is not universe polymorphic. In particular, if M is a colimit of some family of M i : Type u, it is not completely trivial to use the category library to lift some family of M i ->* N to M ->* N for some N : Type v without going through some ulift shenanigans. The fact that ulifting groups does not preserve colimits doesn't show a good sign as well, though I think it is well-behaved for limits of modules.

[Mario Carneiro]

shouldn't it be possible to prove it's a limit anyway? Categorical notions are usually only defined up to isomorphism anyway. (Plus universal constructions in lean are fundamentally restricted due to universe issues as Andrew says.)

[Andrew Yang]

Nonetheless we can either

1. Disregard the universe issue and treat it later when we really need to
2. Provide some wrapper API for ulift shenanigans.

[Christian Merten]

I personally think we should try the "ulift shenanigans" strategy instead of always falling back to doing things explicitly by hand. But for now maybe we can choose Andrews option 1, i.e. disregard universe issues for now?

In any case we will need (commutative) ring and algebra versions of docs#adicCompletion. And for good definitional properties I suppose the ring version should be defined as the limit over R ⧸ (I ^ n) instead of R ⧸ (I ^ n • R) which docs#adicCompletion would specialize to. Then there should be comparison isomorphisms relating the three (module, ring and algebra) adic completions. Do you agree?

[Joël Riou]

You may put suitable instances on a type Functor.sections, and not rely too much on the category theory limits API, even though when the universe are well suited, this is the point of a limit cone in the category of types (and also, in other categories as forgetful functors should at least reflects these limits).

[Kevin Buzzard]

I am happy to use Type u in my code, but the moment I have problems with Type u and Type v I just switch to u = v rather than trying to fix them, because secretly I am confident that I will never care about multiple universe polymorphism.

[Adam Topaz]

Johan Commelin said:

I wouldn't be surprised if the answer is in large part: "history". I think this was developed a long time ago by Kenny Lau. The category library was much more in flux back then. And Kenny was on a constructive streak, so he didn't want to "choose" a limit.

One shouldn't choose anything anyway. We should have a IsAdicCompletion class.

[Christian Merten]

I managed to prove exactness of adic completion over noetherian rings for f.g. modules with the current definition without going through category theory. This seems okay, but not ideal, as it essentially mimics the proof of exactness of inverse limits when the appropriate inverse system has surjective transition maps.

• Given a short exact sequence $0 \to (M_i) \to (N_i) \to (P_i) \to 0$ of inverse systems indexed by a countable set $I$ where the system $(M_i)$ is Mittag-Leffler, the induced sequence on inverse limits is exact. The proof I know for this is the following: Since the index set is countable and cofiltered, we find $\mathbb{N}$ as a cofinal subset. Hence we are reduced to the case of $I = \mathbb{N}$. By Mittag-Leffler we may also assume that the transition maps in $(M_i)$ are surjective. This refined statement is now shown by induction.
• To show this in full generality (for a cofiltered countable index category) we need the generalization of docs#CategoryTheory.Limits.sequentialFunctor_initial, which I currently don't want to spend time on. But, if we stick to the strategy outlined in the first bullet point, I am happy to show the refined version for $I = \mathbb{N}$, since that is the case needed for adic completions. One then at least gets the version for countable, cofiltered, preorderd sets via docs#CategoryTheory.Limits.sequentialFunctor_initial.
• Are you okay with the strategy outline in the first bullet point and with handling the case of $I = \mathbb{N}$ first and generalize later via the docs#CategoryTheory.Functor.Initial API?

[Andrew Yang]

I think it is perfectly fine to go for $I = \mathbb{N}$ first.

[Christian Merten]

Do we want API for working with sequential limits?

[Andrew Yang]

Of course! Any API useful for you is probably useful to someone else. Any development is greatly appreciated.

[Christian Merten]

So I am showing exactness in AddCommGroupCat right?

[Christian Merten]

Concerning adic completions: I have tried out a few things and decided to follow the following path:

• Keep docs#adicCompletion mostly as is but rename to AdicCompletion.
• Make an AdicCompletion folder and maybe move to Mathlib/RingTheory (currently it is in LinearAlgebra).
• Add the universal lifting property by manual construction (since this is very easy, no machinery is needed).
• Add a type AdicCauchySequence as a submodule of ∀ n, M, a surjective linear map AdicCauchySequence I M →ₗ[R] AdicCompletion I M and a corresponding induction principle.
• Provide comparison ismorphisms to the sections of the corresponding functor ℕᵒᵖ ⥤ ModuleCat.{u} R.
• For the algebra version: Don't introduce a second AdicCompletionAlgebra, but provide a Algebra R (AdicCompletion I R) instance, deduced from it being a R-subalgebra of ∀ n , R ⧸ (I^n • ⊤ : Ideal R).
• Since working with R ⧸ (I^n • ⊤ : Ideal R) is stupidly annoying (note that this is not def-eq to R ⧸ I^n), mimic the API for modules for algebras, in particular add constructors for AdicCauchySequence I R from the compatibility condition involving only R ⧸ I ^ n and Algebra homomorphisms AdicCompletion I R →ₐ[R] R ⧸ I ^ n.

I would appreciate any comments on the outlined steps.

[Kevin Buzzard]

Given that we just changed ringOfIntegers (a subring) to RingOfIntegers (a type) and this solved some slowdowns, I think that this approach is probably a good idea.

[Christian Merten]

I am confused: is this ringOfIntegers change still pending? Never mind, I found the PR.

[Christian Merten]

The starting point is #12516. For functoriality: #12543 and for the algebra instance: #12553.