Chapter 3. Tor and Ext
FC05 — Weibel, An Introduction to Homological Algebra.
This chapter contains 10 definitions, 6 theorems, 8 propositions, 9 lemmas, 8 corollaries, 5 examples, 3 constructions and 17 other statements.
Of the 66 statements checked against Lean, 5 are formalized somewhere and 61 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 61 | 92% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 4 | 6% | Mathlib states and proves it. |
| in lean-categories | 1 | 2% | This repository states and proves it. |
| checked in total | 66 |
- Project-first search was performed at repo HEAD
f901738.LeanCategories/Homological/Extensions.leanexportsLeanCategories.Homological.ExtensionandExtension.Equivfor arbitrary rings. Its module docstring mentions the Baer sum, but no Baer-sum operation or Ext¹ classification is implemented there. PinnedShortComplex.Splittingsupplies the split-sequence side, so U036 is the only project-existing C03 route. - Pinned Mathlib is
P=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0.Module.FinitePresentationis defined for arbitrary semirings/rings and gives the exact finite-generator/finite-relation presentation of U014.CharacterModule.dual_surjective_iff_injective, specialized to scalar ring ℤ on the underlying additive map, gives U013. GenericLimits.limandFunctor.rightDerivedprovide the derived inverse-limit construction U043 and its countable-tower specialization U044 under the usual completeness/enough-injectives assumptions. - The chapter continues Weibel’s arbitrary-associative-ring convention. P/H
Module.Flatis declared only under[CommSemiring R], andMathlib/LinearAlgebra/TensorProduct/Basic.leanstill uses a commutative scalar ring (with an explicit TODO/comment about the missing right-action generalization). Therefore the arbitrary-ring flatness/Tor, central-localization, character-module, and tensor-based rows are not credited from commutative Mathlib implementations. - Current Mathlib was rechecked at
H=5aedf732b6987e8c26ab3c9ebc855314f82b045f. Targeted source search found no Baer sum/Yoneda-Ext classification, no explicit Tor/Ext calculations required by C03, nolim¹/Milnor/Roos development, and no Künneth or universal-coefficient theorem matching the source rows. - Pinned
CategoryTheory/CofilteredSystem.leanprovidesFunctor.IsMittagLefflerand stabilization/eventual-range theorems, but not Weibel’s additional “trivial Mittag–Leffler” definition nor the theoremMittag–Leffler ⇒ lim¹=0; the file itself lists a related Stacks lemma as TODO. Under strict whole-row semantics U052 and U053 therefore remain unmatched. - The project/P/H extension searches found no Baer-sum construction, abelian-group structure on extension classes, or classification by
Abelian.Ext. Generic intrinsic Ext and its projective/injective resolution computations were already mapped in FC05 C02; they do not by themselves realize the C03 extension-classification rows U037–U042. - External search on 2026-09-06 for Künneth, universal coefficient, Milnor exact sequences, Mittag–Leffler/right-derived limit,
lim1, Baer sum, and Yoneda Ext found no proved source-general implementation.deancureton/sphere-six-complex@895c0a0661501581c34d42fea3c553d4f0ee43b1has a file namedClassicalIntegralUCTBoundary.lean, but its general integral singular-cohomology UCT is introduced aspublic axiom classicalIntegralSingularCohomologyUCT; it is not a proof and is not a mapping route. - The older definition-only Weibel catalogue is not route authority. Its flat/Tor hints silently lose the source’s arbitrary-ring right/left-module generality, and its Mittag–Leffler/AB4* hints do not supply the complete source bundles checked here.
Ndenotes dated 2026-09-06 negative evidence after project-first inspection, P, H/current Mathlib, and targeted external Lean search. Generic derived-functor infrastructure, a commutative-only specialization, an axiom, or an adjacent definition does not count as realization of an explicit calculation/comparison theorem under strict bundle semantics.
Calculation 3.1.1 — Tor of Z/p
For abelian B: Tor_0^Z(Z/p,B)=B/pB, Tor_1^Z(Z/p,B)={b:pb=0}, and Tor_n=0 for n≥2, from the length-one free resolution.
Not formalized. partial: generic homological/derived infrastructure — No checked explicit calculation of Tor₁^ℤ(ℤ/p,B) was found; the generic Tor owner is not an explicit computation.
Proposition 3.1.2 — Tor over Z has only degree-one torsion
For abelian A,B, Tor_1^Z(A,B) is torsion and Tor_n^Z(A,B)=0 for n≥2.
Not formalized. partial: generic homological/derived infrastructure — No checked theorem computes all higher Tor over ℤ in the source form.
Proposition 3.1.3 — Tor with Q/Z detects torsion
Tor_1^Z(Q/Z,B) is the torsion subgroup of B.
Not formalized. partial: generic homological/derived infrastructure — No checked theorem identifies Tor₁^ℤ(ℚ/ℤ,B) with the torsion subgroup.
Proposition 3.1.4 — Torsionfree abelian groups are Tor-acyclic
If A is torsionfree abelian, Tor_n^Z(A,B)=0 for n>0 and every B.
Not formalized. partial: generic homological/derived infrastructure — Pinned torsion-free/flat results over Bezout domains are adjacent, but no checked whole row identifies all higher Tor-acyclicity in the source form.
Reusable comparison — Balancing Tor over a commutative ring
For commutative R, Tor_^R(A,B)≅Tor_^R(B,A); in particular Tor_1^Z(A,Q/Z) is the torsion subgroup of A.
Not formalized. partial: generic homological/derived infrastructure — The source balance is stated for commutative R, but pinned Tor explicitly lacks the two-variable balancing theorem.
Corollary 3.1.5 — Torsionfree iff first Tor vanishes
For abelian A, Tor_1^Z(A,-)=0 iff A is torsionfree iff Tor_1^Z(-,A)=0.
Not formalized. partial: generic homological/derived infrastructure — No checked theorem gives the source torsion-free iff Tor₁(-,A)/Tor₁(A,-) vanishing criterion for all abelian groups.
Calculation 3.1.6 — Periodic Tor over Z/m
For d∣m, the periodic free resolution of Z/d over Z/m gives the stated alternating formulas for Tor_n^{Z/m}(Z/d,B) in all degrees.
Not formalized. partial: generic homological/derived infrastructure — No checked periodic Tor calculation for ℤ/m was found.
Example 3.1.7 — Tor with a regular element
If r is a left nonzerodivisor on R, then Tor_0^R(R/rR,B)=B/rB, Tor_1={b:rb=0}, and higher Tor vanishes.
Not formalized. partial: generic homological/derived infrastructure — No checked regular-element quotient Tor computation was found.
Definition 3.2.1 — Flat module
A left module B is flat when -⊗_R B is exact; right flatness is dual. Projectives are flat, but flat need not be projective.
Not formalized. partial: generic homological/derived infrastructure — Weibel defines flatness for modules over arbitrary associative rings. P/H Module.Flat is declared only under [CommSemiring R] and lists noncommutative generalization as TODO.
Theorem 3.2.2 — Localization is flat
For a central multiplicative set S⊂R, S^{-1}R is flat as an R-module, realized as a filtered colimit of free modules.
Not formalized. partial: generic homological/derived infrastructure — Weibel uses localization at a central multiplicative set in a possibly noncommutative ring. P/H localization-flatness APIs are commutative-base.
Definition 3.2.3 — Pontryagin dual
For a left R-module B, B*=Hom_Ab(B,Q/Z) with right action (fr)(b)=f(rb).
Not formalized. partial: generic homological/derived infrastructure — P/H character modules are developed over commutative scalars; no checked owner gives the source right R-module structure on Hom_Ab(B,ℚ/ℤ) for arbitrary associative R.
Proposition 3.2.4 — Equivalent criteria for flatness
For a left R-module B: flatness, injectivity of B*, injectivity of I⊗B→B for right ideals I, and Tor_1^R(R/I,B)=0 are equivalent.
Not formalized. partial: generic homological/derived infrastructure — The source flatness equivalence bundle is arbitrary-ring and includes the noncommutative character-module criterion; P/H do not cover that generality.
Lemma 3.2.5 — Pontryagin dual detects injections
f:B→C is injective iff f:C→B* is surjective.
Formalized. CharacterModule.dual_surjective_iff_injective (apply after restricting the underlying additive map to ℤ) — The pinned character module is Hom_Ab(-,ℚ/ℤ) at scalar ring ℤ; dualization is surjective exactly when the original map is injective, which is the source detection statement for any underlying abelian-group map.
Searched: P
Definition — Finitely presented module
M is finitely presented if it has a presentation Rm→Rn→M→0 with m,n finite.
Formalized. Module.FinitePresentation; Module.FinitePresentation.exists_fin' — Pinned finite presentation is defined for arbitrary semirings/rings, not only commutative ones, and gives exactly a finite-generator finite-relation presentation.
Searched: P
Construction — Natural evaluation map σ
Defines σ:A*⊗_R M→Hom_R(M,A)* by σ(f⊗m)(h)=f(h(m)).
Not formalized. partial: generic homological/derived infrastructure — The evaluation map uses the arbitrary-ring right/left tensor product, absent from P/H.
Lemma 3.2.6 — σ is an isomorphism for finitely presented modules
For finitely presented M, the natural σ:A⊗M→Hom_R(M,A) is an isomorphism for all A.
Not formalized. partial: generic homological/derived infrastructure — The finite-presentation evaluation isomorphism depends on U015’s noncommutative tensor construction.
Theorem 3.2.7 — Finitely presented flat modules are projective
Every finitely presented flat R-module is projective.
Not formalized. partial: generic homological/derived infrastructure — P/H prove finitely-presented-flat implies projective in commutative settings, but the source row is for arbitrary associative rings.
Flat Resolution Lemma 3.2.8 — Tor can be computed from flat resolutions
A resolution of either variable by flat modules computes Tor by tensor homology, not only projective resolutions.
Not formalized. partial: generic homological/derived infrastructure — No noncommutative flat-resolution/Tor owner exists in P/H.
Proposition 3.2.9 — Flat base change for Tor
If R→T and T is flat over R, then Tor_nR(A,C)≅Tor_nT(A⊗_R T,C) for R-module A and T-module C.
Not formalized. partial: generic homological/derived infrastructure — No checked source-general flat-base-change theorem for Tor was found.
Corollary 3.2.10 — Two-sided flat base change for Tor
For commutative R and flat R-algebra T, T⊗_R Tor_nR(A,B)≅Tor_nT(A⊗T,T⊗B).
Not formalized. partial: generic homological/derived infrastructure — Even in the commutative specialization, no checked Tor base-change isomorphism matching the row was found.
Lemma 3.2.11 — Central scalar action on Tor
Multiplication by a central r on A induces multiplication by r on Tor_n^R(A,B).
Not formalized. partial: generic homological/derived infrastructure — The scalar action is on arbitrary-ring Tor and depends on the missing noncommutative Tor owner.
Corollary 3.2.12 — Tor inherits quotient-ring module structure
If A is an R/r-module, then Tor_*^R(A,B) is annihilated by r and hence is an R/r-module.
Not formalized. partial: generic homological/derived infrastructure — The quotient-ring Tor module structure depends on the same missing arbitrary-ring Tor layer.
Corollary 3.2.13 — Localization criterion for vanishing of Tor
For commutative R, Tor_n^R(A,B)=0 iff all prime localizations vanish, equivalently all maximal localizations vanish.
Not formalized. partial: generic homological/derived infrastructure — No checked localization criterion for Tor vanishing at all maximals was found.
Lemma 3.3.1 — Ext over Z vanishes above degree one
For abelian groups A,B, Ext_Z^n(A,B)=0 for n≥2.
Not formalized. partial: generic homological/derived infrastructure — No checked theorem states the full Ext^n_ℤ=0 calculation for n≥2 in this source form.
Calculation 3.3.2 — Ext from Z/p
Ext_Z^0(Z/p,B) is the p-torsion subgroup, Ext_Z^1(Z/p,B)=B/pB, and higher Ext vanishes.
Not formalized. partial: generic homological/derived infrastructure — No checked explicit computation of Ext¹_ℤ(ℤ/p,B) was found.
Example 3.3.3 — Ext of torsion groups into Z
For torsion A, Hom(A,Z)=0 and Ext_Z^1(A,Z)=A*; in particular Ext_Z^1(Z_{p∞},Z) is the p-adic integers.
Not formalized. partial: generic homological/derived infrastructure — No checked Lean computation identifies these Ext groups with the torsion quotients/p-adic integers.
Proposition 3.3.4 — Ext and arbitrary sums/products
Ext_Rn(⊕A_α,B)≅∏Ext_Rn(A_α,B) and Ext_Rn(A,∏B_β)≅∏Ext_Rn(A,B_β).
Not formalized. partial: generic homological/derived infrastructure — Pinned Ext has finite biproduct additivity, not the arbitrary sums/products formulas in this row.
Examples 3.3.5 — Infinite Ext examples
Applies the product formulas to countably infinite Z/p-vector spaces and to B=∏_{p≥2}Z/p, illustrating large Ext and divisibility detection.
Not formalized. partial: generic homological/derived infrastructure — No checked implementation of the stated infinite-rank Ext calculations was found.
Lemma 3.3.6 — Scalar action on Ext
For commutative R, multiplication by r in either argument induces multiplication by r on Ext_R^n(A,B).
Not formalized. partial: generic homological/derived infrastructure — No checked owner gives the source scalar action on Ext in the stated module-theoretic form.
Corollary 3.3.7 — Ext inherits quotient-ring module structure
If A is an R/r-module, Ext_R^*(A,B) is naturally an R/r-module.
Not formalized. partial: generic homological/derived infrastructure — No checked quotient-ring scalar/module structure on Ext matching the row was found.
Construction/comparison — Localization map for Hom
Defines Φ:S{-1}Hom_R(A,B)→Hom_{S{-1}R}(S{-1}A,S{-1}B) and notes finite presentation as a sufficient hypothesis for it to be an isomorphism.
Not formalized. partial: generic homological/derived infrastructure — P/H Hom-localization theorems use commutative localization; the source permits central localization in a possibly noncommutative ring.
Lemma 3.3.8 — Hom localizes for finitely presented source
If A is finitely presented and S central multiplicative, Φ is an isomorphism.
Not formalized. partial: generic homological/derived infrastructure — Module.FinitePresentation.linearEquivMap is pinned for commutative localization, but does not realize the source central noncommutative localization statement.
Definition 3.3.9 — Noetherian ring and finite free resolutions
A right noetherian ring has every right ideal finitely generated; finitely generated modules are finitely presented and admit resolutions by finitely generated free modules.
Not formalized. partial: generic homological/derived infrastructure — P/H have Noetherian/finitely-presented module infrastructure but no checked packaged finite free resolution with all terms finitely generated as stated.
Proposition 3.3.10 — Ext commutes with localization under noetherian finiteness
For commutative noetherian R and finitely generated A, S{-1}Ext_Rn(A,B)≅Ext_{S{-1}R}n(S{-1}A,S{-1}B).
Not formalized. partial: generic homological/derived infrastructure — No checked Ext-localization isomorphism matching the source Noetherian/finite hypotheses was found.
Corollary 3.3.11 — Localization criterion for vanishing of Ext
Under the same hypotheses, Ext_R^n(A,B)=0 iff its localizations at all prime ideals vanish, equivalently all maximal ideals.
Not formalized. partial: generic homological/derived infrastructure — No checked local-global vanishing criterion for Ext was found.
Definition — Extensions and equivalence; split extension
An extension of A by B is 0→B→X→A→0; equivalence is an isomorphism of such sequences fixing A,B. The canonical A⊕B sequence is split.
Formalized. LeanCategories.Homological.Extension; Extension.Equiv; P ShortComplex.Splitting — LeanCategories owns extensions and endpoint-identity equivalences for arbitrary rings; pinned short-complex splitting supplies the split-extension/canonical biproduct side of the source definition.
Searched: P
Lemma 3.4.1 — Ext^1=0 forces all extensions to split
If Ext^1(A,B)=0, every extension of A by B splits, by lifting id_A through Hom(A,X)→Hom(A,A).
Not formalized. partial: generic homological/derived infrastructure — Without an Ext¹/extension classification theorem, the vanishing iff every extension splits statement is not represented.
Porism 3.4.2 — Obstruction class Θ(ξ)
For an extension ξ, Θ(ξ)=∂(id_A)∈Ext^1(A,B) depends only on its equivalence class and vanishes exactly when ξ splits.
Not formalized. partial: generic homological/derived infrastructure — The obstruction map Θ from an extension to derived Ext¹ is not exported by project or Mathlib.
Theorem 3.4.3 — Ext^1 classifies extensions
Θ gives a bijection between equivalence classes of extensions of A by B and Ext_R^1(A,B), carrying the split extension to 0.
Not formalized. partial: generic homological/derived infrastructure — No checked classification of extension-equivalence classes by Ext¹ was found.
Definition 3.4.4 — Baer sum
Defines the sum of two extensions by pullback over A followed by quotient by the skew-diagonal copy of B.
Not formalized. partial: generic homological/derived infrastructure — The project module docstring mentions Baer sum but exports no Baer-sum construction; P/H/current/external search found none.
Corollary 3.4.5 — Extensions form an abelian group identified with Ext^1
Equivalence classes of extensions form an abelian group under Baer sum, and Θ is a group isomorphism to Ext^1(A,B).
Not formalized. partial: generic homological/derived infrastructure — No checked abelian-group structure on extension classes or isomorphism with Ext¹ was found.
Vista 3.4.6 — Yoneda Ext groups
Defines Ext^n in an abelian category via equivalence classes of n-fold exact extensions, with Baer/Yoneda addition; when enough projectives exist this agrees with derived-functor Ext.
Not formalized. partial: generic homological/derived infrastructure — No checked Yoneda-n-extension definition/classification was found.
Construction — Right derived functors of inverse limit
For small I and suitable abelian A, defines R^n lim_I on the functor category A^I using injective resolutions.
Formalized. Limits.lim; Functor.rightDerived — For any small diagram category and abelian target satisfying the usual completeness/enough-injectives hypotheses, the pinned limit functor has generic right derived functors, exactly Rⁿ lim.
Searched: P
Definition — Countable towers
For I=…→2→1→0, objects of Ab^I are called countable towers of abelian groups.
Formalized. functor category ℕᵒᵖ ⥤ A; Limits.lim; Functor.rightDerived — A countable inverse tower is the pinned functor-category specialization of U043, so its derived inverse limits are obtained by the same generic construction.
Searched: P
Definition/convention — Grothendieck axiom AB4
AB4* means completeness plus exactness of arbitrary products (equivalently products of surjections are surjective); Ab, modules, and chain complexes satisfy it, while sheaves need not.
Not formalized. partial: generic homological/derived infrastructure — Mathlib defines AB4Star and ModuleCat satisfies it, but the source row also packages finite-abelian-group and sheaf examples/failure; no checked whole bundle was found.
Definition 3.5.1 — Eilenberg lim^1 for a countable tower
Defines Δ:∏A_i→∏A_i by differences along transition maps; ker Δ=lim A_i and lim^1 A_i=coker Δ, with lim^n=0 for n≠0,1 by definition of this model.
Not formalized. partial: generic homological/derived infrastructure — No checked Eilenberg product complex computing lim/lim¹ was found.
Lemma 3.5.2 — lim^n forms a cohomological δ-functor
Snake Lemma applied to products of a short exact sequence of towers gives the natural long exact lim/lim^1 sequence.
Not formalized. partial: generic homological/derived infrastructure — P/H have generic derived functors but no lim¹ δ-functor package or higher-vanishing theorem.
Lemma 3.5.3 — Surjective towers have vanishing lim^1
If every transition A_{i+1}→A_i is onto, then Δ is onto, so lim^1A_i=0; the projections lim A_i→A_j are onto.
Not formalized. partial: generic homological/derived infrastructure — No checked lim¹=0 theorem for surjective towers was found.
Corollary 3.5.4 — Eilenberg lim^1 equals R^1lim
For countable towers of abelian groups, lim1≅R1lim and R^nlim=0 for n≠0,1.
Not formalized. partial: generic homological/derived infrastructure — No checked identification of the Eilenberg cokernel with R¹lim or countable higher derived-limit vanishing was found.
Reusable comparison — AB4 generalization of lim^1
The same proof identifies lim^1 with R^1lim and kills higher derived limits for towers in any AB4* abelian category.
Not formalized. partial: generic homological/derived infrastructure — No checked AB4* derived-limit generalization was found.
Example 3.5.5 — A nonzero lim^1: p-adic completion quotient
For the tower p^iZ⊂Z, lim1{piZ}≅Z_p^/Z, with Z_p^=lim Z/p^iZ.
Not formalized. partial: generic homological/derived infrastructure — No checked p-adic-completion/nonzero-lim¹ example was found.
Definition 3.5.6 — Mittag–Leffler and trivial Mittag–Leffler conditions
Defines stabilization of images in each stage; the trivial condition requires sufficiently far transition maps to be zero.
Not formalized. partial: generic homological/derived infrastructure — Functor.IsMittagLeffler is pinned for stabilization of ranges, but the row additionally defines Weibel’s “trivial Mittag–Leffler” condition; no checked whole definition bundle exists.
Proposition 3.5.7 — Mittag–Leffler implies lim^1=0
A countable tower satisfying Mittag–Leffler has vanishing lim^1.
Not formalized. partial: generic homological/derived infrastructure — No checked theorem Mittag–Leffler ⇒ lim¹=0 was found; the pinned cofiltered-system file lists a related Stacks result as TODO.
Theorem 3.5.8 — Milnor exact sequence for inverse limits of complexes
For a Mittag–Leffler tower of chain complexes C_i with C=lim C_i, 0→lim^1H_{q+1}(C_i)→H_q(C)→lim H_q(C_i)→0.
Not formalized. partial: generic homological/derived infrastructure — No checked Milnor short exact sequence for inverse towers of chain complexes was found.
Variant — Cochain version of the Milnor exact sequence
For a Mittag–Leffler tower of cochain complexes, 0→lim1H{q-1}(C_i)→H^q(lim C_i)→lim H^q(C_i)→0.
Not formalized. partial: generic homological/derived infrastructure — No checked cochain dual Milnor sequence was found.
Application 3.5.9 — Milnor sequence for cohomology of increasing CW subcomplexes
If X=∪X_i is an increasing union of CW subcomplexes, 0→lim1H{q-1}(X_i)→H^q(X)→lim H^q(X_i)→0.
Not formalized. partial: generic homological/derived infrastructure — No checked increasing-union cohomology Milnor sequence was found.
Application 3.5.10 — Milnor sequence for Ext over a union
If A=∪A_i, then 0→lim1Ext_R{q-1}(A_i,B)→Ext_R^q(A,B)→lim Ext_R^q(A_i,B)→0; includes the p-adic completion specialization.
Not formalized. partial: generic homological/derived infrastructure — No checked Ext-of-union Milnor sequence was found.
Application 3.5.11 — Total complexes as inverse limits of truncations
For a double complex C, Tot(C)=lim Tot(T_iC) for brutal vertical truncations, giving the corresponding Milnor short exact sequence on homology.
Not formalized. partial: generic homological/derived infrastructure — No checked comparison of a total complex with inverse limits of truncations and the associated Milnor sequence was found.
Vista 3.5.12 — Roos complex for higher derived limits
For a poset I and AB4* category, builds a cochain complex C^A from products over chains in I; lim_I^n A=Hn(CA), yielding a universal δ-functor and R^nlim when enough injectives exist.
Not formalized. partial: generic homological/derived infrastructure — No checked Roos complex/higher derived-limit computation was found.
Theorem 3.6.1 — Künneth formula
If P is a chain complex of flat right R-modules and every d(P_n) is flat, then 0→H_n(P)⊗M→H_n(P⊗M)→Tor_1^R(H_{n-1}(P),M)→0.
Not formalized. partial: generic homological/derived infrastructure — No checked algebraic Künneth theorem was found in P/H/current/external Lean.
Universal Coefficient Theorem for Homology 3.6.2 — UCT for a free abelian chain complex
For P free over Z, the Künneth sequence splits noncanonically: H_n(P⊗M)≅H_n(P)⊗M⊕Tor_1^Z(H_{n-1}(P),M).
Not formalized. partial: generic homological/derived infrastructure — No checked algebraic universal coefficient short exact sequence for free ℤ-complexes was found. The external sphere-six repository states a topological integral UCT only through a public axiom, so it is not a route.
Theorem 3.6.3 — Künneth formula for tensor products of complexes
For P,Q with P_n and d(P_n) flat, gives the direct-sum H_p(P)⊗H_q(Q) term, Tor_1 correction, and noncanonical splitting over Z with P free.
Not formalized. partial: generic homological/derived infrastructure — No checked Künneth short exact sequence for free chain complexes was found.
Application 3.6.4 — Universal coefficient/Künneth formulas in topology
Defines H_*(X;M) via S(X)⊗M and obtains the split UCT; with Eilenberg–Zilber, obtains the Künneth formula for products of spaces.
Not formalized. partial: generic homological/derived infrastructure — No checked topological Künneth/UCT theorem for singular homology was found.
Universal Coefficient Theorem for Cohomology 3.6.5 — UCT for Hom complexes
If P_n and d(P_n) are projective, 0→Ext_R1(H_{n-1}(P),M)→Hn(Hom_R(P,M))→Hom_R(H_n(P),M)→0 splits noncanonically.
Not formalized. partial: generic homological/derived infrastructure — No checked cohomological UCT short exact sequence for free ℤ-complexes was found.
Application 3.6.6 — Universal coefficient theorem for topological cohomology
Defines H^(X;M)=H^Hom(S(X),M) and specializes the UCT to Hn(X;M)≅Hom(H_n(X),M)⊕Ext_Z1(H_{n-1}(X),M).
Not formalized. partial: generic homological/derived infrastructure — The external sphere-six topological UCT is introduced as an axiom, not a proof; P/H have no replacement.
Example 3.6.7 — H^1(X;Z) is torsionfree for path-connected X
For path-connected X, H^1(X;Z)≅Hom(H_1(X),Z), hence is torsionfree.
Not formalized. partial: generic homological/derived infrastructure — No checked theorem proving H₁(X;ℤ) torsion-free for every space was found.