Chapter 8. Simplicial Methods in Homological Algebra
FC05 — Weibel, An Introduction to Homological Algebra.
This chapter contains 26 definitions, 9 theorems, 5 propositions, 10 lemmas, 5 corollaries, 16 examples, 15 constructions, 3 conventions, 1 criterion and 16 other statements.
Of the 106 statements checked against Lean, 24 are formalized somewhere and 82 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 82 | 77% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 24 | 23% | Mathlib states and proves it. |
| checked in total | 106 |
- Project-first search was performed at repo HEAD
f90173886bc881c2d43c0a7eb2d9fe7f110ac9a5. No project declaration owns a complete C08 source row under strict bundle semantics. - Pinned Mathlib is
P=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0, Apache-2.0 and directly project-compatible. EveryPtarget cited in the chapter table was inspected at that revision. A local P-compiled witness also checked the exact definitional assemblies for semisimplicial objects (U010), degreewise postcomposition (U014), pointwise simplicial products (U019), and bisimplicial objects (U050). - Current Mathlib was refreshed again on 2026-09-06 at
H=5aedf732b6987e8c26ab3c9ebc855314f82b045f. Targeted P→H/current searches found no H-only declaration closing the missing generator/relations equivalence, simplicial-group Kan theorem, higher simplicial homotopy-group package, Eilenberg–Zilber/Alexander–Whitney theorem, comonadic standard resolution, relative Tor/Ext theory, or André–Quillen theory. - Open Mathlib PR searches were refreshed for Dold–Kan, Eilenberg–Zilber, simplicial homotopy, André–Quillen, and cotangent complexes. No Dold–Kan/Eilenberg–Zilber/AQ PR was found. PRs surfaced by the broader simplicial-homotopy search (
[#41735](https://github.com/leanprover-community/mathlib4/pull/41735)homotopy-cartesian squares at05f5b74caccabab60ca495271b65e19b85f8d208,[#42158](https://github.com/leanprover-community/mathlib4/pull/42158)nerve homotopy atb50e98976e1b6298e3b0a6d2df5305abac9f0d34,[#41963](https://github.com/leanprover-community/mathlib4/pull/41963)nerve products atac9800b417b53c33d797559c04d12d8fed0e08f2, and[#37659](https://github.com/leanprover-community/mathlib4/pull/37659)relative singular homology at01b33ef8a476b54c7d1538ff14e245d097577b7d) do not realize any unmatched C08 whole-source bundle, so none is promoted as a reference-port. - Indexed GitHub Lean searches for
AndreQuillen, “André-Quillen”, “relative Tor”, “cotangent complex”,AlexanderWhitney,EilenbergZilber, andcotriplefound no exact missing owner. The only external Eilenberg–Zilber-named candidate inspected wasthe-omega-institute/newmathatE=223bff05b2227f278d34738b20c15a95a5f64e86(MIT),lean4/BEDC/Derived/EilenbergZilberUp.lean; it computes a specialized spectral-sequence page/toy result rather than Weibel’s natural chain comparison, convergence theorem, Alexander–Whitney map, or shuffle homotopy inverse, so it is negative evidence only. - U003 remains unmatched because pinned
SimplexCategory/GeneratorsRelations/NormalForms.leanexplicitly leaves uniqueness of the face normal form as TODO; therefore the bundled unique epi-mono/standard face-degeneracy expression is incomplete, and U004–U005’s equivalences from generators-and-relations data are not available either. - U011/U012/U015 remain unmatched despite
SemiSimplexCategoryand the simplicial alternating-face complex: the pin has no left adjoint freely adjoining degeneracies and no semisimplicial alternating/free-module complex realizing the source’s explicit “simplicial or semisimplicial” bundles. - U017 remains unmatched although
SSet.toTop ⊣ TopCat.toSSetis pinned: the source also asserts the CW-type iff characterization of the realization-singular counit, and no checked declaration proves that clause. U021 remains unmatched because no checked declaration proves every simplicial group is Kan. - U030–U034 are not inferred from the additive normalized Moore complex. Pinned
normalizedMooreComplexuses the opposite endpoint convention to Weibel U032, andDoldKan/Decomposition.leanexplicitly records the degenerate-subcomplex complement as unfinished. U035 is promoted because the pinned chain-homotopy equivalence directly gives the source homology comparison. - U040 remains unmatched: pinned
SSet.Homotopydefines the cylinder map andtoSimplicialObjectHomotopyconverts it to a combinatorial homotopy, but no converse/bijection realizing the source equivalence was found. U041 is not inferred because the pinned chain-homotopy construction targets the alternating-face complex, while the source row specifically asserts the induced chain homotopy on the normalized complex. - U045 remains unmatched because
DoldKan/Equivalence.leanexplicitly lists the dual cosimplicial/cochain Dold–Kan equivalence as TODO. U046–U048 are promoted through the explicit Γ construction, unit/counit comparison isomorphisms, and reflects-isomorphisms instances already present at P. - U049 remains unmatched: extra degeneracy gives pinned contractibility/chain-homotopy consequences, but the source row bundles an asphericity definition and an iff with exactness not supplied by the checked API. U051–U057 remain unmatched because no checked P/H/O/E source supplies the bisimplicial total-complex/diagonal Eilenberg–Zilber spectral sequence or Alexander–Whitney/shuffle chain equivalence.
- U058–U059 are pinned generic category-theory owners, but U060–U080 are not inferred from them: no checked API constructs the canonical simplicial comonad resolution, cotriple projectives, standard/free resolutions, or cotriple derived-functor theory in those rows.
- U081–U095 remain unmatched: no checked source realizes Weibel’s relative Tor/Ext, k-split comparison, relative flatness, or the associated base-change spectral sequences. U096–U097 are pinned through
CommAlgCatand Kähler differentials. U098–U106 remain unmatched:Mathlib/RingTheory/Kaehler/JacobiZariski.leancontains only the low-degree naive cotangent/Kähler exact sequence and explicitly notes stronger Tor input as future work; it is not the all-degree André–Quillen cotangent-complex/Jacobi–Zariski package of the source. Nis dated 2026-09-06 negative evidence after A, P, H, open PR/current searches, indexed GitHub searches, and the external E candidate above. A prerequisite, an equivalent slogan without the source comparison theorem, or one clause of a bundled row is not credited as the route for that row.
Definition — simplicial category Δ; simplicial and cosimplicial objects
Let Δ be the category of finite ordinals [n]={0<1<…<n} and monotone maps. A simplicial object in C is a contravariant functor Δ→C; a cosimplicial object is a covariant functor Δ→C.
Formalized. Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean::SimplexCategory; Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean::CategoryTheory.SimplicialObject, CategoryTheory.CosimplicialObject — Pinned Mathlib models objects [n], monotone maps, and the contravariant/covariant functor definitions exactly.
Searched: P
Example 8.1.1
For any object A of a category C, the constant functor Δ^op→C with value A is the constant simplicial object at A.
Formalized. Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean::CategoryTheory.SimplicialObject.const — Pinned Mathlib has the constant simplicial-object functor with the prescribed value in every degree.
Searched: P
Lemma 8.1.2
Every monotone map [n]→[m] factors uniquely as a surjection followed by an injection; equivalently it has unique expressions in the standard degeneracy and face maps with the prescribed index orders.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: Every monotone map [n]→[m] factors uniquely as a surjection followed by an injection; equivalently it has unique expressions in the standard degeneracy and face maps with the prescribed index orders. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Proposition 8.1.3
A simplicial object is equivalently a sequence A_n with face maps ∂i:A_n→A{n-1} and degeneracy maps σ_i:A_n→A_{n+1} satisfying the standard simplicial identities.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: A simplicial object is equivalently a sequence A_n with face maps ∂i:A_n→A{n-1} and degeneracy maps σ_i:A_n→A_{n+1} satisfying the standard simplicial identities. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Corollary 8.1.4
Dually, a cosimplicial object is equivalently a sequence A^n with coface maps ∂^i and codegeneracy maps σ^i satisfying the dual simplicial identities.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: Dually, a cosimplicial object is equivalently a sequence A^n with coface maps ∂^i and codegeneracy maps σ^i satisfying the dual simplicial identities. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Example 8.1.5
The geometric n-simplex is Δn={(t_0,…,t_n)∈R{n+1}: t_i≥0 and Σ_i t_i=1}, with the standard coface and codegeneracy maps.
Formalized. Mathlib/AlgebraicTopology/TopologicalSimplex.lean::SimplexCategory.toTop₀, SimplexCategory.toTop — The pinned cosimplicial topological simplex uses the standard real simplex and the functorial coface/codegeneracy maps.
Searched: P
Construction — Geometric Realization 8.1.6
The geometric realization |X| of a simplicial set X is the quotient of ⨿_n X_n×Δ^n by the face/degeneracy identifications induced from the simplicial structure.
Formalized. Mathlib/AlgebraicTopology/SingularSet.lean::SSet.toTop; SSet.toTopSimplex — Pinned Mathlib defines geometric realization as the left Kan extension of the standard topological simplex along Yoneda. This is the categorical coend/quotient realization implementing the source face/degeneracy identifications.
Searched: P
Example 8.1.7
For a group G, the simplicial set BG has BG_n=G^n with the standard bar faces and degeneracies; its realization is the classifying space BG from group topology.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For a group G, the simplicial set BG has BG_n=G^n with the standard bar faces and degeneracies; its realization is the classifying space BG from group topology. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Example 8.1.8
An ordered simplicial complex K determines a simplicial set SS(K): SS_n(K) consists of nondecreasing (n+1)-tuples of vertices whose underlying set is a simplex of K, with simplicial operators induced by maps in Δ.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: An ordered simplicial complex K determines a simplicial set SS(K): SS_n(K) consists of nondecreasing (n+1)-tuples of vertices whose underlying set is a simplex of K, with simplicial operators induced by maps in Δ. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Definition 8.1.9
Let Δ_s be the subcategory of Δ with the same objects and only injective morphisms. A semisimplicial object in C is a contravariant functor Δ_s→C.
Formalized. Mathlib/AlgebraicTopology/SimplexCategory/SemiSimplexCategory.lean::SemiSimplexCategory, toSimplexCategory; pinned assembly SemiSimplexCategoryᵒᵖ ⥤ C — Pinned Mathlib defines the same objects with order-embedding/injective morphisms. A local P-compiled audit witness typechecked the source semisimplicial-object definition as SemiSimplexCategoryᵒᵖ ⥤ C.
Searched: P
Construction — left adjoint from semisimplicial to simplicial objects
If C has finite coproducts, the forgetful functor from simplicial to semisimplicial objects has a left adjoint L; (LK)_n is the coproduct of K_p over all surjections [n]↠[p].
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: If C has finite coproducts, the forgetful functor from simplicial to semisimplicial objects has a left adjoint L; (LK)_n is the coproduct of K_p over all surjections [n]↠[p]. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Definition 8.2.1
For a simplicial or semisimplicial object A in an abelian category, the associated unnormalized chain complex has C_n(A)=A_n and differential d=Σ_i(-1)^i∂_i.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For a simplicial or semisimplicial object A in an abelian category, the associated unnormalized chain complex has C_n(A)=A_n and differential d=Σ_i(-1)^i∂_i. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Example 8.2.2
A central sequence x_1,…,x_m in a ring R determines a semisimplicial module built from the exterior powers Λ{n+1}Rm; its associated chain complex is the Koszul complex K(x).
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: A central sequence x_1,…,x_m in a ring R determines a semisimplicial module built from the exterior powers Λ{n+1}Rm; its associated chain complex is the Koszul complex K(x). Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Convention/construction — apply functors degreewise to (co/semi)simplicial objects
Any functor F:A→B applies degreewise to simplicial objects, producing a simplicial object F(A) in B; the same construction applies to semisimplicial and cosimplicial objects.
Formalized. Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean::SimplicialObject.whiskering; generic Functor.comp for cosimplicial/semisimplicial objects — Functor postcomposition gives the source degreewise construction in all three variances. A local P-compiled audit witness typechecked all three cases.
Searched: P
Example 8.2.3
For a ring R and a (semi)simplicial set X, applying the free R-module functor degreewise gives a (semi)simplicial R-module R[X]; its associated chain complex is the simplicial chain complex used to define homology.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For a ring R and a (semi)simplicial set X, applying the free R-module functor degreewise gives a (semi)simplicial R-module R[X]; its associated chain complex is the simplicial chain complex used to define homology. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Example 8.2.4
For a space X, the singular simplicial set has n-simplices Hom_Top(Δ^n,X). Its associated simplicial chain complex is the usual singular chain complex of X.
Formalized. Mathlib/AlgebraicTopology/SingularSet.lean::TopCat.toSSet; Mathlib/AlgebraicTopology/SingularHomology/Basic.lean::AlgebraicTopology.singularChainComplexFunctor — Pinned Mathlib identifies n-simplices with continuous maps from the standard n-simplex and builds the usual singular chain complex from that simplicial set.
Searched: P
Comparison/adjunction — geometric realization versus singular simplicial set
Remark There is a natural continuous map | S ( X ) | X , which is a homotopy equivalence if (and only if) X has the homotopy type of a CW complex. It is induced from the maps S_n ( X ) × Δ^n → X sending ( f , t ) to f ( t )
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: Remark There is a natural continuous map Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Example 8.2.5
The representable simplicial set Δ[n]=Hom_Δ(-,[n]) satisfies Yoneda: simplicial maps Δ[n]→A are naturally in bijection with n-simplices A_n.
Formalized. Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean::SSet.stdSimplex; SSet.yonedaEquiv — Pinned Mathlib has Δ[n]=Hom_Δ(-,[n]) and the natural bijection (Δ[n] ⟶ X) ≃ X_n.
Searched: P
Construction — Cartesian Products 8.2.6
The product of simplicial objects is degreewise: (A×B)_n=A_n×B_n, with faces and degeneracies acting diagonally.
Formalized. generic functor-category binary product CategoryTheory.Limits.prod; pinned assembly (X ⨯ Y : SimplicialObject C) — A local P-compiled audit witness verified definitionally that the product object evaluates to X.obj n ⨯ Y.obj n; functorial maps therefore act diagonally.
Searched: P
Definition — Fibrant Simplicial Sets 8..7 [OCR-damaged label]
A simplicial set X is fibrant (a Kan complex) if every compatible family of n-faces x_i∈X_n for i≠k, satisfying ∂i x_j=∂{j-1}x_i for i<j with i,j≠k, is filled by some y∈X_{n+1} with ∂_i y=x_i for all i≠k.
Formalized. Mathlib/AlgebraicTopology/SimplicialSet/KanComplex.lean::SSet.KanComplex; KanComplex.iff; horn.IsCompatible.exists_lift_of_kanComplex — Pinned Mathlib gives the compatible-face horn-filling condition and proves it equivalent to fibrancy.
Searched: P
Lemma 8.2.8
Every simplicial group is fibrant as a simplicial set; consequently every simplicial abelian group and every simplicial R-module is fibrant.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: Every simplicial group is fibrant as a simplicial set; consequently every simplicial abelian group and every simplicial R-module is fibrant. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Definition — Fibrations 8.2.9
A simplicial map π:E→B is a Kan fibration if, whenever compatible faces x_i∈E_n are prescribed for i≠k and y∈B_{n+1} satisfies π(x_i)=∂i y, there is x∈E{n+1} with ∂_i x=x_i for i≠k and π(x)=y. A simplicial set X is fibrant exactly when X→* is a fibration.
Formalized. Mathlib/AlgebraicTopology/SimplicialSet/CategoryWithFibrations.lean::SSet.modelCategoryQuillen.fibrations_eq, SSet.modelCategoryQuillen.fibration_iff, SSet.horn.IsCompatible.exists_lift; Mathlib/AlgebraicTopology/SimplicialSet/KanComplex.lean::SSet.KanComplex — Pinned Mathlib defines fibrations by right lifting against horn inclusions, derives the compatible-face lift over a base simplex, and defines a Kan complex as a fibrant object, i.e. the map to the terminal object is a fibration.
Searched: P
Convention/construction — Front-to-Back Duality 8.2.10
The involution of Δ fixing [n] and sending each face ∂i to ∂{n-i} and each degeneracy σ_i to σ_{n-i} gives the front-to-back dual of every simplicial construction.
Formalized. Mathlib/AlgebraicTopology/SimplexCategory/Rev.lean::SimplexCategory.rev; Mathlib/AlgebraicTopology/SimplicialObject/Op.lean::CategoryTheory.SimplicialObject.opFunctor, CategoryTheory.SimplicialObject.opFunctor_obj_δ, CategoryTheory.SimplicialObject.opFunctor_obj_σ, CategoryTheory.SimplicialObject.opEquivalence — Pinned Mathlib fixes [n], reverses face/degeneracy indices, and induces the involutive equivalence on simplicial objects.
Searched: P
Definition/construction — based fibrant simplicial sets: Zn and the homotopy relation
For a based fibrant simplicial set X, write =σ_0^n()∈X_n and Z_n={x∈X_n:∂i x=* for all i}. For x,x′∈Z_n, define x∼x′ when some y∈X{n+1} has ∂_i y=* for i<n, ∂n y=x, and ∂{n+1}y=x′.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For a based fibrant simplicial set X, write =σ_0^n()∈X_n and Z_n={x∈X_n:∂i x= for all i}. For x,x′∈Z_n, define x∼x′ when some y∈X*{n+1} has ∂_i y=* for i<n, ∂n y=x, and ∂{n+1}y=x′. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Lemma/Definition 8.3.1
For a fibrant simplicial set X with basepoint, the homotopy relation on n-cycles Z_n is an equivalence relation; define π_n(X)=Z_n/∼.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For a fibrant simplicial set X with basepoint, the homotopy relation on n-cycles Z_n is an equivalence relation; define π_n(X)=Z_n/∼. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Comparison — simplicial homotopy groups versus topological realization
Remark If X is a fibrant simplicial set, π_n ( X ) agrees with the topological homotopy group π_n ( | X | ) ; see [May,16.1]. Since π_n ( | X | ) ≅ π_n ( | S ( X ) | ) , one usually defines π_n ( X ) as π_n S ( X ) when X is not fibrant. Thus π_1 ( X ) is a group, and π_n ( X ) is an abelian group for n ≥ 2
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: Remark If X is a fibrant simplicial set, π_n ( X ) agrees with the topological homotopy group π_n ( Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Example 8.3.2
For a fibrant simplicial set X, π_0(X) is X_0 modulo the equivalence relation generated by declaring the two endpoints ∂_0y and ∂_1y of every 1-simplex y equivalent.
Formalized. Mathlib/AlgebraicTopology/SimplicialSet/PiZero.lean::SSet.π₀Rel, SSet.π₀, SSet.π₀.mk_eq_mk_iff — Pinned Mathlib defines the edge relation on vertices, takes its equivalence closure by Quot, and characterizes equality of component classes by the generated equivalence relation.
Searched: P
Example 8.3.3
For the simplicial classifying space BG, the simplicial homotopy groups satisfy π_1(BG)≅G and π_n(BG)=0 for n≠1; the same holds for the geometric realization.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For the simplicial classifying space BG, the simplicial homotopy groups satisfy π_1(BG)≅G and π_n(BG)=0 for n≠1; the same holds for the geometric realization. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Definition 8.3.4
An Eilenberg–Mac Lane space K(G,n) is a fibrant simplicial set with π_n≅G and π_i=0 for i≠n; for n≥2 the group G is necessarily abelian. The simplicial classifying space BG is a K(G,1).
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: An Eilenberg–Mac Lane space K(G,n) is a fibrant simplicial set with π_n≅G and π_i=0 for i≠n; for n≥2 the group G is necessarily abelian. The simplicial classifying space BG is a K(G,1). Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Construction — normalized complex of a simplicial group/module
For a simplicial group G, define the normalized Moore subgroup N_nG=⋂_{i<n}ker(∂_i); with differential induced by the remaining face, these form the normalized Moore complex.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For a simplicial group G, define the normalized Moore subgroup N_nG=⋂_{i<n}ker(∂_i); with differential induced by the remaining face, these form the normalized Moore complex. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Comparison/remark — Remark 8.3.5
For a fibration π:E→B of fibrant simplicial sets with fiber F over the chosen basepoint, F is fibrant and there are connecting maps ∂:π_n(B)→π_{n-1}(F) fitting into the natural long exact homotopy sequence …→π_n(F)→π_n(E)→π_n(B)→π_{n-1}(F)→….
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For a fibration π:E→B of fibrant simplicial sets with fiber F over the chosen basepoint, F is fibrant and there are connecting maps ∂:π_n(B)→π_{n-1}(F) fitting into the natural long exact homotopy sequence …→π_n(F)→π_n(E)→π_n(B)→π_{n-1}(F)→…. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Definition 8.3.6
For a simplicial object A in an abelian category, define the normalized (Moore) complex by N_n(A)=⋂_{i=0}^{n-1}ker(∂i:A_n→A{n-1}) with differential d=(-1)^n∂_n, and define π_n(A)=H_n(N(A)).
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For a simplicial object A in an abelian category, define the normalized (Moore) complex by N_n(A)=⋂_{i=0}^{n-1}ker(∂i:A_n→A{n-1}) with differential d=(-1)^n∂_n, and define π_n(A)=H_n(N(A)). Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Definition — degenerate subcomplex D(A)
The degenerate subcomplex D(A)⊂C(A) is generated degreewise by degeneracies: D_n(A)=Σ_i σ_i(C_{n-1}(A)).
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: The degenerate subcomplex D(A)⊂C(A) is generated degreewise by degeneracies: D_n(A)=Σ_i σ_i(C_{n-1}(A)). Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Lemma 8.3.7
For every simplicial object A in an abelian category, C(A)=N(A)⊕D(A); hence N(A)≅C(A)/D(A).
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For every simplicial object A in an abelian category, C(A)=N(A)⊕D(A); hence N(A)≅C(A)/D(A). Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Theorem 8.3.8
For every simplicial object A in an abelian category, π_(A)=H_(N(A)) is naturally isomorphic to the homology H_*(C(A)) of the unnormalized chain complex.
Formalized. Mathlib/AlgebraicTopology/DoldKan/HomotopyEquivalence.lean::AlgebraicTopology.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex — Pinned Mathlib proves a chain-homotopy equivalence between the normalized Moore and alternating-face complexes, which in particular gives the source homology isomorphism.
Searched: P
Application 8.3.9
For a fibrant simplicial set X, the inclusion of simplices X→Z[X] induces the Hurewicz homomorphism π_(X)→π_(Z[X])≅H_*(X;Z), agreeing after realization with the usual topological Hurewicz map.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For a fibrant simplicial set X, the inclusion of simplices X→Z[X] induces the Hurewicz homomorphism π_(X)→π_(Z[X])≅H_*(X;Z), agreeing after realization with the usual topological Hurewicz map. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Proposition 8.3.1o [OCR-damaged label]
For a simplicial abelian group A, the Hurewicz map π_(A) → H_(A; Z)=H_*(|A|; Z) is a split monomorphism; the extraction prints 8.3.1o
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For a simplicial abelian group A, the Hurewicz map π_(A) → H_(A; Z)=H_*( Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Comparison — simplicial abelian groups split homotopically into Eilenberg-MacLane factors
Every simplicial abelian group has the homotopy type of a product of Eilenberg–Mac Lane spaces K(π_nA,n).
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: Every simplicial abelian group has the homotopy type of a product of Eilenberg–Mac Lane spaces K(π_nA,n). Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Definition 8.3.11
Two simplicial maps f,g:A→B are simplicially homotopic when there are maps h_i:A_n→B_{n+1} satisfying the standard face/degeneracy homotopy identities, with endpoints f and g.
Formalized. Mathlib/AlgebraicTopology/SimplicialObject/Homotopy.lean::CategoryTheory.SimplicialObject.Homotopy — The pinned structure consists of the source family h_i:A_n→B_{n+1} together with exactly the simplicial face/degeneracy identities.
Searched: P
Theorem 8.3.12
For simplicial objects A,B in an abelian category or in Sets, simplicial homotopies f≃g are in bijection with simplicial maps h:A×Δ[1]→B whose restrictions along the two endpoint inclusions are f and g.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For simplicial objects A,B in an abelian category or in Sets, simplicial homotopies f≃g are in bijection with simplicial maps h:A×Δ[1]→B whose restrictions along the two endpoint inclusions are f and g. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Lemma 8.3.13
If f,g:A→B are simplicially homotopic maps of simplicial objects in an abelian category, then N(f),N(g):N(A)→N(B) are chain homotopic.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: If f,g:A→B are simplicially homotopic maps of simplicial objects in an abelian category, then N(f),N(g):N(A)→N(B) are chain homotopic. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Construction — Path Spaces 8.3.14
The path-space functor P:Δ→Δ sends [n] to [n+1] by adjoining a new initial element. For a simplicial object A, (PA)n=A{n+1}, with faces and degeneracies shifted by one, and ∂_0:PA→A is simplicial.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: The path-space functor P:Δ→Δ sends [n] to [n+1] by adjoining a new initial element. For a simplicial object A, (PA)n=A{n+1}, with faces and degeneracies shifted by one, and ∂_0:PA→A is simplicial. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Theorem — Dold-Kan Theorem 8.4.1
Dold–Kan: for any abelian category A, the normalized chain complex functor N gives an equivalence between simplicial objects in A and nonnegatively graded chain complexes in A.
Formalized. Mathlib/AlgebraicTopology/DoldKan/Equivalence.lean::CategoryTheory.Abelian.DoldKan.equivalence — Pinned Mathlib proves SimplicialObject A ≌ ChainComplex A ℕ for every abelian category, with normalized Moore complex as the forward functor.
Searched: P
Corollary 8.4.2
For an abelian category A, the functors π_n on simplicial objects form the universal homological δ-functor extending π_0; equivalently they are the left derived functors of π_0.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For an abelian category A, the functors π_n on simplicial objects form the universal homological δ-functor extending π_0; equivalently they are the left derived functors of π_0. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Definition — Corollary/Definition 8.4.3
Dual Dold–Kan: cosimplicial objects in an abelian category are equivalent, via normalized cochains, to nonnegatively graded cochain complexes.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: Dual Dold–Kan: cosimplicial objects in an abelian category are equivalent, via normalized cochains, to nonnegatively graded cochain complexes. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Construction 8.4.4
An explicit inverse K to the normalized-chain functor is constructed by K(C)n=⊕{[n]↠[p]} C_p, with faces and degeneracies induced by factorization in Δ.
Formalized. Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean::AlgebraicTopology.DoldKan.Γ₀, AlgebraicTopology.DoldKan.Γ₀.obj₂, AlgebraicTopology.DoldKan.Γ₀.splitting — Pinned Mathlib constructs Γ degreewise as a finite coproduct indexed by epimorphisms in the simplex category and defines all simplicial operators from epi-mono factorization, matching the source explicit inverse.
Searched: P
Construction — natural comparison K N(A) → A in the Dold-Kan inverse construction
For the explicit Dold–Kan inverse K, N(K(C))≅C; the comparison K(N(A))→A is obtained by sending each summand indexed by a surjection to the corresponding degeneracy of normalized chains.
Formalized. Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean::AlgebraicTopology.DoldKan.N₁Γ₀; Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean::AlgebraicTopology.DoldKan.Γ₂N₁, AlgebraicTopology.DoldKan.Γ₂N₂; Mathlib/AlgebraicTopology/DoldKan/Equivalence.lean::CategoryTheory.Abelian.DoldKan.equivalence — Pinned Mathlib constructs the natural unit/counit comparison isomorphisms proving NΓ≅id and ΓN≅id, hence the source comparison maps are isomorphisms.
Searched: P
Lemma 8.4.5
If a simplicial morphism f:B→A induces an isomorphism N(f):N(B)→N(A) of normalized chain complexes, then f is an isomorphism.
Formalized. Mathlib/AlgebraicTopology/DoldKan/NReflectsIso.lean::AlgebraicTopology.DoldKan.instReflectsIsomorphismsN₁, AlgebraicTopology.DoldKan.instReflectsIsomorphismsN₂ — Pinned Mathlib proves the normalization functors reflect isomorphisms, directly realizing the source criterion.
Searched: P
Definition — Augmented Objects 8.4.6
An augmented simplicial object A_→A_{-1} is aspherical when π_n(A_)=0 for n≠0 and the augmentation induces π_0(A_*)≅A_{-1}. In an abelian category this is equivalent to exactness of the augmented normalized/unnormalized complexes. Right and left contractibility are the extra-degeneracy conditions of 8.4.6 and imply asphericity.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: An augmented simplicial object A_→A_{-1} is aspherical when π_n(A_)=0 for n≠0 and the augmentation induces π_0(A_*)≅A_{-1}. In an abelian category this is equivalent to exactness of the augmented normalized/unnormalized complexes. Right and left contractibility are the extra-degeneracy conditions of 8.4.6 and imply asphericity. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Definition — bisimplicial object
A bisimplicial object is a contravariant functor Δ×Δ→C, equivalently a bigraded family A_{pq} with commuting horizontal and vertical simplicial structures.
Formalized. pinned assembly (SimplexCategory × SimplexCategory)ᵒᵖ ⥤ C — The source row is the functor definition itself. A local P-compiled audit witness typechecked the bisimplicial-object type directly from the pinned simplex category and functor category.
Searched: P
Construction — associated first-quadrant double complex C(A)
A bisimplicial object in an abelian category has an associated first-quadrant double complex with horizontal and vertical differentials given by the alternating sums of the corresponding face maps, with the standard sign convention.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: A bisimplicial object in an abelian category has an associated first-quadrant double complex with horizontal and vertical differentials given by the alternating sums of the corresponding face maps, with the standard sign convention. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Construction — diagonal simplicial object diag(A)
The diagonal simplicial object of a bisimplicial object A is diag(A)n=A{nn}, with faces ∂_i^h∂_i^v and degeneracies σ_ihσ_iv.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: The diagonal simplicial object of a bisimplicial object A is diag(A)n=A{nn}, with faces ∂_i^h∂_i^v and degeneracies σ_ihσ_iv. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Theorem — Eilenberg-Zilber Theorem 8.5.1
For a bisimplicial object A in an abelian category there is a natural isomorphism π_diag(A)≅H_Tot(CA). Moreover E1_{pq}=π_qv(A_{p*}) and E2_{pq}=π_phπ_q^v(A) form a convergent first-quadrant spectral sequence abutting to π_{p+q}diag(A).
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For a bisimplicial object A in an abelian category there is a natural isomorphism π_diag(A)≅H_Tot(CA). Moreover E1_{pq}=π_qv(A_{p*}) and E2_{pq}=π_phπ_q^v(A) form a convergent first-quadrant spectral sequence abutting to π_{p+q}diag(A). Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Lemma 8.5.2
For bisimplicial objects in an abelian category, both diag and Tot∘C preserve projective objects.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For bisimplicial objects in an abelian category, both diag and Tot∘C preserve projective objects. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Application 8.5.3
For a simplicial right R-module A and simplicial left R-module B, A⊗_R B is bisimplicial and C(A⊗_R B) has total complex Tot(C(A)⊗_R C(B)); Eilenberg–Zilber therefore gives the standard Künneth comparison for their product.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For a simplicial right R-module A and simplicial left R-module B, A⊗_R B is bisimplicial and C(A⊗_R B) has total complex Tot(C(A)⊗_R C(B)); Eilenberg–Zilber therefore gives the standard Künneth comparison for their product. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Construction/comparison — The Alexander-Whitney Map 8.5.4
The Alexander–Whitney maps f_{pq}:A_{nn}→A_{pq} for p+q=n assemble to a chain map C(diag A)→Tot(CA) inducing the Eilenberg–Zilber isomorphism; the shuffle map is a chain-homotopy inverse.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: The Alexander–Whitney maps f_{pq}:A_{nn}→A_{pq} for p+q=n assemble to a chain map C(diag A)→Tot(CA) inducing the Eilenberg–Zilber isomorphism; the shuffle map is a chain-homotopy inverse. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Comparison/counterexample — degeneracies are necessary for Eilenberg-Zilber
The Eilenberg-Zilber theorem fails for semisimplicial bisimplicial objects in general; the degeneracy operators are essential
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: The Eilenberg-Zilber theorem fails for semisimplicial bisimplicial objects in general; the degeneracy operators are essential Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Definition 8.6.1
A triple (monad) on a category C is an endofunctor T with unit η:id→T and multiplication μ:T^2→T satisfying associativity and unit laws; a cotriple (comonad) is the dual structure.
Formalized. Mathlib/CategoryTheory/Monad/Basic.lean::CategoryTheory.Monad, CategoryTheory.Comonad — Pinned Mathlib packages endofunctor, unit/counit, multiplication/comultiplication and the source unit/associativity laws.
Searched: P
Construction — Main Application 8.6.2
An adjunction F⊣U produces a monad UF on the source category and a comonad FU on the target, with unit/counit and multiplication/comultiplication induced by the adjunction.
Formalized. Mathlib/CategoryTheory/Monad/Adjunction.lean::CategoryTheory.Adjunction.toMonad, CategoryTheory.Adjunction.toComonad — Pinned Mathlib constructs the induced monad and comonad from any adjunction exactly as in the source.
Searched: P
Example 8.6.3
For G-modules, the adjunction ZG⊗_Z- ⊣ forgetful gives the standard free-module cotriple used to construct canonical group-homology resolutions.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For G-modules, the adjunction ZG⊗_Z- ⊣ forgetful gives the standard free-module cotriple used to construct canonical group-homology resolutions. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Construction — Simplicial Object of a Cotriple 8.6.4
For a cotriple ⊥ with counit ε and comultiplication δ, define ⊥_nA=⊥^{n+1}A, with faces ∂i=⊥^i ε ⊥^{n-i} and degeneracies σ_i=⊥^i δ ⊥^{n-i}. These maps form the canonical augmented simplicial object ⊥*A→A.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For a cotriple ⊥ with counit ε and comultiplication δ, define ⊥_nA=⊥^{n+1}A, with faces ∂*i=⊥^i ε ⊥^{n-i} and degeneracies σ_i=⊥^i δ ⊥^{n-i}. These maps form the canonical augmented simplicial object ⊥**A→A. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Definition 8.6.5
For a cotriple ⊥ with counit ε, an object P is ⊥-projective when ε_P:⊥P→P admits a section. Objects in the image of the left adjoint producing ⊥ are ⊥-projective.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For a cotriple ⊥ with counit ε, an object P is ⊥-projective when ε_P:⊥P→P admits a section. Objects in the image of the left adjoint producing ⊥ are ⊥-projective. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Example/comparison — Paradigm 8.6.6
For the free-module adjunction R-mod↔︎Sets, the cotriple FU is the free-module cotriple. An R-module is FU-projective exactly when it is projective in the ordinary module-theoretic sense.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For the free-module adjunction R-mod↔︎Sets, the cotriple FU is the free-module cotriple. An R-module is FU-projective exactly when it is projective in the ordinary module-theoretic sense. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Criterion — ⊥-Projective Lifting Property 8.6.7
For a cotriple FU from an adjunction F⊣U, P is ⊥-projective iff maps P→A_2 lift across every morphism A_1→A_2 whose image under U is a split epimorphism.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For a cotriple FU from an adjunction F⊣U, P is ⊥-projective iff maps P→A_2 lift across every morphism A_1→A_2 whose image under U is a split epimorphism. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Proposition 8.6.8
The canonical augmented simplicial object ⊥_*A→A associated to a cotriple is aspherical for every ⊥-projective A; in an abelian category its associated augmented chain complex is exact.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: The canonical augmented simplicial object ⊥_*A→A associated to a cotriple is aspherical for every ⊥-projective A; in an abelian category its associated augmented chain complex is exact. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Corollary 8.6.9
If U:A→C has a left adjoint F and A is abelian, then for every C∈C the augmented simplicial object ⊥_*(FC)→FC is contractible, hence aspherical.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: If U:A→C has a left adjoint F and A is abelian, then for every C∈C the augmented simplicial object ⊥_*(FC)→FC is contractible, hence aspherical. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Proposition 8.6.10
If U:A→C has a left adjoint F, then for every A∈A the augmented simplicial object U(⊥_*A)→U(A) is left contractible in C, hence aspherical.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: If U:A→C has a left adjoint F, then for every A∈A the augmented simplicial object U(⊥_*A)→U(A) is left contractible in C, hence aspherical. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Application — Group Homology 8.6.11
For G-modules, the canonical simplicial resolution from the free-forgetful cotriple is aspherical and built from induced/free G-modules; applying coinvariants computes ordinary group homology.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For G-modules, the canonical simplicial resolution from the free-forgetful cotriple is aspherical and built from induced/free G-modules; applying coinvariants computes ordinary group homology. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Construction — The Bar Resolution 8.6.12
For a ring map k→R, the adjunction R⊗_k- ⊣ forgetful gives the bar cotriple on R-modules and its canonical simplicial resolution is the relative bar resolution.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For a ring map k→R, the adjunction R⊗_k- ⊣ forgetful gives the bar cotriple on R-modules and its canonical simplicial resolution is the relative bar resolution. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Proposition 8.6.13
For k commutative, tensoring the relative bar resolutions of modules over k-algebras R and R′ is chain-homotopy equivalent to the bar resolution over R⊗_kR′ of the tensor-product module.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For k commutative, tensoring the relative bar resolutions of modules over k-algebras R and R′ is chain-homotopy equivalent to the bar resolution over R⊗_kR′ of the tensor-product module. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Comparison — bar-resolution Eilenberg-Zilber homotopy equivalence
The Eilenberg-Zilber/shuffle map Tot β(R,R)⊗β(R′,R′)→β(R⊗R′,R⊗R′) is a chain-homotopy equivalence; tensoring it with coefficients yields Proposition 8.6.13
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: The Eilenberg-Zilber/shuffle map Tot β(R,R)⊗β(R′,R′)→β(R⊗R′,R⊗R′) is a chain-homotopy equivalence; tensoring it with coefficients yields Proposition 8.6.13 Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Construction — Free Resolutions 8.6.14
The free-module/forgetful adjunction R-mod↔︎Sets yields a cotriple whose canonical augmented simplicial module is aspherical; its associated chain complex is a functorial free resolution.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: The free-module/forgetful adjunction R-mod↔︎Sets yields a cotriple whose canonical augmented simplicial module is aspherical; its associated chain complex is a functorial free resolution. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Construction — Sheaf Cohomology 8.6.15
For sheaves of abelian groups on X, T(F)=∏{x∈X}x*(F_x) is the triple arising from the stalk/skyscraper adjunction. Its canonical cosimplicial resolution is the Godement resolution and consists of Γ-acyclic sheaves, so it computes sheaf cohomology.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For sheaves of abelian groups on X, T(F)=∏*{x∈X}x**(F_x) is the triple arising from the stalk/skyscraper adjunction. Its canonical cosimplicial resolution is the Godement resolution and consists of Γ-acyclic sheaves, so it computes sheaf cohomology. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Example 8.6.16
For commutative k-algebras, a simplicial resolution is an augmented simplicial commutative algebra whose underlying simplicial set is aspherical. The free commutative-algebra adjunction supplies canonical such resolutions.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For commutative k-algebras, a simplicial resolution is an augmented simplicial commutative algebra whose underlying simplicial set is aspherical. The free commutative-algebra adjunction supplies canonical such resolutions. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Definition 8.7.1
For a cotriple ⊥ and coefficient functor E to an abelian category, cotriple homology is H_n(A;E)=π_n E(⊥_*A), equivalently homology of the associated normalized/unnormalized chain complex.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For a cotriple ⊥ and coefficient functor E to an abelian category, cotriple homology is H_n(A;E)=π_n E(⊥_*A), equivalently homology of the associated normalized/unnormalized chain complex. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Definition — triple cohomology
Dually, a triple T and covariant coefficient functor E define triple cohomology Hn(C;E)=πn E(T^{*+1}C), computed by the associated cochain complex.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: Dually, a triple T and covariant coefficient functor E define triple cohomology Hn(C;E)=πn E(T^{*+1}C), computed by the associated cochain complex. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Definition — cotriple cohomology for contravariant coefficients
For a contravariant coefficient functor E on a category with cotriple ⊥, E(⊥_*A) is cosimplicial and its cohomotopy groups define cotriple cohomology H^n(A;E).
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For a contravariant coefficient functor E on a category with cotriple ⊥, E(⊥_*A) is cosimplicial and its cohomotopy groups define cotriple cohomology H^n(A;E). Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Example 8.7.2
For the free-module cotriple, applying -⊗_RN to the canonical free resolution computes Tor, while applying Hom_R(-,N) computes Ext; thus ordinary derived functors are instances of cotriple (co)homology.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For the free-module cotriple, applying -⊗_RN to the canonical free resolution computes Tor, while applying Hom_R(-,N) computes Ext; thus ordinary derived functors are instances of cotriple (co)homology. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Definition 8.7.3
A theory of ⊥-left derived functors assigns functors L_nE, augmentation in degree zero, and connecting morphisms for ⊥-exact sequences, satisfying the Barr–Beck axioms.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: A theory of ⊥-left derived functors assigns functors L_nE, augmentation in degree zero, and connecting morphisms for ⊥-exact sequences, satisfying the Barr–Beck axioms. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Theorem — Uniqueness Theorem 8.7.4
Cotriple homology H_*(-;E) is a theory of ⊥-left derived functors, and any other such theory is uniquely naturally isomorphic to it compatibly with the degree-zero augmentation and connecting maps.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: Cotriple homology H_*(-;E) is a theory of ⊥-left derived functors, and any other such theory is uniquely naturally isomorphic to it compatibly with the degree-zero augmentation and connecting maps. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Definition 8.7.5
For k→R, relative Tor is cotriple homology for the base-change cotriple: Tor_p^R/k(M,N)=π_p((⊥_M)⊗R N), equivalently the homology of the displayed two-sided bar complex. Relative Ext is the corresponding cotriple cohomology Ext_R/kp(M,N)=πp Hom_R(⊥**M,N)
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For k→R, relative Tor is cotriple homology for the base-change cotriple: Tor_p^R/k(M,N)=π_p((⊥_M)⊗R N), equivalently the homology of the displayed two-sided bar complex. Relative Ext is the corresponding cotriple cohomology Ext_R/kp(M,N)=πp Hom_R(⊥**M,N) Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Example 8.7.6
If R=k/I, then the relative cotriple satisfies ⊥M≅M; consequently relative Tor and Ext over R/k vanish in positive degrees and degree zero is the ordinary tensor/Hom group.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: If R=k/I, then the relative cotriple satisfies ⊥M≅M; consequently relative Tor and Ext over R/k vanish in positive degrees and degree zero is the ordinary tensor/Hom group. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Definition 8.7.7
A chain complex P_* of R-modules is k-split when its underlying complex of k-modules is split exact; an augmented resolution P_*→M is k-split when its augmented underlying k-complex is split exact.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: A chain complex P_* of R-modules is k-split when its underlying complex of k-modules is split exact; an augmented resolution P_*→M is k-split when its augmented underlying k-complex is split exact. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Lemma 8.7.8
A k-split short exact sequence of R-modules induces natural long exact sequences for relative Tor and relative Ext over R/k.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: A k-split short exact sequence of R-modules induces natural long exact sequences for relative Tor and relative Ext over R/k. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Definition — k-split cotriple-projective resolution
A k-split ⊥-projective resolution P_*→M is a resolution by ⊥-projective modules whose augmented chain complex is split exact over k.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: A k-split ⊥-projective resolution P_*→M is a resolution by ⊥-projective modules whose augmented chain complex is split exact over k. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Theorem — Comparison Theorem 8.7.9
Let P_→M be a k-split ⊥-projective resolution and Q_→N a k-split resolution. Every R-linear map M→N lifts to a chain map P_→Q_, and any two lifts are chain homotopic.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: Let P_→M be a k-split ⊥-projective resolution and Q_→N a k-split resolution. Every R-linear map M→N lifts to a chain map P_→Q_, and any two lifts are chain homotopic. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Theorem 8.7.10
For any k-split ⊥-projective resolution P_→M, relative groups are computed by it: Tor_{R/k}(M,N)≅H_(P_⊗R N) and Ext{R/k}(M,N)≅H^Hom_R(P_*,N).
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For any k-split ⊥-projective resolution P_→M, relative groups are computed by it: Tor_{R/k}(M,N)≅H_(P_⊗R N) and Ext{R/k}(M,N)≅H^Hom_R(P_*,N). Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Lemma 8.7.11
For k-algebras R_1,R_2, let ⊥_i=R_i⊗k- and ⊥{12}=(R_1⊗_kR_2)⊗_k-. If P_i is ⊥_i-projective for i=1,2, then P_1⊗kP_2 is ⊥{12}-projective.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For k-algebras R_1,R_2, let ⊥_i=R_i⊗k- and ⊥{12}=(R_1⊗_kR_2)⊗_k-. If P_i is ⊥_i-projective for i=1,2, then P_1⊗kP_2 is ⊥{12}-projective. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Application 8.7.12
Tensoring k-split relative projective resolutions yields the external product Tor_p{R_1/k}(M_1,N_1)⊗Tor_q{R_2/k}(M_2,N_2)→Tor_{p+q}^{(R_1⊗R_2)/k}(M_1⊗M_2,N_1⊗N_2), with the analogous external product for relative Ext.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: Tensoring k-split relative projective resolutions yields the external product Tor_p{R_1/k}(M_1,N_1)⊗Tor_q{R_2/k}(M_2,N_2)→Tor_{p+q}^{(R_1⊗R_2)/k}(M_1⊗M_2,N_1⊗N_2), with the analogous external product for relative Ext. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Example 8.7.13
If R is k-flat and I is generated by a regular sequence of length d, then T=Tor_1{R/k}(R/I,R/I)≅(R/I)d and Tor_i{R/k}(R/I,R/I)≅ΛiT; hence these groups vanish for i>d.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: If R is k-flat and I is generated by a regular sequence of length d, then T=Tor_1{R/k}(R/I,R/I)≅(R/I)d and Tor_i{R/k}(R/I,R/I)≅ΛiT; hence these groups vanish for i>d. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Theorem 8.7.14
Relative Tor and Ext over a product ring split componentwise: the relative groups for R×R′ are the direct sums/products of the corresponding relative groups for R and R′.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: Relative Tor and Ext over a product ring split componentwise: the relative groups for R×R′ are the direct sums/products of the corresponding relative groups for R and R′. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Definition — relatively flat module
A right R-module P is relatively flat if P⊗*R N** is exact for every k-split exact sequence N_* of left R-modules; equivalently Tor_n^R/k(P,N)=0 for n>0 and all left R-modules N
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: A right R-module P is relatively flat if P⊗*R N** is exact for every k-split exact sequence N_* of left R-modules; equivalently Tor_n^R/k(P,N)=0 for n>0 and all left R-modules N Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Lemma — Relatively Flat Resolution Lemma 8.7.15
If P_→M is a k-split resolution by relatively flat right R-modules, then Tor_^{R/k}(M,N)≅H_(P_⊗_R N) for every left R-module N.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: If P_→M is a k-split resolution by relatively flat right R-modules, then Tor_^{R/k}(M,N)≅H_(P_⊗_R N) for every left R-module N. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Corollary 8.7.16
If R→T makes T flat as an R-module, then for every right T-module M and left R-module N there is a natural flat-base-change isomorphism Tor_^{R/k}(M,N)≅Tor_^{T/k}(M,T⊗_R N).
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: If R→T makes T flat as an R-module, then for every right T-module M and left R-module N there is a natural flat-base-change isomorphism Tor_^{R/k}(M,N)≅Tor_^{T/k}(M,T⊗_R N). Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Application/comparison — Vista 8.7.17
The free-ring cotriple on nonunital rings gives cotriple homology theories underlying algebraic K-theoretic constructions discussed in the vista.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: The free-ring cotriple on nonunital rings gives cotriple homology theories underlying algebraic K-theoretic constructions discussed in the vista. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Convention — §8.8 fixes k and the category of commutative k-algebras
Fix a commutative ring k and work in the category of commutative k-algebras for §8.8.
Formalized. Mathlib/Algebra/Category/CommAlgCat/Basic.lean::CommAlgCat; CommAlgCat.Hom — Pinned Mathlib bundles commutative unital k-algebras and k-algebra homomorphisms into the category used in the source section.
Searched: P
Definition 8.8.1
Defines the Kähler differential module Ω_R/k by generators dr and the additivity/Leibniz relations; also defines k-derivations D:R→M and the R-module Der_k(R,M)
Formalized. Mathlib/RingTheory/Kaehler/Basic.lean::KaehlerDifferential; KaehlerDifferential.D; Derivation.liftKaehlerDifferential; KaehlerDifferential.linearMapEquivDerivation — Pinned Mathlib defines Ω_{B/A}, the universal derivation, and the natural equivalence from B-linear maps out of Ω to A-derivations.
Searched: P
Definitions 8.8.2
Defines André-Quillen cohomology Dn(R/k,M)=πn Der_k(⊥**R,M), the cotangent complex L_R/k=[n↦R⊗⊥nRΩ*⊥_nR/k], and André-Quillen homology D_n(R/k,M)=π_n(M⊗_R L_R/k)
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: Defines André-Quillen cohomology Dn(R/k,M)=πn Der_k(⊥**R,M), the cotangent complex L_R/k=[n↦R⊗⊥nRΩ*⊥_nR/k], and André-Quillen homology D_n(R/k,M)=π_n(M⊗_R L_R/k) Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Definition/comparison — simplicial polynomial resolutions compute André-Quillen theory
A simplicial polynomial resolution P_*→R has each P_n polynomial over k and is aspherical on underlying simplicial sets. Such a resolution is simplicially homotopy equivalent to the canonical cotriple resolution and computes André–Quillen (co)homology and the cotangent complex.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: A simplicial polynomial resolution P_*→R has each P_n polynomial over k and is aspherical on underlying simplicial sets. Such a resolution is simplicially homotopy equivalent to the canonical cotriple resolution and computes André–Quillen (co)homology and the cotangent complex. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Application 8.8.3
If k is noetherian and R is a finitely generated k-algebra, one can choose a simplicial polynomial resolution P_*→R in which every P_n is a polynomial k-algebra on finitely many variables.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: If k is noetherian and R is a finitely generated k-algebra, one can choose a simplicial polynomial resolution P_*→R in which every P_n is a polynomial k-algebra on finitely many variables. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Application 8.8.4
If Tor_i^k(K,R)=0 for i>0 (in particular if one algebra is k-flat), André–Quillen homology and cohomology satisfy the stated flat base-change isomorphisms after K⊗_kR.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: If Tor_i^k(K,R)=0 for i>0 (in particular if one algebra is k-flat), André–Quillen homology and cohomology satisfy the stated flat base-change isomorphisms after K⊗_kR. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Application/comparison 8.8.5
When R is k-free, the symmetric-algebra cotriple from k-modules gives an alternative simplicial resolution; comparison with the free-set cotriple yields the same André–Quillen groups.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: When R is k-free, the symmetric-algebra cotriple from k-modules gives an alternative simplicial resolution; comparison with the free-set cotriple yields the same André–Quillen groups. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Named exact sequences 8.8.6
For k→K→R and an R-module M, the transitivity theorem gives the Jacobi–Zariski long exact sequences relating André–Quillen (co)homology of R/k, R/K, and K/k.
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: For k→K→R and an R-module M, the transitivity theorem gives the Jacobi–Zariski long exact sequences relating André–Quillen (co)homology of R/k, R/K, and K/k. Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Theorem — Barr’s Theorem 8.8.7
If a natural R-module complex C_(R) has H_0(C_(R))≅Ω_R/k, is a split resolution of Ω_R/k for polynomial R, and has C_p(R)≅R⊗*k F_p(UR) functorially, then Dq(R/k,M)≅Hq Hom_R(C**(R),M) and D_q(R/k,M)≅H_q(M⊗*R C**(R))
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: If a natural R-module complex C_(R) has H_0(C_(R))≅Ω_R/k, is a split resolution of Ω_R/k for polynomial R, and has C_p(R)≅R⊗*k F_p(UR) functorially, then Dq(R/k,M)≅Hq Hom_R(C**(R),M) and D_q(R/k,M)≅H_q(M⊗*R C**(R)) Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Preview 8.8.8
Preview of Chapter 9: the natural Hochschild chain complex has H_1(R,R)≅Ω_R/k; its Hodge summands are then used with Barr’s theorem, leading to the characteristic-zero André-Quillen comparison
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: Preview of Chapter 9: the natural Hochschild chain complex has H_1(R,R)≅Ω_R/k; its Hodge summands are then used with Barr’s theorem, leading to the characteristic-zero André-Quillen comparison Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.
Corollary 8.8.9
If k is a characteristic-zero field, André–Quillen homology and cohomology are the first Hodge summands of Hochschild theory: D_q(R/k,M)≅HH_{q+1}^{(1)}(R,M) and Dq(R/k,M)≅HH{q+1}_{(1)}(R,M).
Not formalized. partial: adjacent simplicial, Dold–Kan, monad/comonad, homological-algebra, or Kähler-differential infrastructure — No checked A/P/H/O/E declaration realizes the whole source bundle: If k is a characteristic-zero field, André–Quillen homology and cohomology are the first Hodge summands of Hochschild theory: D_q(R/k,M)≅HH_{q+1}^{(1)}(R,M) and Dq(R/k,M)≅HH{q+1}_{(1)}(R,M). Under strict bundle semantics, adjacent prerequisites, a converse not formalized, a narrower specialization, or a proper subset do not own the row.