New user, planning to do some homological algebra

Stream: new members

[Liran Shaul]

Hi, I am Liran Shaul, an homological algebraist from Prague. I have some plans to try to add some major results in Homological algebra to Lean. As a small test, I just added to the injective module file in matlab a result showing that direct product of injectives is injective. I think I was able to push this to the github, but it was not yet approved. I am not sure if I need to do anything for it to be approved.

[Bryan Gin-ge Chen]

Welcome! Looks like your PR is at #31263 and is waiting for CI to finish seeing if the code compiles and passes linting, etc. You probably have already seen it but our guide for contributors is here and describes the contribution flow in some detail.

[Liran Shaul]

Bryan Gin-ge Chen said:

Welcome! Looks like your PR is at #31263 and is waiting for CI to finish seeing if the code compiles and passes linting, etc. You probably have already seen it but our guide for contributors is here and describes the contribution flow in some detail.

Thank you! I did not see this before. It is helpful.

[Axel Boldt]

It seems that in the rest of Injective.lean, they consider slightly more general situations where the ring R can belong to any universe, not just to Type like in your addition. Also, they seem to have certain naming conventions for their theorems which you aren't following. Maybe that's why the pull request is held up.

[Liran Shaul]

I hope someone could help me. I accepted some suggestions for imporvements, but after accepting one of them, it stopped compiling. I tried to revert back to last known version, but it still seem to suggest an error on github, despite working earlier. Can anyone take a look? thank you.

[Michael Rothgang]

I can take a look at your PR and give you some style feedback; hopefully tomorrow.

[Andrew Yang]

Have you tried to open the file locally? It should tell you the error.

[Liran Shaul]

I am now pleased to announce that I was able to get to zero sorries on my project. I will put the full details on the arxiv soon once I finish writing the paper describing it. Here are the highlights of the project:

1. Pushouts of modules

The project develops from scratch the theory of pushouts in the category of $R$ -modules. Given linear maps $f: A \to B$ and $g: A \to C$ , the pushout $B \sqcup_A C$ is constructed as the quotient $(B \oplus C)/\langle (f(a), -g(a)) \mid a \in A \rangle$ , together with its universal property. Key results include the identification of $\operatorname{coker}(\mathtt{inr})$ with $\operatorname{coker}(f)$ , and, crucially, a base-change compatibility: $S \otimes_R (B \sqcup_A C) \cong (S \otimes_R B) \sqcup_{S \otimes_R A} (S \otimes_R C)$ .

2. Universal injectivity

A linear map $f: M \to N$ is called universally injective (or pure) if $f \otimes_R \mathrm{id}_Q: M \otimes_R Q \to N \otimes_R Q$ is injective for every $R$ -module $Q$ . The file establishes:

• A universally injective map is in particular injective.
• (Stacks 058K, (1)$\Rightarrow$ (4)) If $f$ is universally injective, it has the right lifting property against maps between finite free modules: given a commutative square with $k: F \to G$ a map of finite free modules and $h: G \to N$ , $g: F \to M$ with $h \circ k = f \circ g$ , there exists $\varphi: G \to M$ with $\varphi \circ k = g$ .
• Universal exactness and lifting for finitely presented modules: If $0 \to X_1 \xrightarrow{f} X_2 \to X_3 \to 0$ is a short exact sequence with $f$ universally injective, then any map from a finitely presented module $P$ to $X_3$ lifts to $X_2$ .
• Descent of universal injectivity along faithfully flat base change: If $S$ is faithfully flat over $R$ and $f \otimes S: M \otimes_R S \to N \otimes_R S$ is universally injective (as an $S$ -module map), then $f$ is universally injective over $R$ . This uses the natural isomorphism $S \otimes_R (M \otimes_R Q) \cong (S \otimes_R M) \otimes_S (S \otimes_R Q)$ .

3. Domination and the pushout criterion

Given linear maps $f: M \to N$ and $g: M \to M'$ , one says $g$ dominates $f$ (written $f \preceq g$ ) if $\ker f \subseteq \ker g$ , i.e., $g$ factors through the image of $f$ . The file proves:

• Domination is a preorder (reflexive and transitive) and is preserved by composition on the right.
• The canonical map $\mathtt{inr}: M' \to M' \sqcup_M N$ into the pushout is universally injective if and only if $g$ dominates $f$ (Stacks 0ASL / Lemma 10.88.4). The proof proceeds via an explicit analysis of $\ker(\mathtt{inr})$ and its behavior under tensor product.
• A universally injective short exact sequence splits: the universally injective map is a split monomorphism.
• An equivalent characterization: $g$ dominates $f$ if and only if $g$ factors through some module that factors $f$ .

4. The Mittag-Leffler condition

Inverse systems. A projective system of sets $(F_i, f_{ij})$ over a directed poset satisfies the Mittag-Leffler condition if for every $i$ there exists $j \geq i$ such that $\mathrm{Im}(f_{ij}: F_j \to F_i) = \mathrm{Im}(f_{kj}: F_k \to F_i)$ for all $k \geq j$ (the images eventually stabilize). The file proves:

• The Mittag-Leffler condition is equivalent to eventually stable images.
• If a system has surjective transition maps, it satisfies Mittag-Leffler.
• The non-emptiness of the inverse limit for Mittag-Leffler systems indexed by a countable directed set.

• The Mittag-Leffler exactness theorem: a short exact sequence $0 \to A_i \to B_i \to C_i \to 0$ of Mittag-Leffler inverse systems gives an exact sequence $0 \to \varprojlim A_i \to \varprojlim B_i \to \varprojlim C_i \to 0$ on inverse limits.
  Modules. An $R$ -module $M$ is Mittag-Leffler if for every directed system of $R$ -modules $(N_i, f_{ij})$ with colimit $N$ , the inverse system $(\mathrm{Hom}_R(M, N_i))$ satisfies the Mittag-Leffler condition. Several equivalent reformulations are proved, including one in terms of finitely presented test modules (the definition matching Stacks 059M). Stability properties include:

• Finitely presented modules are Mittag-Leffler.

• Free modules are Mittag-Leffler.
• Direct summands of Mittag-Leffler modules are Mittag-Leffler.
• Projective modules are Mittag-Leffler (since they are direct summands of free modules).
• A countably generated Mittag-Leffler module has a presentation as a colimit of a countable system.

5. Kaplansky's theorem and devissage

This file contains the transfinite devissage machinery. A Kaplansky devissage of an $R$ -module $M$ indexed by an ordinal $S$ is a filtration $M_0 \subseteq M_1 \subseteq \cdots$ (indexed by $\alpha < S$ ) such that: it starts at $0$ , has union $M$ , is continuous at limit ordinals, and each successive quotient $M_{\alpha+1}/M_\alpha$ is countably generated. The key results are:

• Kaplansky devissage $\Leftrightarrow$ direct sum decomposition (kaplansky_devissage_iff_direct_sum): $M$ admits a Kaplansky devissage if and only if $M \cong \bigoplus_{i \in I} M_i$ where each $M_i$ is countably generated. This is proved by a transfinite induction constructing the devissage from a given decomposition and vice versa.
• Direct summands inherit decomposability (dirsummand_of_dirSumCountable): If $M$ is a direct sum of countably generated modules and $N$ is a direct summand of $M$ , then $N$ is also a direct sum of countably generated modules. This is proved by a long transfinite induction building a Kaplansky devissage for $N$ from the one on $M$ via the retraction.

6. Lazard's theorem

This file establishes Lazard's theorem: a flat module is a filtered colimit of finitely generated free modules. The key steps are:

• Every finitely presented module is a compact object in the category of $R$ -modules (maps from it into a filtered colimit factor through a finite stage).
• Direct limits of flat modules are flat.
• Flat modules can be enlarged to free modules: if $M$ is flat, there is a free module $F \supseteq M$ such that $M$ is a direct summand of $F$ (locally), enabling the construction of a filtered system of free modules approximating $M$ .
• Lazard's theorem (Module.Flat.Lazard): $M$ is flat if and only if it is a filtered (direct) colimit of finite free modules.

7. Base change and the main result (basechange.lean, dirlimitchange.lean)

The final assembly. The file dirlimitchange.lean establishes the key commutation: $S \otimes_R \varinjlim_i G_i \cong \varinjlim_i (S \otimes_R G_i)$ as an $S$ -linear isomorphism, compatibly with the natural maps.

The file basechange.lean then proves:

• Free modules base change projectively (trivially).
• Projectivity is preserved under faithful flat base change in the easy direction: if $P$ is projective over $R$ , then $S \otimes_R P$ is projective over $S$ .

• Projectivity $\Leftrightarrow$ countable flat + Mittag-Leffler (for finitely or countably generated modules): a countably generated flat Mittag-Leffler module is projective (using Lazard's theorem plus the Kaplansky/devissage machinery).

• The Main Theorem (proj_faithfullyFlat): if $R\to S$ is a faithfully flat map of commutative rings, and $P$ is an $R$-module such that $S \otimes_R P$ is projective over $S$ then $P$ is projective over $R$ .

[Martin Dvořák]

Hello! I am happy to see another person working with Lean in Czechia! But what is the wall of text you just pasted here?

[Liran Shaul]

Hi, thank you! sorry for the wall of text. It was an attempt to summerize the formalization project I just finished, but I guess it might be too massive for such a post. I hope to post the arxiv version in about a week.