arxiv: 2605.08108 · v1 · submitted 2026-04-27 · 🧮 math.RA · math.KT

Recognition: 2 theorem links

· Lean Theorem

The structure of lim¹-groups

Ioannis Emmanouil

Pith reviewed 2026-05-12 01:52 UTC · model grok-4.3

classification 🧮 math.RA math.KT

keywords lim^1 groupsinverse sequencesmodulesderived limitsfiltrationscompletionscokernelsexactness obstructions

0 comments

The pith

Every lim¹ group arising from an inverse sequence of modules is the cokernel of a map from a module to its completion.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that lim¹ groups, which arise as the first derived functor of the inverse limit for sequences of modules, always take a concrete form. For any given inverse sequence (X_n), there is a decreasing filtration (A_n) of some module A and a morphism from (A_n) to (X_n) that induces an isomorphism on lim¹. Under this identification, lim¹ equals the cokernel of the natural map from A to the completion lim A/A_n. This matters because it realizes abstract derived limits as explicit obstructions to surjectivity in the completion process, giving a uniform way to study them through filtered modules.

Core claim

If (A_n)_n is a decreasing filtration of a module A and the completion is defined as the inverse limit of the quotients A/A_n, then lim¹_n A_n is the cokernel of the canonical map A to its completion. The note proves that every lim¹ group is of this form: for any inverse sequence of modules (X_n)_n there exists a decreasing filtration sequence (A_n)_n of some module A together with a morphism (A_n)_n to (X_n)_n, depending functorially on the given sequence, that induces an isomorphism on lim¹.

What carries the argument

The functorial morphism of inverse sequences from a filtration sequence (A_n) of a module to an arbitrary sequence (X_n) that induces an isomorphism on the derived limit lim¹.

If this is right

Any algebraic property established for cokernels of maps to completions transfers directly to all lim¹ groups.
An arbitrary inverse system can be replaced by a filtered module system without changing the value of the derived limit.
The realization respects all morphisms of sequences, so diagrams involving lim¹ commute with the corresponding diagrams of completions.
Questions about vanishing or structure of lim¹ reduce to questions about the surjectivity of maps to completions in the filtered case.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

This form may allow explicit computations of lim¹ by choosing convenient filtrations for concrete sequences.
The result could link derived limits to other completion functors or exactness properties in module categories.
It raises the question of whether similar structural realizations exist for higher derived limits or in other abelian categories.

Load-bearing premise

The construction of the filtration sequence and the morphism requires that the category of modules contain enough special objects to build the required data functorially.

What would settle it

An explicit inverse sequence of modules for which no decreasing filtration sequence admits a morphism inducing an isomorphism on lim¹ would show the claim is false.

read the original abstract

If $(A_n)_n$ is a decreasing filtration of a module $A$ and $\widehat{A} = \lim_n A/A_n$, then $\lim^1_n A_n$ is identified with the cokernel of the canonical map $A \longrightarrow \widehat{A}$. In this note, we show that any $\lim^1$-group is canonically of that form: For any inverse sequence of modules $(X_n)_n$ there exists an inverse sequence $(A_n)_n$ as above and a morphism $(A_n)_n \longrightarrow (X_n)_n$, depending functorially on $(X_n)_n$, that induces an isomorphism on $\lim^1$. The proof is based on Quillen's small object argument, as formulated by Eklof and Trlifaj in their investigation of the existence of enough injective objects in certain cotorsion pairs, and also uses a construction by Salce that provides enough projective objects therein.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Every lim^1 arises functorially as the cokernel of a completion map A to hat A for some filtration, built via Eklof-Trlifaj and Salce.

read the letter

Every lim^1 of an inverse sequence of modules can be realized as the cokernel of the canonical map from a module to its completion with respect to a decreasing filtration, and this realization is functorial in the sequence. The paper achieves this by applying the Eklof-Trlifaj version of Quillen's small object argument to produce enough injectives in a suitable cotorsion pair, together with Salce's construction for enough projectives. This yields an inverse sequence (A_n) and a map to the given (X_n) that induces an isomorphism on lim^1. This is new in the sense that the functorial aspect via these tools does not appear in the cited prior work. It does well in giving a concrete, uniform representation that might streamline arguments involving lim^1 in homological algebra and related fields like K-theory. The argument looks sound because it builds on standard results that guarantee the existence of the required objects in the category of modules. There is no obvious circularity, as the tools are external and well-established. A minor soft spot could be the lack of explicit examples, which might help readers see how the construction works in practice, but that is not central. The central claim holds up based on the sketched proof. This paper is for specialists in homological algebra who encounter lim^1 groups and want a better handle on their structure. A reader working on exact sequences or filtrations would get value from the representation theorem. It deserves serious refereeing because it provides a new tool with potential applications, even if the immediate impact depends on how widely the functoriality gets used.

Referee Report

0 major / 2 minor

Summary. The manuscript claims that for any inverse sequence of modules (X_n), there exists a decreasing filtration (A_n) of a module A together with a functorial morphism (A_n) → (X_n) inducing an isomorphism on lim¹, thereby realizing every lim¹-group as the cokernel of the canonical map A → Â where Â = lim A/A_n. The argument proceeds by defining a suitable cotorsion pair in the category of modules (or inverse systems) and invoking the Eklof-Trlifaj formulation of Quillen's small-object argument to obtain enough injectives together with Salce's construction to obtain enough projectives.

Significance. If the central claim holds, the result supplies a canonical, functorial representation of arbitrary lim¹-groups in terms of filtered completions, which may streamline computations and structural arguments in homological algebra. The proof builds directly on established existence theorems (Eklof-Trlifaj and Salce) rather than introducing new ad-hoc constructions, which is a strength of the approach.

minor comments (2)

The abstract refers to '(A_n)_n as above' before the filtration is defined; a brief parenthetical reminder of the notation in the abstract would improve readability.
In the proof section, the verification that the induced map on lim¹ is an isomorphism could be accompanied by an explicit diagram chase or reference to the classical identification of lim¹ with the cokernel, to make the final step fully self-contained.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the manuscript and for recommending acceptance. The report contains no major comments.

Circularity Check

0 steps flagged

No significant circularity; central existence result constructed from external standard theorems

full rationale

The paper proves that any lim^1-group arises as the cokernel of A → Â for a filtration (A_n) by constructing a functorial morphism from such a filtration system to an arbitrary inverse sequence (X_n), using Quillen's small object argument (via Eklof-Trlifaj for enough injectives in cotorsion pairs) and Salce's construction for enough projectives. These are independent, externally verified results in the category of modules (or inverse systems), not derived from quantities defined inside the paper. The classical identification lim^1 ≅ coker(A → Â) is also external. No self-citation, self-definitional step, fitted-input prediction, or ansatz smuggling occurs; the derivation chain terminates in cited theorems that apply once the cotorsion pair is defined with a set-generated left class. The result is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on standard properties of inverse limits and derived functors together with known existence theorems for cotorsion pairs.

axioms (2)

standard math Standard properties of inverse limits, completions, and the derived functor lim^1 in the category of modules
Invoked throughout the identification and the main theorem.
domain assumption Existence of enough injective objects in the cotorsion pairs under consideration, via Quillen's small object argument
Explicitly cited as the basis for the construction, referencing Eklof-Trlifaj.

pith-pipeline@v0.9.0 · 5456 in / 1225 out tokens · 43341 ms · 2026-05-12T01:52:38.561804+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/AbsoluteFloorClosure.lean reality_from_one_distinction unclear
any lim¹-group is canonically of that form: For any inverse sequence of modules (X_n) there exists an inverse sequence (A_n) ... that induces an isomorphism on lim¹
IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel unclear
The proof is based on Quillen's small object argument, as formulated by Eklof and Trlifaj ... and also uses a construction by Salce

Reference graph

Works this paper leans on

13 extracted references · 13 canonical work pages

[1]

Angeleri-H¨ ugel, L.A., Bazzoni, S., Herbera, D.: A solution to the Baer splitting problem. Trans. Amer. Math. Soc.360, 2409-2421 (2008)

work page 2008
[2]

arXiv:2310.02716

Carelli, M., Ivanov, S.O.: Transfinite version of the Mittag-Leffler condition for the vanishing of the derived limit. arXiv:2310.02716

work page arXiv
[3]

Topology35, 267-271 (1996)

Emmanouil, I.: Mittag-Leffler condition and the vanishing of lim 1. Topology35, 267-271 (1996)

work page 1996
[4]

Eklof, P.C., Trlifaj, J.: How to make Ext vanish. Bull. London Math. Soc.33, 41-51 (2001)

work page 2001
[5]

Topology5, 241-243 (1966)

Gray, B.: Spaces of the samen-type, for alln. Topology5, 241-243 (1966)

work page 1966
[6]

Grothendieck, A.: EGA III. Publ. Math. IHES11(1961)

work page 1961
[7]

De Gruyter Expositions in Mathematics41, Berlin (2006)

G¨ obel, R., Trlifaj, J.: Approximations and Endomorphism Algebras of Modules. De Gruyter Expositions in Mathematics41, Berlin (2006)

work page 2006
[8]

Pacific J

Milnor, J.: On axiomatic homology theory. Pacific J. Math.32, 337-341 (1962)

work page 1962
[9]

Applications

Roos, J.E.: Sur les foncteurs d´ eriv´ es de lim ← − . Applications. C.R. Acad. Sc. Paris252, 3702-3704 (1961)

work page 1961
[10]

Salce, L.: Cotorsion theories for abelian groups. Sympos. Math.23, 11-32 (1979) Academic Press, New York

work page 1979
[11]

Lecture notes, Cortona workshop, 2000

Trlifaj, J.: Covers, envelopes and cotorsion theories. Lecture notes, Cortona workshop, 2000

work page 2000
[12]

Cambridge University Press (1994)

Weibel, C.: An introduction to homological algebra. Cambridge University Press (1994)

work page 1994
[13]

Thesis, Princeton, 1959 Department of Mathematics, University of Athens, Athens 15784, Greece E-mail address:emmanoui@math.uoa.gr

Yeh, Z.Z.: Higher inverse limits and homology theories. Thesis, Princeton, 1959 Department of Mathematics, University of Athens, Athens 15784, Greece E-mail address:emmanoui@math.uoa.gr

work page 1959