Chapter 9. Hochschild and Cyclic Homology
FC05 — Weibel, An Introduction to Homological Algebra.
This chapter contains 36 definitions, 15 theorems, 18 propositions, 19 lemmas, 25 corollaries, 9 examples, 13 constructions, 4 conventions, 1 notation and 24 other statements.
Of the 164 statements checked against Lean, 14 are formalized somewhere and 150 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 150 | 91% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 13 | 8% | Mathlib states and proves it. |
| in another Lean project | 1 | 1% | Some other Lean development has it; using it means porting that code. |
| checked in total | 164 |
- Project-first search was performed at repository HEAD
f90173886bc881c2d43c0a7eb2d9fe7f110ac9a5. No project declaration owns a complete C09 source row under strict bundle semantics. - Pinned Mathlib is
P=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0, Apache-2.0 and directly project-compatible. Every P declaration cited below was checked at that revision; the complete positive interface set compiles together in/tmp/fc05_c09_all_targets_probe.lean, and the two derived interface chains for Kähler localization/essential finite type compile in/tmp/fc05_c09_derived_positive_probe.lean. - Current Mathlib was refreshed on 2026-09-06 at
H=5aedf732b6987e8c26ab3c9ebc855314f82b045f, Apache-2.0, Lean 4.34.0-rc2. Neither P nor H contains a Hochschild-homology or cyclic-homology implementation. Current searches likewise found no completed Connes/mixed-complex, cyclic, negative/periodic cyclic, or Loday–Quillen package closing the corresponding source bundles. T=0857cbca8b6a91dd22680eba45ecc284c14d8325is the refreshed 2026-09-06 TauCeti HEAD, Apache-2.0, Lean 4.34.0-rc2. Targeted T searches found nearby tensor-coalgebra primitives and Kähler infrastructure but no Hochschild/cyclic complex or theorem bundle matching C09. The reduced-tensor-coalgebra primitive theorem is specific to that coalgebra and does not own the generic primitive-elements row U156.- U038 is the only C09 route in this block that depends on post-pin current Mathlib:
Mathlib/FieldTheory/TranscendentalSeparable.lean::Algebra.IsSeparablyGeneratedat exact revision5aedf732b6987e8c26ab3c9ebc855314f82b045f; the file is absent at P, so it isreference-port, notmathlib. - Indexed GitHub code search on 2026-09-06 returned no Lean code for the phrases “Hochschild homology”, identifiers
HochschildHomology/CyclicHomology, or a substantive cyclic-homology implementation. The sole phrase hit for “cyclic homology” wasdeancureton/sphere-six-complexat revision895c0a0661501581c34d42fea3c553d4f0ee43b1, where “infinite-cyclic homology” refers to an ordinary chain homology group; it is not cyclic homology theory and is not a reference-port. Open Mathlib PR searches found no Hochschild/cyclic-homology work closing these gaps. - U004 is not inferred from the standard tensor-product action alone.
Mathlib/Algebra/Module/Bimodule.leanexplains and suppliesTensorProduct.Algebra.module, but does not package the full equivalence between bimodules and modules overR⊗Rᵐᵒᵖstated by the source row. - U006 is exact even though the flat tensor-product proof is installed as an instance: the named pinned ingredients
Module.Flat.iff_rTensor_injectiveₛandModule.Flat.rTensor_preserves_injective_linearMap, together withModule.Projective.tensorProduct, realize the two source implications; the project-pin instance check compiles. - U015 is routed through the exact localized-module interface:
KaehlerDifferential.isLocalizedModule_mapregisters the Kähler map under localization andIsLocalizedModule.linearEquivsupplies the canonical localized-module isomorphism. - U020–U025 are not inferred from field-theoretic separability, formal étaleness, or Azumaya infrastructure. The source defines separable finite-dimensional algebras through semisimplicity after every field extension and then proves equivalences with enveloping-module projectivity/HH vanishing. P has adjacent
FormallyEtale,Algebra.IsSeparablefor fields, andIsAzumaya.matrix, but not that complete source chain;Algebra/Azumaya/Defs.leanexplicitly lists the center-plus-separable-algebra characterization as future work. - In U035–U050, the source’s term “smooth” denotes the square-zero lifting property; this is P’s
Algebra.FormallySmooth, not P’s finite-presentationAlgebra.Smooth. U035, U037, U039 and U050 therefore have exact P owners. For U037,/tmp/fc05_c09_u037_probe.leancompiles both split fundamental sequences at P: Jacobi–Zariski/H₁-cotangent exactness gives injectivity of the left maps and projectivity of the right Kähler modules gives splitting. U036 remains unmatched because its full bundle additionally includes Hochschild/symmetric-H² statements. - P’s
FieldTheory/SeparablyGenerated.leandevelops criteria but has no standalone separably-generated predicate. H addsMathlib/FieldTheory/TranscendentalSeparable.lean::Algebra.IsSeparablyGenerated, which exactly realizes U038 and is therefore a revision-specific reference-port. The same H file definesAlgebra.IsTranscendentalSeparable, but U041 also bundles the smoothness conclusion, which H does not prove; U040–U044 likewise contain stronger arbitrary-extension smoothness/reducedness bundles not supplied by the checked current files. - U073 is not inferred from P’s category-theoretic Morita equivalence:
Mathlib/RingTheory/Morita/Basic.leanexplicitly lists the characterization by invertible bimodules—the literal source definition—as TODO. U074 is direct becauseMorita/Matrix.leanconstructs the matrix-ring equivalence. - No checked P/H/T declaration supplies the algebraic de Rham differential/complex U124 or the complete primitive/DG-coalgebra bundles U156/U162. H does add
Mathlib/RingTheory/Coalgebra/Primitive.lean::Coalgebra.skewPrimitive, which gives the ungraded primitive-element submodule after specializing to(1,1), but U156 also requires the graded-submodule statement, so strict bundle semantics leave U156 unmatched. TauCeti’s tensor-coalgebra primitive calculation is still only a special case. Ndenotes dated 2026-09-06 negative evidence after project-first inspection, P, H/current Mathlib, T, open Mathlib work, indexed GitHub search, and relevant external Lean repositories. A prerequisite, mathematically derivable consequence, analogous construction, differently scoped theorem, or proper subset of a bundled row is not credited as that row’s route.
Convention — chapter-wide tensor-product notation over the fixed commutative ring k
Fix a commutative base ring k. Throughout Chapter 9, tensor products are over k unless otherwise indicated, and R^{⊗n} denotes the n-fold tensor power.
Formalized. Mathlib/LinearAlgebra/TensorPower/Basic.lean::TensorPower — Pinned Mathlib defines the n-fold tensor power over a commutative base and provides the notation ⨂[k]^n R, exactly the chapter convention R^{⊗n}.
Searched: P
Definition/construction 9.1.1
For a k-algebra R and R-bimodule M, defines the standard simplicial Hochschild module M⊗R^⊗, Hochschild homology H_n(R,M)=π_n(M⊗R^⊗), the dual cosimplicial module Hom_k(R^⊗,M), and Hochschild cohomology Hn(R,M)=πn Hom_k(R^⊗,M)
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For a k-algebra R and R-bimodule M, defines the standard simplicial Hochschild module M⊗R^⊗, Hochschild homology H_n(R,M)=π_n(M⊗R^⊗), the dual cosimplicial module Hom_k(R^⊗,M), and Hochschild cohomology Hn(R,M)=πn Hom_k(R^⊗,M) Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Example 9.1.2
For a group G and right G-module M, the Hochschild complex of kG with the bimodule obtained by giving M trivial left G-action recovers the usual bar complex; hence Hochschild homology recovers group homology with these coefficients.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For a group G and right G-module M, the Hochschild complex of kG with the bimodule obtained by giving M trivial left G-action recovers the usual bar complex; hence Hochschild homology recovers group homology with these coefficients. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition/construction — enveloping algebra R^e and bimodules as R^e-modules
For a k-algebra R, the enveloping algebra is R^e=R⊗_k R^op. R-bimodules are equivalently left R^e-modules, with (r⊗s^op)m=rms.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For a k-algebra R, the enveloping algebra is R^e=R⊗_k R^op. R-bimodules are equivalently left R^e-modules, with (r⊗s^op)m=rms. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Lemma 9.1.3
For a k-algebra R with enveloping algebra Re=R⊗kR^op and R-bimodule M, Hochschild groups are relative derived functors: HH(R,M)≅Tor_{R^e/k}(M,R) and HH^(R,M)≅Ext_{Re/k}(R,M).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For a k-algebra R with enveloping algebra R^e=R⊗*kR^op and R-bimodule M, Hochschild groups are relative derived functors: HH**(R,M)≅Tor_{Re/k}(M,R) and HH^(R,M)≅Ext_{Re/k}*(R,M). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Lemma 9.1.4
If P and Q are flat k-modules, then P⊗_kQ is flat; if P and Q are projective k-modules, then P⊗_kQ is projective.
Formalized. Mathlib/RingTheory/Flat/Basic.lean::Module.Flat.iff_rTensor_injectiveₛ, Module.Flat.rTensor_preserves_injective_linearMap; Mathlib/Algebra/Module/Projective.lean::Module.Projective.tensorProduct — At the project pin, Mathlib proves tensor products of flat modules are flat via the named injectivity criterion/preservation API, and Module.Projective.tensorProduct gives the projective statement. The combined U006 instance check compiles in the project environment.
Searched: P
Corollary 9.1.5
If R is k-flat, then HH_(R,M)≅Tor_{Re}(M,R); if R is k-projective, then HH^(R,M)≅Ext_{Re}(R,M).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: If R is k-flat, then HH_(R,M)≅Tor_{Re}(M,R); if R is k-projective, then HH^(R,M)≅Ext_{Re}(R,M). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Proposition 9.1.6
For T=T(V) and a T-bimodule M, HH_i(T,M)=0 for i≠0,1 and there is an exact sequence 0→HH_1(T,M)→M⊗V→^b M→HH_0(T,M)→0 with b(m⊗v)=mv-vm.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For T=T(V) and a T-bimodule M, HH_i(T,M)=0 for i≠0,1 and there is an exact sequence 0→HH_1(T,M)→M⊗V→^b M→HH_0(T,M)→0 with b(m⊗v)=mv-vm. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Theorem 9.1.7
For a commutative ring map k→ℓ, k-algebra R, and R_ℓ-bimodule M, extension of scalars gives natural isomorphisms HH_^k(R,M)≅HH_^ℓ(R⊗_kℓ,M) and likewise in Hochschild cohomology.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For a commutative ring map k→ℓ, k-algebra R, and R_ℓ-bimodule M, extension of scalars gives natural isomorphisms HH_^k(R,M)≅HH_^ℓ(R⊗_kℓ,M) and likewise in Hochschild cohomology. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Theorem 9.1.8
For k-algebras, Hochschild (co)homology is compatible with finite products; under flat base change R→T one has the stated tensor base-change formula; localization at a central multiplicative set is the corresponding special case.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For k-algebras, Hochschild (co)homology is compatible with finite products; under flat base change R→T one has the stated tensor base-change formula; localization at a central multiplicative set is the corresponding special case. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Lemma 9.1.9
For left R-modules M,N, the bimodule Hom_k(M,N) satisfies HHn(R,Hom_k(M,N))≅Extn_{R/k}(M,N).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For left R-modules M,N, the bimodule Hom_k(M,N) satisfies HHn(R,Hom_k(M,N))≅Extn_{R/k}(M,N). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition — derivations and principal derivations
A k-derivation f:R→M satisfies f(rs)=r f(s)+f(r)s. Principal derivations are f_m(r)=rm-mr; write Der_k(R,M) and PDer_k(R,M) for the respective modules.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: A k-derivation f:R→M satisfies f(rs)=r f(s)+f(r)s. Principal derivations are f_m(r)=rm-mr; write Der_k(R,M) and PDer_k(R,M) for the respective modules. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Lemma 9.2.1
The first Hochschild cohomology is H^1(R,M)≅Der_k(R,M)/PDer_k(R,M). For commutative R, Kähler differentials Ω_{R/k} represent k-derivations.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: The first Hochschild cohomology is H^1(R,M)≅Der_k(R,M)/PDer_k(R,M). For commutative R, Kähler differentials Ω_{R/k} represent k-derivations. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Proposition 9.2.2
For commutative R and a right R-module M made symmetric as a bimodule, HH_0(R,M)≅M and HH_1(R,M)≅M⊗RΩ{R/k}; in particular HH_1(R,R)≅Ω_{R/k}.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For commutative R and a right R-module M made symmetric as a bimodule, HH_0(R,M)≅M and HH_1(R,M)≅M⊗RΩ{R/k}; in particular HH_1(R,R)≅Ω_{R/k}. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Corollary 9.2.3
For a commutative k-algebra R and multiplicative set S, Kähler differentials commute with localization: Ω_{S{-1}R/k}≅S{-1}Ω_{R/k}.
Formalized. Mathlib/RingTheory/Etale/Kaehler.lean::KaehlerDifferential.isLocalizedModule_map; Mathlib/Algebra/Module/LocalizedModule/Basic.lean::IsLocalizedModule.linearEquiv — For a localization R→S⁻¹R, the pinned Kähler map is registered as a localized-module map; the generic localized-module linear equivalence identifies the target with the localization of Ω[R/k], giving the source isomorphism.
Searched: P
Construction/comparison — Alternate Calculation 9.2.4
Let I=ker(R⊗_kR→R), where multiplication is the map. The k-split exact sequence 0→I→R^e→R→0 gives an alternative low-degree Hochschild calculation and identifies the universal derivation class in I/I^2.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Let I=ker(R⊗_kR→R), where multiplication is the map. The k-split exact sequence 0→I→R^e→R→0 gives an alternative low-degree Hochschild calculation and identifies the universal derivation class in I/I^2. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Example 9.2.5
If R/k is a separable algebraic field extension, then Ω_{R/k}=0: for r∈R a separable polynomial relation f(r)=0 gives f′(r)dr=0 with f′(r) invertible.
Formalized. Mathlib/RingTheory/Etale/Field.lean::Algebra.FormallyEtale.of_isSeparable; Mathlib/RingTheory/Etale/Basic.lean::Algebra.FormallyEtale.subsingleton_kaehlerDifferential — A separable field extension is formally étale at the pin, and formal étaleness makes its Kähler differential module subsingleton, hence zero, exactly the source calculation.
Searched: P
Named exact sequence — First Fundamental Exact Sequence for \(\Omega\) 9.2.6
For commutative ring maps k→R→T there is an exact sequence Ω_{R/k}⊗R T → Ω{T/k} → Ω_{T/R} → 0.
Formalized. Mathlib/RingTheory/Kaehler/Basic.lean::KaehlerDifferential.exact_mapBaseChange_map, KaehlerDifferential.map_surjective — Pinned Mathlib proves exactness of T⊗[R]Ω[R/k] → Ω[T/k] → Ω[T/R] and surjectivity of the last map, exactly the first fundamental sequence.
Searched: P
Named exact sequence — Second Fundamental Exact Sequence for & 9.2.7
For an ideal I of a commutative k-algebra R there is an exact conormal sequence I/I^2 → Ω_{R/k}⊗R R/I → Ω{(R/I)/k} → 0.
Formalized. Mathlib/RingTheory/Kaehler/Basic.lean::KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange, KaehlerDifferential.mapBaseChange_surjective — For a surjection R→R/I, pinned Mathlib proves exactness I/I² → (R/I)⊗[R]Ω[R/k] → Ω[(R/I)/k] and surjectivity of the second map, exactly the source conormal sequence.
Searched: P
Definition — finite-dimensional separable k-algebra
A finite-dimensional semisimple k-algebra R is separable when R⊗_kℓ remains semisimple for every field extension ℓ/k.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: A finite-dimensional semisimple k-algebra R is separable when R⊗_kℓ remains semisimple for every field extension ℓ/k. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Lemma 9.2.8
For a finite field extension K/k, the finite-dimensional algebra K is separable in the algebra sense of §9.2 exactly when K/k is separable in the field-theoretic sense.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For a finite field extension K/k, the finite-dimensional algebra K is separable in the algebra sense of §9.2 exactly when K/k is separable in the field-theoretic sense. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Corollary 9.2.9
A finite-dimensional commutative k-algebra is separable iff it is a finite product of finite separable field extensions of k.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: A finite-dimensional commutative k-algebra is separable iff it is a finite product of finite separable field extensions of k. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Lemma 9.2.10
For R=M_m(k), the R^e-module R is projective.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For R=M_m(k), the R^e-module R is projective. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Theorem 9.2.11
For a k-algebra R over a field, the following are equivalent: R is finite-dimensional separable; R is projective as an R^e-module; HH_n(R,M)=0 for all n>0 and all bimodules M; HH^n(R,M)=0 for all n>0 and all bimodules M.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For a k-algebra R over a field, the following are equivalent: R is finite-dimensional separable; R is projective as an R^e-module; HH_n(R,M)=0 for all n>0 and all bimodules M; HH^n(R,M)=0 for all n>0 and all bimodules M. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Lemma 9.2.12
If a k-algebra R is projective as an R^e-module, then R is finite-dimensional over k (Villamayor–Zelinsky).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: If a k-algebra R is projective as an R^e-module, then R is finite-dimensional over k (Villamayor–Zelinsky). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition/construction — square-zero (Hochschild) extensions, factor sets, and equivalence
A square-zero extension of R by an R-bimodule M is a surjection E→R with square-zero kernel identified with M; it is Hochschild when 0→M→E→R→0 is k-split. A splitting gives a factor set f:R⊗R→M satisfying the Hochschild 2-cocycle identity, and equivalent splittings/extensions change f by a coboundary
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: A square-zero extension of R by an R-bimodule M is a surjection E→R with square-zero kernel identified with M; it is Hochschild when 0→M→E→R→0 is k-split. A splitting gives a factor set f:R⊗R→M satisfying the Hochschild 2-cocycle identity, and equivalent splittings/extensions change f by a coboundary Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Theorem — Classification Theorem 9.3.1
Equivalence classes of Hochschild square-zero extensions of a k-algebra R by an R-bimodule M are in natural bijection with HH^2(R,M).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Equivalence classes of Hochschild square-zero extensions of a k-algebra R by an R-bimodule M are in natural bijection with HH^2(R,M). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition — symmetric bimodules, symmetric factor sets, and Hs^2
For commutative R, a bimodule is symmetric when rm=mr; commutative Hochschild extensions have symmetric factor sets f(r,s)=f(s,r). The source writes H_s^2(R,M) for the submodule of H^2(R,M) represented by symmetric factor sets
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For commutative R, a bimodule is symmetric when rm=mr; commutative Hochschild extensions have symmetric factor sets f(r,s)=f(s,r). The source writes H_s^2(R,M) for the submodule of H^2(R,M) represented by symmetric factor sets Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Classification result — Commutative Extensions 9.3.1.1
For commutative R and R-module M, equivalence classes of commutative square-zero extensions of R by M are classified by the symmetric Hochschild group H_s^2(R,M).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For commutative R and R-module M, equivalence classes of commutative square-zero extensions of R by M are classified by the symmetric Hochschild group H_s^2(R,M). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Comparison — symmetric Hochschild H^2 versus André-Quillen D^1 over a field
Over a field k, the commutative-extension classification identifies H_s^2(R,M) with André-Quillen cohomology D^1(R,M); the source notes that 8.8.9 gives the characteristic-zero case
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Over a field k, the commutative-extension classification identifies H_s^2(R,M) with André-Quillen cohomology D^1(R,M); the source notes that 8.8.9 gives the characteristic-zero case Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition 9.3.2
A k-algebra R is quasi-free if every map R→T lifts across every square-zero extension E→T of k-algebras; free associative k-algebras are quasi-free.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: A k-algebra R is quasi-free if every map R→T lifts across every square-zero extension E→T of k-algebras; free associative k-algebras are quasi-free. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Proposition 9.3.3
Over a field k, a k-algebra R is quasi-free if and only if HH^2(R,M)=0 for every R-bimodule M.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Over a field k, a k-algebra R is quasi-free if and only if HH^2(R,M)=0 for every R-bimodule M. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Corollary 9.3.3.1
If R is a k-algebra over a field and HH^2(R,M)=0 for every R-bimodule M, then every k-algebra surjection E→R with nilpotent kernel admits a k-algebra section.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: If R is a k-algebra over a field and HH^2(R,M)=0 for every R-bimodule M, then every k-algebra surjection E→R with nilpotent kernel admits a k-algebra section. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Convention — §9.3.1 restricts to commutative algebras
From §9.3.1 onward in this subsection, all algebras under consideration are commutative.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: From §9.3.1 onward in this subsection, all algebras under consideration are commutative. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition — smooth k-algebra
A commutative k-algebra R is smooth if every map R→T lifts across every square-zero extension E→T in commutative k-algebras; polynomial k-algebras are smooth.
Formalized. Mathlib/RingTheory/Smooth/Basic.lean::Algebra.FormallySmooth, Algebra.FormallySmooth.iff_comp_surjective, Algebra.FormallySmooth.polynomial — Weibel’s “smooth” in this section is the square-zero lifting property that Mathlib calls FormallySmooth; iff_comp_surjective states the lifting criterion and polynomial algebras carry the instance, exactly the source definition/example.
Searched: P
Proposition 9.3.4
Over a field k, a commutative k-algebra R is smooth iff H_s^2(R,M)=0 for every R-module M. For smooth R, every surjection E→R of commutative k-algebras with nilpotent kernel splits as a k-algebra map.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Over a field k, a commutative k-algebra R is smooth iff H_s^2(R,M)=0 for every R-module M. For smooth R, every surjection E→R of commutative k-algebras with nilpotent kernel splits as a k-algebra map. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Named exact sequences — Fundamental Sequences for \(\Omega\) with Smoothness 9.3.5
For k→R→T: if T is smooth over R, 0→Ω_R/k⊗_R T→Ω_T/k→Ω_T/R→0 is split exact; if T=R/I is smooth over k, 0→I/I^2→Ω_R/k⊗R R/I→Ω(R/I)/k→0 is split exact
Formalized. Mathlib/RingTheory/Kaehler/JacobiZariski.lean::Algebra.H1Cotangent.exact_δ_mapBaseChange, Algebra.H1Cotangent.exact_map_δ; Mathlib/RingTheory/Extension/ExtendScalars.lean::Algebra.Extension.h1CotangentEquivCotangent, Algebra.Extension.cotangentComplex_comp_h1CotangentEquivCotangent; Mathlib/RingTheory/Extension/Cotangent/Basic.lean::Algebra.Extension.exact_cotangentComplex_toKaehler, Algebra.Extension.toKaehler_surjective; Mathlib/RingTheory/Smooth/Basic.lean::Algebra.FormallySmooth.projective_kaehlerDifferential; Mathlib/Algebra/Module/Projective.lean::Module.projective_lifting_property — At the project pin, Jacobi–Zariski exactness plus vanishing of H1Cotangent under formal smoothness makes the left maps injective; the ordinary/conormal sequences are exact and their right terms are projective, so Module.projective_lifting_property supplies splittings. Both source sequences were assembled and compiled in /tmp/fc05_c09_u037_probe.lean.
Searched: P
Definition — separably generated field extension
A finitely generated field extension K/k is separably generated when it has a transcendence basis (t_1,…,t_r) such that K is separably algebraic over k(t_1,…,t_r)
Formalized. Mathlib/FieldTheory/TranscendentalSeparable.lean::Algebra.IsSeparablyGenerated — Current Mathlib at 5aedf732b6987e8c26ab3c9ebc855314f82b045f defines a field extension to be separably generated exactly by the existence of a transcendence basis over which the remaining extension is separable. The file is absent at P and H uses Lean 4.34.0-rc2, so this is revision-specific reference-port evidence rather than pinned mathlib.
Searched: H
Proposition 9.3.6
If k is a field, every separably generated field extension K/k is smooth over k.
Formalized. Mathlib/RingTheory/Smooth/Field.lean::Algebra.FormallySmooth.of_algebraicIndependent_of_isSeparable — Pinned Mathlib proves that an algebraically independent transcendence family followed by a separable algebraic extension yields a formally smooth field extension; this is exactly the source separably-generated implication.
Searched: P
Corollary 9.3.7
If k is perfect, every field extension K/k is smooth; in particular this holds for every field extension in characteristic zero.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: If k is perfect, every field extension K/k is smooth; in particular this holds for every field extension in characteristic zero. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition — separable field extension via finitely generated subextensions
In positive characteristic, call K/k separable when every finitely generated intermediate extension is separably generated. Such extensions are smooth over k.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: In positive characteristic, call K/k separable when every finitely generated intermediate extension is separably generated. Such extensions are smooth over k. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Theorem 9.3.8
For a field extension k⊂K, K is separable over k if and only if K is smooth over k
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For a field extension k⊂K, K is separable over k if and only if K is smooth over k Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Comparison/remark — Remark 9.3.9
For a field extension K/k, separability is equivalent to K⊗_kℓ being reduced for every finite field extension ℓ/k.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For a field extension K/k, separability is equivalent to K⊗_kℓ being reduced for every finite field extension ℓ/k. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Lemma 9.3.10
If K/k is separably generated, then K⊗_kℓ is reduced for every field extension ℓ/k.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: If K/k is separably generated, then K⊗_kℓ is reduced for every field extension ℓ/k. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition/convention — Hilbert-Samuel function/polynomial and regular-local criterion used below
For a d-dimensional noetherian local ring (R,m), h_R(n)=length(R/m^n) agrees for n≫0 with a degree-d Hilbert–Samuel polynomial. The regular-local criterion used below is expressed through this function.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For a d-dimensional noetherian local ring (R,m), h_R(n)=length(R/m^n) agrees for n≫0 with a degree-d Hilbert–Samuel polynomial. The regular-local criterion used below is expressed through this function. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Theorem 9.3.11
If (R,m) is a noetherian local ring containing a field k and R is smooth over k, then R is a regular local ring.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: If (R,m) is a noetherian local ring containing a field k and R is smooth over k, then R is a regular local ring. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition 9.3.12
A commutative noetherian ring R is regular when R_p is regular local for every prime p. If R contains a field k, it is geometrically regular over k when R⊗_kℓ is regular for every finite field extension ℓ/k.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: A commutative noetherian ring R is regular when R_p is regular local for every prime p. If R contains a field k, it is geometrically regular over k when R⊗_kℓ is regular for every finite field extension ℓ/k. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Corollary 9.3.13
If a commutative noetherian ring R containing a field k is smooth over k, then R is geometrically regular over k.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: If a commutative noetherian ring R containing a field k is smooth over k, then R is geometrically regular over k. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Comparison — geometric regularity implies smoothness
The converse to Corollary 9.3.13 is stated: a geometrically regular k-algebra is smooth over k (with reference to EGA IV)
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: The converse to Corollary 9.3.13 is stated: a geometrically regular k-algebra is smooth over k (with reference to EGA IV) Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Theorem 9.3.14
If R is a smooth k-algebra, then the module of Kähler differentials Ω_{R/k} is projective as an R-module.
Formalized. Mathlib/RingTheory/Smooth/Basic.lean::Algebra.FormallySmooth.projective_kaehlerDifferential — Pinned Mathlib installs projectivity of Ω[R/k] directly from the square-zero lifting (FormallySmooth) hypothesis, exactly Theorem 9.3.14 in the source terminology.
Searched: P
Application 9.3.15
For R=k[x_1,…,x_n]/J with J=(f_1,…,f_m), the conormal map J/J2→Rn is represented by the Jacobian matrix (∂f_i/∂x_j). The Jacobian criterion states that R is smooth iff this matrix has rank n−dim(R_M) over R/M for every maximal ideal M.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For R=k[x_1,…,x_n]/J with J=(f_1,…,f_m), the conormal map J/J2→Rn is represented by the Jacobian matrix (∂f_i/∂x_j). The Jacobian criterion states that R is smooth iff this matrix has rank n−dim(R_M) over R/M for every maximal ideal M. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Construction — shuffle external product on Hochschild/bar complexes
Tensoring bar resolutions and applying the shuffle map defines the external Hochschild product at chain level for pairs of k-algebras and bimodules.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Tensoring bar resolutions and applying the shuffle map defines the external Hochschild product at chain level for pairs of k-algebras and bimodules. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Proposition 9.4.1
The shuffle construction induces natural external products HH_i(R,M)⊗HH_j(R′,M′)→HH_{i+j}(R⊗R′,M⊗M′), and analogously in Hochschild cohomology.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: The shuffle construction induces natural external products HH_i(R,M)⊗HH_j(R′,M′)→HH_{i+j}(R⊗R′,M⊗M′), and analogously in Hochschild cohomology. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Comparison — associativity of the external shuffle product
The explicit shuffle formula makes the external Hochschild product associative for triple tensor products of algebras and coefficient bimodules
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: The explicit shuffle formula makes the external Hochschild product associative for triple tensor products of algebras and coefficient bimodules Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Construction — internal Hochschild product for commutative algebras
If R is commutative, multiplication R⊗R→R turns the external Hochschild products into internal products; in homology this gives HH_p(R,M)⊗HH_q(R,M′)→HH_{p+q}(R,M⊗_{R^e}M′).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: If R is commutative, multiplication R⊗R→R turns the external Hochschild products into internal products; in homology this gives HH_p(R,M)⊗HH_q(R,M′)→HH_{p+q}(R,M⊗_{R^e}M′). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Proposition 9.4.2
For commutative R, the Hochschild chain complex C(R⊗R^⊗) with shuffle product is a graded-commutative differential graded k-algebra; consequently H_(R,R) is a graded-commutative k-algebra
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For commutative R, the Hochschild chain complex C(R⊗R^⊗) with shuffle product is a graded-commutative differential graded k-algebra; consequently H_(R,R) is a graded-commutative k-algebra Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Corollary 9.4.3
For commutative R and any R-bimodule M, HH_(R,M) is naturally a graded module over the graded ring HH_(R,R).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For commutative R and any R-bimodule M, HH_(R,M) is naturally a graded module over the graded ring HH_(R,R). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition/construction — exterior algebra of Kähler differentials
For commutative R, the exterior algebra of Kähler differentials is Ω^**{R/k}=⊕*{n≥0}Λ_R^nΩ_{R/k}, with Ω^0_{R/k}=R.
Formalized. Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean::ExteriorAlgebra; Mathlib/LinearAlgebra/ExteriorAlgebra/Grading.lean::ExteriorAlgebra.gradedAlgebra; Mathlib/LinearAlgebra/ExteriorPower/Basic.lean::exteriorPower — Applying the pinned exterior algebra and its grading to Ω[R/k] gives the direct-sum graded algebra with degree n equal to Λ_R^n Ω[R/k] (and degree zero canonically R), exactly the source construction.
Searched: P
Corollary 9.4.4
For commutative R, the degree-one isomorphism Ω_{R/k}≅HH_1(R,R) extends to a natural graded-algebra map ψ:Ω^{R/k}→HH(R,R). If Q⊂R, ψ is split injective via e(r_0⊗⋯⊗r_n)=r_0dr_1∧⋯∧dr_n/n!.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For commutative R, the degree-one isomorphism Ω_{R/k}≅HH_1(R,R) extends to a natural graded-algebra map ψ:Ω^{R/k}→HH(R,R). If Q⊂R, ψ is split injective via e(r_0⊗⋯⊗r_n)=r_0dr_1∧⋯∧dr_n/n!. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition 9.4.5
A commutative k-algebra R is essentially of finite type if it is a localization of a finitely generated k-algebra. If k is noetherian, then R and R^e are noetherian.
Formalized. Mathlib/RingTheory/EssentialFiniteness.lean::Algebra.EssFiniteType, Algebra.EssFiniteType.baseChange, Algebra.EssFiniteType.isNoetherianRing — Pinned EssFiniteType is localization of a finite-type algebra. Over a Noetherian base it gives R Noetherian; base change makes R⊗_kR essentially finite type over R, so it is Noetherian as well. Both instance chains were compile-checked at P.
Searched: P
Proposition 9.4.6
If R is a commutative k-algebra essentially of finite type over a field and R is smooth over k, then the enveloping ring R^e=R⊗_kR is regular.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: If R is a commutative k-algebra essentially of finite type over a field and R is smooth over k, then the enveloping ring R^e=R⊗_kR is regular. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Theorem 9.4.7
Hochschild–Kostant–Rosenberg: if R is a commutative k-algebra essentially of finite type over a field and smooth over k, then ψ:Ω^{R/k}→HH(R,R) is an isomorphism of graded R-algebras.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Hochschild–Kostant–Rosenberg: if R is a commutative k-algebra essentially of finite type over a field and smooth over k, then ψ:Ω^{R/k}→HH(R,R) is an isomorphism of graded R-algebras. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Comparison/remark — Remark 9.4.8
Under the regularity hypotheses of §9.4, Ω_{R/k} is projective and for each maximal ideal m its localization Ω_{R/k,m} is free of rank dim(R_m).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Under the regularity hypotheses of §9.4, Ω_{R/k} is projective and for each maximal ideal m its localization Ω_{R/k,m} is free of rank dim(R_m). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition/comparison — Hodge/λ decomposition target for Hochschild (co)homology
For commutative R containing Q, the Hochschild chain complex decomposes into Hodge subcomplexes C_*h(R){(i)}, yielding Hodge decompositions of Hochschild homology and cohomology; the first summand is related to André–Quillen homology.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For commutative R containing Q, the Hochschild chain complex decomposes into Hodge subcomplexes C_*h(R){(i)}, yielding Hodge decompositions of Hochschild homology and cohomology; the first summand is related to André–Quillen homology. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Lemma — Barr’s Lemma 9.4.9
Barr’s lemma: if u∈QΣ_n has the universal property that the associated Hochschild boundary vanishes for every algebra, then u is a scalar multiple of the antisymmetrizer ε_n.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Barr’s lemma: if u∈QΣ_n has the universal property that the associated Hochschild boundary vanishes for every algebra, then u is a scalar multiple of the antisymmetrizer ε_n. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition — shuffle elements spq and sn in the symmetric-group ring
For n>1 and p+q=n, define the shuffle element s_{pq}∈ZΣ_n as the signed sum of all (p,q)-shuffles, and set s_n=Σ_{0<p<n}s_{p,n-p}.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For n>1 and p+q=n, define the shuffle element s_{pq}∈ZΣ_n as the signed sum of all (p,q)-shuffles, and set s_n=Σ_{0<p<n}s_{p,n-p}. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Lemma 9.4.10
The Hochschild differential intertwines shuffle operators: b s_n=s_{n-1} b for every n.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: The Hochschild differential intertwines shuffle operators: b s_n=s_{n-1} b for every n. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Proposition 9.4.11
The minimal polynomial of the shuffle operator s_n on QΣ_n is x(x-λ_2)…(x-λ_n), with λ_i=2^i-2.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: The minimal polynomial of the shuffle operator s_n on QΣ_n is x(x-λ_2)…(x-λ_n), with λ_i=2^i-2. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition 9.4.12
Defines the idempotents e_n^(i) from Proposition 9.4.11 as the Eulerian idempotents of QΣ_n, with e_0^(0)=1 and e_n^(0)=0 for n>0
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Defines the idempotents e_n^(i) from Proposition 9.4.11 as the Eulerian idempotents of QΣ_n, with e_0^(0)=1 and e_n^(0)=0 for n>0 Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Corollary 9.4.13
e_n ^(n) is the signature idempotent ε_n
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: e_n ^(n) is the signature idempotent ε_n Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Corollary — Corolary 94.4 [OCR-damaged label; later cited as 9.4.14]
The Hodge idempotents satisfy b e_n(i)=e_{n-1}(i)b for i<n and b e_n^(n)=0. Definition 9.4.15 explicitly cites this source result as 9.4.14.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: The Hodge idempotents satisfy b e_n(i)=e_{n-1}(i)b for i<n and b e_n^(n)=0. Definition 9.4.15 explicitly cites this source result as 9.4.14. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition 9.4.15
For commutative R containing Q, define C_nh(R){(i)}=e_n{(i)}(R⊗R{⊗n}); Corollary 9.4.14 makes these chain subcomplexes. Their homology groups H_n^{(i)}(R,R) give the Hodge decomposition of HH_n(R,R).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For commutative R containing Q, define C_nh(R){(i)}=e_n{(i)}(R⊗R{⊗n}); Corollary 9.4.14 makes these chain subcomplexes. Their homology groups H_n^{(i)}(R,R) give the Hodge decomposition of HH_n(R,R). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition 9.5.1
Two rings R and S are Morita equivalent when there are bimodules _R P_S and _S Q_R with P⊗_S Q≅R as R-bimodules and Q⊗_R P≅S as S-bimodules.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Two rings R and S are Morita equivalent when there are bimodules _R P_S and _S Q_R with P⊗_S Q≅R as R-bimodules and Q⊗_R P≅S as S-bimodules. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Proposition 9.5.2
For every ring R and m≥1, M_m(R) is Morita equivalent to R.
Formalized. Mathlib/RingTheory/Morita/Matrix.lean::ModuleCat.matrixEquivalence, moritaEquivalenceMatrix, IsMoritaEquivalent.matrix — Pinned Mathlib constructs the equivalence between modules over R and over a nonempty square matrix ring and packages it as Morita equivalence, exactly Proposition 9.5.2.
Searched: P
Corollary 9.5.3
Under Morita equivalence R-mod-R ≃ M_m(R)-mod-M_m(R), an R-bimodule M corresponds to the matrix bimodule M_m(M).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Under Morita equivalence R-mod-R ≃ M_m(R)-mod-M_m(R), an R-bimodule M corresponds to the matrix bimodule M_m(M). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Lemma 9.5.4
If bimodules P,Q implement a Morita equivalence between R and S, then P is finitely generated projective both as a left R-module and as a right S-module.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: If bimodules P,Q implement a Morita equivalence between R and S, then P is finitely generated projective both as a left R-module and as a right S-module. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Lemma 9.5.5
If L is a left R-module and Q a projective right R-module, then HH_i(R,L⊗Q)=0 for i>0 and HH_0(R,L⊗Q)≅Q⊗_R L.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: If L is a left R-module and Q a projective right R-module, then HH_i(R,L⊗Q)=0 for i>0 and HH_0(R,L⊗Q)≅Q⊗_R L. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Theorem 9.5.6
Hochschild homology is Morita invariant: if R and S are Morita equivalent via P,Q, then HH_(R,M)≅HH_(S,Q⊗_R M⊗_R P) naturally in the R-bimodule M.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Hochschild homology is Morita invariant: if R and S are Morita equivalent via P,Q, then HH_(R,M)≅HH_(S,Q⊗_R M⊗_R P) naturally in the R-bimodule M. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition 9.5.7
The matrix trace tr:M_m(R)→R is tr((g_{ij}))=Σ_i g_{ii}; its tensor-level extension gives the explicit Morita comparison used below.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: The matrix trace tr:M_m(R)→R is tr((g_{ij}))=Σ_i g_{ii}; its tensor-level extension gives the explicit Morita comparison used below. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Corollary 9.5.8
Under the Morita equivalence R≃M_m(R), the isomorphism HH_(M_m(R),M_m(M))→HH_(R,M) is induced by the explicit trace map.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Under the Morita equivalence R≃M_m(R), the isomorphism HH_(M_m(R),M_m(M))→HH_(R,M) is induced by the explicit trace map. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Construction — cyclic operator on the standard Hochschild simplicial module ZR
The standard Hochschild simplicial module ZR has Z_nR=R^{⊗(n+1)} and cyclic operator t(r_0⊗⋯⊗r_n)=r_n⊗r_0⊗⋯⊗r_{n-1}, giving an action of C_{n+1} compatible with the simplicial operators.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: The standard Hochschild simplicial module ZR has Z_nR=R^{⊗(n+1)} and cyclic operator t(r_0⊗⋯⊗r_n)=r_n⊗r_0⊗⋯⊗r_{n-1}, giving an action of C_{n+1} compatible with the simplicial operators. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition 9.6.1
A cyclic object is a simplicial object A together with automorphisms t_n:A_n→A_n of order n+1 satisfying the standard compatibility identities with all face and degeneracy maps.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: A cyclic object is a simplicial object A together with automorphisms t_n:A_n→A_n of order n+1 satisfying the standard compatibility identities with all face and degeneracy maps. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Example 9.6.2
The classifying simplicial set BG is cyclic: on G^n, the cyclic operator sends (g_1,…,g_n) to ((g_1…g_n)^{-1},g_1,…,g_{n-1}).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: The classifying simplicial set BG is cyclic: on G^n, the cyclic operator sends (g_1,…,g_n) to ((g_1…g_n)^{-1},g_1,…,g_{n-1}). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition 9.6.3
The cyclic category ΔC has morphisms represented by pairs (α,t^i), where α:[n]→[p] is monotone and 0≤i≤n; composition is determined by the cyclic identities.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: The cyclic category ΔC has morphisms represented by pairs (α,t^i), where α:[n]→[p] is monotone and 0≤i≤n; composition is determined by the cyclic identities. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Proposition 9.6.4
The formal pairs of Definition 9.6.3 form Connes’ cyclic category ΔC containing Δ, and cyclic objects in a category A are exactly contravariant functors ΔC→A.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: The formal pairs of Definition 9.6.3 form Connes’ cyclic category ΔC containing Δ, and cyclic objects in a category A are exactly contravariant functors ΔC→A. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definitions 9.6.5
For a cyclic object A in an abelian category, the Hochschild complex is the chain complex of the underlying simplicial object, with differential b. The companion differential b′ and norm N are the operators used to assemble the cyclic bicomplex.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For a cyclic object A in an abelian category, the Hochschild complex is the chain complex of the underlying simplicial object, with differential b. The companion differential b′ and norm N are the operators used to assemble the cyclic bicomplex. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition 9.6.6
For a cyclic object A, Tsygan’s bicomplex CC_{**}(A) has alternating Hochschild and acyclic columns, while each row is the periodic complex for the cyclic-group action with maps 1−(-1)^qt and the norm N.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For a cyclic object A, Tsygan’s bicomplex CC_{**}(A) has alternating Hochschild and acyclic columns, while each row is the periodic complex for the cyclic-group action with maps 1−(-1)^qt and the norm N. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition 9.6.7
The cyclic homology HC_(A) of a cyclic object A is H_Tot(CC_{**}(A)); for a k-algebra R, HC_(R) means HC_(ZR). In degree zero, HC_0(R)=R/[R,R].
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: The cyclic homology HC_(A) of a cyclic object A is H_Tot(CC_{**}(A)); for a k-algebra R, HC_(R) means HC_(ZR). In degree zero, HC_0(R)=R/[R,R]. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Lemma 9.6.8
C C_** ( A ) is a double complex
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: C C_** ( A ) is a double complex Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Corollary 9.6.9
Quotienting each A_n by its cyclic-group action gives a quotient chain complex A_*/(1-t); its differential is induced by the Hochschild differential b.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Quotienting each A_n by its cyclic-group action gives a quotient chain complex A_*/(1-t); its differential is induced by the Hochschild differential b. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Lemma 9.6.10
If k contains Q, cyclic homology HC_(A) is naturally isomorphic to the homology of the quotient Hochschild complex A_/∼ by the cyclic-group action.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: If k contains Q, cyclic homology HC_(A) is naturally isomorphic to the homology of the quotient Hochschild complex A_/∼ by the cyclic-group action. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Construction — I, S, and B maps leading to the SBI sequence
The inclusion of the Hochschild column defines I:HH_n(A)→HC_n(A); translation by two columns defines S:HC_n(A)→HC_{n-2}(A); the connecting morphism is B:HC_{n-1}(A)→HH_n(A).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: The inclusion of the Hochschild column defines I:HH_n(A)→HC_n(A); translation by two columns defines S:HC_n(A)→HC_{n-2}(A); the connecting morphism is B:HC_{n-1}(A)→HH_n(A). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Proposition 9.6.11
Every cyclic object A has Connes’ long exact SBI sequence …→HC_{n+1}(A)→^S HC_{n-1}(A)→^B HH_n(A)→^I HC_n(A)→^S HC_{n-2}(A)→….
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Every cyclic object A has Connes’ long exact SBI sequence …→HC_{n+1}(A)→^S HC_{n-1}(A)→^B HH_n(A)→^I HC_n(A)→^S HC_{n-2}(A)→…. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Corollary 9.6.12
If A→A′ is a morphism of cyclic objects inducing isomorphisms HH_n(A)→HH_n(A′) for all n, then it also induces isomorphisms HC_n(A)→HC_n(A′) for all n.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: If A→A′ is a morphism of cyclic objects inducing isomorphisms HH_n(A)→HH_n(A′) for all n, then it also induces isomorphisms HC_n(A)→HC_n(A′) for all n. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Application 9.6.13
The matrix trace is a morphism of cyclic modules Z(M_mR)→Z(R); since it is a Hochschild-homology isomorphism, it induces HC_(M_mR)≅HC_(R).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: The matrix trace is a morphism of cyclic modules Z(M_mR)→Z(R); since it is a Hochschild-homology isomorphism, it induces HC_(M_mR)≅HC_(R). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Example 9.6.14
For the base ring k, HH_n(k,k)=0 for n>0; the SBI sequence gives HC_n(k)≅k for even n and HC_n(k)=0 for odd n.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For the base ring k, HH_n(k,k)=0 for n>0; the SBI sequence gives HC_n(k)≅k for even n and HC_n(k)=0 for odd n. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Named calculation — \(\mathbf { H } \mathbf { C } { 1 }\) 9.6.15
The SBI sequence gives HC_1(R) as the cokernel of B:H_0(R,R)→H_1(R,R); for commutative R this identifies B with d:R→Ω_R/k, hence HC_1(R)≅Ω_R/k/dR
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: The SBI sequence gives HC_1(R) as the cokernel of B:H_0(R,R)→H_1(R,R); for commutative R this identifies B with d:R→Ω_R/k, hence HC_1(R)≅Ω_R/k/dR Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Example 9.6.16
For k[x], S:HC_{n+2}→HC_n is an isomorphism for n≥1 and 0→HC_2(k[x])→k[x]→^dΩ_{k[x]/k}→HC_1(k[x])→0 is exact. If Q⊂k, this yields HC_0=k[x], HC_{2i}=k for i≥1, and HC_{2i+1}=0.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For k[x], S:HC_{n+2}→HC_n is an isomorphism for n≥1 and 0→HC_2(k[x])→k[x]→^dΩ_{k[x]/k}→HC_1(k[x])→0 is exact. If Q⊂k, this yields HC_0=k[x], HC_{2i}=k for i≥1, and HC_{2i+1}=0. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition/construction 9.6.17
Defines periodic cyclic homology HP_(A) using the product total complex of the two-sided periodic extension of Tsygan’s bicomplex, with period-two S-isomorphisms; also defines negative cyclic homology HN_(A) from the nonpositive-column subcomplex
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Defines periodic cyclic homology HP_(A) using the product total complex of the two-sided periodic extension of Tsygan’s bicomplex, with period-two S-isomorphisms; also defines negative cyclic homology HN_(A) from the nonpositive-column subcomplex Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Notation/comparison — group homology as Hochschild homology of the cyclic module kBG
For the cyclic module kBG, write HH_(G)=HH_(kBG) and HC_(G)=HC_(kBG). Then HH_n(G)=H_n(BG;k)=H_n(G;k).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For the cyclic module kBG, write HH_(G)=HH_(kBG) and HC_(G)=HC_(kBG). Then HH_n(G)=H_n(BG;k)=H_n(G;k). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Theorem 9.7.1
For every group G, HC_n(G)≅H_n(G;k)⊕H_{n-2}(G;k)⊕⋯; under this decomposition S is projection onto the lower summands and B=0.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For every group G, HC_n(G)≅H_n(G;k)⊕H_{n-2}(G;k)⊕⋯; under this decomposition S is projection onto the lower summands and B=0. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Corollary 9.7.2
Periodic cyclic homology of kBG is the product of the ordinary group homology groups in the parity of n: HP_n(G)=∏{i≥0}H{2i}(G;k) for n even and ∏{i≥0}H{2i+1}(G;k) for n odd.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Periodic cyclic homology of kBG is the product of the ordinary group homology groups in the parity of n: HP_n(G)=∏{i≥0}H{2i}(G;k) for n even and ∏{i≥0}H{2i+1}(G;k) for n odd. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition 9.7.3
For x∈G, Z_n(G,x) is the subset of Z_nG=G^{n+1} consisting of tuples whose product g_0⋯g_n lies in the conjugacy class of x; these subsets form cyclic subobjects indexed by conjugacy classes.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For x∈G, Z_n(G,x) is the subset of Z_nG=G^{n+1} consisting of tuples whose product g_0⋯g_n lies in the conjugacy class of x; these subsets form cyclic subobjects indexed by conjugacy classes. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Proposition 9.7.4
For x∈G, inclusion of the centralizer C_G(x) into G induces isomorphisms on the Hochschild and cyclic summands attached to the conjugacy class of x.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For x∈G, inclusion of the centralizer C_G(x) into G induces isomorphisms on the Hochschild and cyclic summands attached to the conjugacy class of x. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Corollary 9.7.5
For each conjugacy class representative x, HH_(G,x)≅H_(C_G(x);k); hence HH_(kG)≅⊕{⟨x⟩}H(C_G(x);k).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For each conjugacy class representative x, HH_(G,x)≅H_(C_G(x);k); hence HH_(kG)≅⊕{⟨x⟩}H**(C_G(x);k). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Comparison/counterexample — cyclic homology does not decompose by centralizers as naively as Hochschild homology
The centralizer decomposition valid for HH_*(kG) does not naively extend to cyclic homology: for G=Z and Q⊂k, all nonidentity conjugacy-class summands HC_n(G,x) vanish for n>0.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: The centralizer decomposition valid for HH_*(kG) does not naively extend to cyclic homology: for G=Z and Q⊂k, all nonidentity conjugacy-class summands HC_n(G,x) vanish for n>0. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Lemma 9.7.6
If Q⊂k and x is central of finite order, then HC_(G,x)≅HC_(G)≅H_(G;k)⊗HC_(k).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: If Q⊂k and x is central of finite order, then HC_(G,x)≅HC_(G)≅H_(G;k)⊗HC_(k). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Corollary 9.7.7
If Q⊂k and G is finite, then HC_(kG)≅⊕{⟨x⟩}HC(C_G(x))≅k⟨G⟩⊗HC_*(k).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: If Q⊂k and G is finite, then HC_(kG)≅⊕{⟨x⟩}HC**(C_G(x))≅k⟨G⟩⊗HC_*(k). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Comparison — finite group algebras in characteristic zero are separable; Hochschild vanishing
If k is a characteristic-zero field and G is finite, Maschke implies kG is semisimple and hence separable; Theorem 9.2.11 gives HH_n(kG)=0 for n>0, and the SBI sequence gives another proof of Corollary 9.7.7
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: If k is a characteristic-zero field and G is finite, Maschke implies kG is semisimple and hence separable; Theorem 9.2.11 gives HH_n(kG)=0 for n>0, and the SBI sequence gives another proof of Corollary 9.7.7 Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Example 9.7.8
For G=C_2 and k=Z, HC_n(C_2,x) is Z in even degrees and zero in odd degrees; consequently HC_n(ZC_2)≅Z⊕Z for n even and (Z/2)^{(n+1)/2} for n odd.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For G=C_2 and k=Z, HC_n(C_2,x) is Z in even degrees and zero in odd degrees; consequently HC_n(ZC_2)≅Z⊕Z for n even and (Z/2)^{(n+1)/2} for n odd. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Theorem 9.7.9
Burghelea’s theorem (Q⊂k) decomposes HC_(kG) into finite-order conjugacy-class summands H_(C_G(x);k)⊗HC_(k) and infinite-order summands H_(C_G(x)/⟨x⟩;k).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Burghelea’s theorem (Q⊂k) decomposes HC_(kG) into finite-order conjugacy-class summands H_(C_G(x);k)⊗HC_(k) and infinite-order summands H_(C_G(x)/⟨x⟩;k). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Construction — Connes operator B and Connes double complex from a cyclic object
Eliminating the acyclic odd columns of Tsygan’s bicomplex yields Connes’ double complex, with vertical Hochschild differential b and horizontal Connes operator B.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Eliminating the acyclic odd columns of Tsygan’s bicomplex yields Connes’ double complex, with vertical Hochschild differential b and horizontal Connes operator B. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition 9.8.1
A mixed complex (M,b,B) is a nonnegatively graded object with b:M_n→M_{n-1}, B:M_n→M_{n+1}, and b²=B²=bB+Bb=0.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: A mixed complex (M,b,B) is a nonnegatively graded object with b:M_n→M_{n-1}, B:M_n→M_{n+1}, and b²=B²=bB+Bb=0. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Construction — mixed complex associated to a cyclic object
Every cyclic object A determines a mixed complex (A,b,B), where b is the Hochschild differential and B is Connes’ operator.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Every cyclic object A determines a mixed complex (A,b,B), where b is the Hochschild differential and B is Connes’ operator. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition 9.8.2
For a mixed complex (M,b,B), Connes’ first-quadrant double complex has B_{pq}=M_{q-p} for 0≤p≤q and zero otherwise, with vertical maps b and horizontal maps B.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For a mixed complex (M,b,B), Connes’ first-quadrant double complex has B_{pq}=M_{q-p} for 0≤p≤q and zero otherwise, with vertical maps b and horizontal maps B. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Proposition 9.8.3
If A is a cyclic object, then HC_* ( A ) is naturally isomorphic to the cyclic homology of the mixed complex ( A , b , B )
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: If A is a cyclic object, then HC_* ( A ) is naturally isomorphic to the cyclic homology of the mixed complex ( A , b , B ) Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Comparison — changing the chain contraction gives the same mixed-complex cyclic homology
For a cyclic object A, replacing the chosen chain contraction by another one changes the associated operator B but still produces a mixed complex whose cyclic homology is naturally isomorphic to HC_*(A)
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For a cyclic object A, replacing the chosen chain contraction by another one changes the associated operator B but still produces a mixed complex whose cyclic homology is naturally isomorphic to HC_*(A) Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Application 9.8.4
For a cyclic k-module, quotienting the Hochschild complex by the degenerate subcomplex gives the normalized mixed complex; Dold–Kan implies it computes the same Hochschild homology.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For a cyclic k-module, quotienting the Hochschild complex by the degenerate subcomplex gives the normalized mixed complex; Dold–Kan implies it computes the same Hochschild homology. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Example 9.8.5
For the tensor algebra T(V), Connes’ operator on the degree-j Hochschild summand is the cyclic norm 1+σ+…+σ^{j-1}; hence HC_n(T)≅HC_n(k)⊕⊕_{j≥1}H_n(C_j;V^{⊗j}).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For the tensor algebra T(V), Connes’ operator on the degree-j Hochschild summand is the cyclic norm 1+σ+…+σ^{j-1}; hence HC_n(T)≅HC_n(k)⊕⊕_{j≥1}H_n(C_j;V^{⊗j}). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Named spectral sequence — Connes’ Spectral Sequence 9.8.6
Filtering Connes’ double complex by columns gives a spectral sequence E^1_{pq}=H_{q-p}(M)⇒HC_{p+q}(M), whose d^1 is induced by Connes’ operator B.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Filtering Connes’ double complex by columns gives a spectral sequence E^1_{pq}=H_{q-p}(M)⇒HC_{p+q}(M), whose d^1 is induced by Connes’ operator B. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Named result — SBI sequence for mixed complexes [numbered heading absent in extraction]
From 0→M_*→Tot(B)→Tot(B)[−2]→0 obtains the long exact SBI sequence for a mixed complex. The heading/number is absent in the extraction, but L10097 and L10101 explicitly call it the SBI sequence (9.8.7)
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: From 0→M_*→Tot(B)→Tot(B)[−2]→0 obtains the long exact SBI sequence for a mixed complex. The heading/number is absent in the extraction, but L10097 and L10101 explicitly call it the SBI sequence (9.8.7) Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Convention — notational consistency for Connes’ operator B
The operator B in a mixed complex induces the d¹ differential B:H_m(M)→H_{m+1}(M) in Connes’ spectral sequence; the notation is consistent with the horizontal maps in Connes’ double complex.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: The operator B in a mixed complex induces the d¹ differential B:H_m(M)→H_{m+1}(M) in Connes’ spectral sequence; the notation is consistent with the horizontal maps in Connes’ double complex. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Construction/comparison — Trivial Mixed Complexes 9.8.8
Any chain complex (C,b) is a mixed complex with B=0. Its cyclic homology is HC_n(C,b,0)=H_n(C)⊕H_{n-2}(C)⊕H_{n-4}(C)⊕….
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Any chain complex (C,b) is a mixed complex with B=0. Its cyclic homology is HC_n(C,b,0)=H_n(C)⊕H_{n-2}(C)⊕H_{n-4}(C)⊕…. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition 9.8.9
Defines the de Rham differential by d(r_0dr_1∧⋯∧dr_n)=dr_0∧⋯∧dr_n; d^2=0 gives the de Rham complex (Ω^*_R/k,d), and H^*_dR(R)=H^(Ω^_R/k) is algebraic de Rham cohomology
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Defines the de Rham differential by d(r_0dr_1∧⋯∧dr_n)=dr_0∧⋯∧dr_n; d^2=0 gives the de Rham complex (Ω^*_R/k,d), and H^*_dR(R)=H^(Ω^_R/k) is algebraic de Rham cohomology Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Lemma 9.8.10
Under the natural comparison Ω^n_{R/k}→HH_n(R,R), the de Rham differential d corresponds to Connes’ operator B: the square with d vertically and B on Hochschild homology commutes.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Under the natural comparison Ω^n_{R/k}→HH_n(R,R), the de Rham differential d corresponds to Connes’ operator B: the square with d vertically and B on Hochschild homology commutes. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Porism — B commutes with the signature-idempotent comparison
Porism Suppose that 1 / ( n + 1 ) ! ∈ R.The above proof shows that c B ( n ! ε_n ) ( r_0 ⊗ · · · ⊗ r_n ) = ( n + 1 ) ! ε_n+1 ( 1 ⊗ r_0 ⊗ · · · ⊗ r_n ) = n ! ε_n+1 B ( r_0 ⊗ · · · ⊗ r_n )
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Porism Suppose that 1 / ( n + 1 ) ! ∈ R.The above proof shows that c B ( n ! ε_n ) ( r_0 ⊗ · · · ⊗ r_n ) = ( n + 1 ) ! ε_n+1 ( 1 ⊗ r_0 ⊗ · · · ⊗ r_n ) = n ! ε_n+1 B ( r_0 ⊗ · · · ⊗ r_n ) Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Corollary 9.8.11
If R is smooth over k, Connes’ spectral sequence has E²_{0q}=Ωq_{R/k}/dΩ{q-1}{R/k} and E²{pq}=H^{q-p}_{dR}(R) for p>0.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: If R is smooth over k, Connes’ spectral sequence has E²_{0q}=Ωq_{R/k}/dΩ{q-1}{R/k} and E²{pq}=H^{q-p}_{dR}(R) for p>0. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Construction/comparison 9.8.12
For commutative R containing Q, the normalized antisymmetrization map e:R{⊗(n+1)}→Ωn_{R/k}, e(r_0⊗⋯⊗r_n)=r_0dr_1∧⋯∧dr_n/n!, satisfies eb=0 and identifies the top Hodge Hochschild piece with differential forms.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For commutative R containing Q, the normalized antisymmetrization map e:R{⊗(n+1)}→Ωn_{R/k}, e(r_0⊗⋯⊗r_n)=r_0dr_1∧⋯∧dr_n/n!, satisfies eb=0 and identifies the top Hodge Hochschild piece with differential forms. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Theorem 9.8.13
For a smooth commutative algebra R essentially of finite type over a characteristic-zero field, cyclic homology decomposes into differential forms modulo exact forms and lower de Rham cohomology groups in the same parity.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For a smooth commutative algebra R essentially of finite type over a characteristic-zero field, cyclic homology decomposes into differential forms modulo exact forms and lower de Rham cohomology groups in the same parity. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Construction — Hodge sub-double-complexes of Connes’ double complex
The Hodge idempotents on the normalized Hochschild complex are compatible with Connes’ operator B and therefore split Connes’ double complex into Hodge sub-double-complexes.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: The Hodge idempotents on the normalized Hochschild complex are compatible with Connes’ operator B and therefore split Connes’ double complex into Hodge sub-double-complexes. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition 9.8.14
Define HC_n^{(i)}(R) as the homology of the i-th Hodge sub-double-complex. These summands give the Hodge decomposition HC_n(R)=⊕_i HC_n^{(i)}(R) (with the stated degree bounds).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Define HC_n^{(i)}(R) as the homology of the i-th Hodge sub-double-complex. These summands give the Hodge decomposition HC_n(R)=⊕_i HC_n^{(i)}(R) (with the stated degree bounds). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Lemma 9.8.15
The Hodge idempotents and Connes operator satisfy e_{n+1}{(i+1)}B=Be_n{(i)} for all n and i≤n.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: The Hodge idempotents and Connes operator satisfy e_{n+1}{(i+1)}B=Be_n{(i)} for all n and i≤n. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Corollary — Crolr 9.816 [OCR-damaged label]
The top Hodge summand is HC_n(n)(R)=Ω_{R/k}n/dΩ_{R/k}^{n-1}; the extraction prints the label as 9.816, preserved in the source-unit field.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: The top Hodge summand is HC_n(n)(R)=Ω_{R/k}n/dΩ_{R/k}^{n-1}; the extraction prints the label as 9.816, preserved in the source-unit field. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Theorem 9.8.17
When Q⊂R, the SBI sequence decomposes as the direct sum of exact sequences on Hodge summands, with S lowering the Hodge index by one and B,I respecting the indicated pieces.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: When Q⊂R, the SBI sequence decomposes as the direct sum of exact sequences on Hodge summands, with S lowering the Hodge index by one and B,I respecting the indicated pieces. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Corollary 9.8.18
Over a characteristic-zero field, HC_n{(1)}(R)≅HH_n{(1)}(R,R)≅D_{n-1}(R/k) for n≥3; for n=2 there is the stated exact sequence relating D_1(R/k), HC_2^{(1)}(R), and H^0_{dR}(R/k).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Over a characteristic-zero field, HC_n{(1)}(R)≅HH_n{(1)}(R,R)≅D_{n-1}(R/k) for n≥3; for n=2 there is the stated exact sequence relating D_1(R/k), HC_2^{(1)}(R), and H^0_{dR}(R/k). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Comparison/remark — Remark 9.8.19
Extends Hochschild and cyclic homology to schemes via the corresponding sheaf complexes and hypercohomology; for smooth X over k with Q⊂k, the Hodge pieces identify with sheaf cohomology of Ω_X^i and with the Hodge filtration on de Rham cohomology
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Extends Hochschild and cyclic homology to schemes via the corresponding sheaf complexes and hypercohomology; for smooth X over k with Q⊂k, the Hodge pieces identify with sheaf cohomology of Ω_X^i and with the Hodge filtration on de Rham cohomology Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition/construction — weight grading on Hochschild and cyclic complexes of a graded algebra
For a graded k-algebra R, give r_0⊗…⊗r_p weight Σ|r_i|. The Hochschild and cyclic operators preserve this weight, so HH and HC decompose into weight summands.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For a graded k-algebra R, give r_0⊗…⊗r_p weight Σ|r_i|. The Hochschild and cyclic operators preserve this weight, so HH and HC decompose into weight summands. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Theorem — Goodwillie’s Theorem 9.9.1
Goodwillie’s theorem: on the nonzero weight-w part of cyclic homology of a graded algebra, the image of periodicity S is annihilated by w; if Q⊂k, S vanishes on every nonzero-weight summand.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Goodwillie’s theorem: on the nonzero weight-w part of cyclic homology of a graded algebra, the image of periodicity S is annihilated by w; if Q⊂k, S vanishes on every nonzero-weight summand. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Corollary 9.9.2
If R is positively graded and contains Q, periodic cyclic homology is insensitive to positive weights: HP_(R)≅HP_(R_0).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: If R is positively graded and contains Q, periodic cyclic homology is insensitive to positive weights: HP_(R)≅HP_(R_0). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Corollary 9.9.3
If R is commutative, positively graded, and contains Q, then algebraic de Rham cohomology satisfies H^*_{dR}(R)≅H^*_{dR}(R_0).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: If R is commutative, positively graded, and contains Q, then algebraic de Rham cohomology satisfies H^*_{dR}(R)≅H^*_{dR}(R_0). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Example 9.9.4
For T(V) with tensor-length grading, the explicit cyclic calculation gives HC_n(T)_w≅H_n(C_w;V^{⊗w}) for w>0; in characteristic zero these nonzero-weight groups vanish away from degree zero as stated.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For T(V) with tensor-length grading, the explicit cyclic calculation gives HC_n(T)_w≅H_n(C_w;V^{⊗w}) for w>0; in characteristic zero these nonzero-weight groups vanish away from degree zero as stated. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Lemma 9.9.5
Any natural map F:R^{⊗(m+1)}→C̄_{m+1}(R) satisfies FB=BF=0 and descends to a natural map C̄m(R)→C̄{m+1}(R).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Any natural map F:R^{⊗(m+1)}→C̄_{m+1}(R) satisfies FB=BF=0 and descends to a natural map C̄m(R)→C̄{m+1}(R). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Examples 9.9.6
For normalized Hochschild chains of a graded algebra, D multiplies a homogeneous tensor by its total weight and e is the natural degree-lowering operator satisfying eb+be=0; these operators enter the contraction used in Goodwillie’s theorem.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For normalized Hochschild chains of a graded algebra, D multiplies a homogeneous tensor by its total weight and e is the natural degree-lowering operator satisfying eb+be=0; these operators enter the contraction used in Goodwillie’s theorem. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Comparison/remark — Remark 9.9.7
The weight operator D:R→R is a derivation, and Goodwillie’s theorem extends from the grading derivation to any derivation acting on a k-algebra
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: The weight operator D:R→R is a derivation, and Goodwillie’s theorem extends from the grading derivation to any derivation acting on a k-algebra Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition — relative cyclic homology for an ideal
For an ideal I in a k-algebra R, let Z(R,I)=ker(Z(R)→Z(R/I)); define relative cyclic homology HC_(R,I)=HC_(Z(R,I)).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For an ideal I in a k-algebra R, let Z(R,I)=ker(Z(R)→Z(R/I)); define relative cyclic homology HC_(R,I)=HC_(Z(R,I)). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Construction — I-adic filtration by cyclic submodules
Filter Z_pR=R^{⊗(p+1)} by F_p^i generated by tensors I{i_0}⊗⋯⊗I{i_p} with i_0+⋯+i_p=i; these are cyclic submodules and give the I-adic filtration used in nilpotent invariance.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Filter Z_pR=R^{⊗(p+1)} by F_p^i generated by tensors I{i_0}⊗⋯⊗I{i_p} with i_0+⋯+i_p=i; these are cyclic submodules and give the I-adic filtration used in nilpotent invariance. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Proposition 9.9.8
Over a characteristic-zero field, if I^{m+1}=0 then S^i:HC_{p+2i}(R,I)→HC_p(R,I) is zero for every i≥m(p+1).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Over a characteristic-zero field, if I^{m+1}=0 then S^i:HC_{p+2i}(R,I)→HC_p(R,I) is zero for every i≥m(p+1). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Corollary 9.9.9
If I is a nilpotent ideal of R , then HP_* ( R , I ) = 0 and HP_* ( R ) ≅ HP_* ( R / I )
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: If I is a nilpotent ideal of R , then HP_* ( R , I ) = 0 and HP_* ( R ) ≅ HP_* ( R / I ) Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition/construction 9.9.10
For a DG-algebra (R,d), the internal differential together with the Hochschild differential makes the Hochschild chains a double complex; HH_*^DG(R) is the homology of its direct-sum total complex (with the stated reindexing convention for cohomological DG-algebras)
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For a DG-algebra (R,d), the internal differential together with the Hochschild differential makes the Hochschild chains a double complex; HH_*^DG(R) is the homology of its direct-sum total complex (with the stated reindexing convention for cohomological DG-algebras) Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Construction — cyclic object and mixed/Tsygan complexes for a DG-algebra after the exercise block
For a DG-algebra, the graded tensor powers form a cyclic object Z(R,d) in chain complexes after the sign correction; defines HC_^DG(R) from the total Tsygan bicomplex and, for positive grading, HP_^DG(R) from its periodic product total complex
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For a DG-algebra, the graded tensor powers form a cyclic object Z(R,d) in chain complexes after the sign correction; defines HC_^DG(R) from the total Tsygan bicomplex and, for positive grading, HP_^DG(R) from its periodic product total complex Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Proposition- 9.9.11
A quasi-isomorphism f:(R,d)→(R′,d′) of flat DG-algebras induces isomorphisms HH_{DG}(R)≅HH_^{DG}(R′) and HC_{DG}(R)≅HC_^{DG}(R′).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: A quasi-isomorphism f:(R,d)→(R′,d′) of flat DG-algebras induces isomorphisms HH_{DG}(R)≅HH_^{DG}(R′) and HC_{DG}(R)≅HC_^{DG}(R′). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Application/comparison — Vista 9.9.12
For a simply connected space X over a field k, the vista relates the Hochschild and cyclic homology of the singular cochain DG-algebra C^*(X) to the homology of the free loop space and its circle action.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For a simply connected space X over a field k, the vista relates the Hochschild and cyclic homology of the singular cochain DG-algebra C^*(X) to the homology of the free loop space and its circle action. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Convention — §9.10 fixes a characteristic-zero field k and associative unital k-algebra R
Fix a characteristic-zero field k and a unital associative k-algebra R; §9.10 relates Lie homology of gl_m(R) to cyclic homology of R.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Fix a characteristic-zero field k and a unital associative k-algebra R; §9.10 relates Lie homology of gl_m(R) to cyclic homology of R. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Construction — trace/cyclic map λ from Lie algebra chains to cyclic chains
The chain map λ:Λ{p+1}gl_m(R)→C_pλ(M_m(R)) sends x_0∧⋯∧x_p to the signed alternating sum of x_0⊗x_{σ(1)}⊗⋯⊗x_{σ(p)}; composing with Morita trace yields H_{p+1}(gl_m(R);k)→HC_p(R).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: The chain map λ:Λ{p+1}gl_m(R)→C_pλ(M_m(R)) sends x_0∧⋯∧x_p to the signed alternating sum of x_0⊗x_{σ(1)}⊗⋯⊗x_{σ(p)}; composing with Morita trace yields H_{p+1}(gl_m(R);k)→HC_p(R). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Lemma 9.10.1
λ is a morphism of chain complexes, inducing λ_*:H_{p+1}(gl_m(R);k)→HC_p(R), and it is compatible with the standard stabilization gl_m(R)↪gl_{m+1}(R) and the matrix trace maps.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: λ is a morphism of chain complexes, inducing λ_*:H_{p+1}(gl_m(R);k)→HC_p(R), and it is compatible with the standard stabilization gl_m(R)↪gl_{m+1}(R) and the matrix trace maps. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definition — Primitive Elements 9.10.2
An element x of a coalgebra H is primitive when Δ(x)=x⊗1+1⊗x. Primitive elements form a submodule Prim(H); in a graded coalgebra they form a graded submodule.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: An element x of a coalgebra H is primitive when Δ(x)=x⊗1+1⊗x. Primitive elements form a submodule Prim(H); in a graded coalgebra they form a graded submodule. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Proposition 9.10.3
The natural quotient map Λ^gl_m(R)→H_0(sl_m(k);Λ^gl_m(R)) to sl_m(k)-coinvariants is a quasi-isomorphism of chain complexes.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: The natural quotient map Λ^gl_m(R)→H_0(sl_m(k);Λ^gl_m(R)) to sl_m(k)-coinvariants is a quasi-isomorphism of chain complexes. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Corollary 9.10.4
For m≥n, the map λ_*:H_n(gl_m(R);k)→HC_{n-1}(R) is a split surjection.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For m≥n, the map λ_*:H_n(gl_m(R);k)→HC_{n-1}(R) is a split surjection. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Named calculation — Invariant Theory Calculation 9.10.5
Invariant theory identifies Λ^nV with V^{⊗n}⊗_{kΣ_n}sgn and, for m≥n, identifies the sl_m-invariants/coinvariants in gl_m(k)^{⊗n} with kΣ_n; this supplies the stable matrix-Lie calculation.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Invariant theory identifies Λ^nV with V^{⊗n}⊗_{kΣ_n}sgn and, for m≥n, identifies the sl_m-invariants/coinvariants in gl_m(k)^{⊗n} with kΣ_n; this supplies the stable matrix-Lie calculation. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Corollary 9.10.6
For every n, stabilization induces isomorphisms H_n(gl_n(R);k)≅H_n(gl_{n+1}(R);k)≅⋯≅H_n(gl(R);k).
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For every n, stabilization induces isomorphisms H_n(gl_n(R);k)≅H_n(gl_{n+1}(R);k)≅⋯≅H_n(gl(R);k). Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Comparison/result — Remark 9.10.7
For commutative R, the obstruction to improving stability to m=n−1 is the naturally split exact sequence H_n(gl_{n-1}(R);k)→H_n(gl_n(R);k)→Ω_{R/k}{n-1}/dΩ_{R/k}{n-2}→0.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: For commutative R, the obstruction to improving stability to m=n−1 is the naturally split exact sequence H_n(gl_{n-1}(R);k)→H_n(gl_n(R);k)→Ω_{R/k}{n-1}/dΩ_{R/k}{n-2}→0. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Definitions/construction 9.10.8
Introduces graded/DG coalgebra structure needed below: Λ^*(V) has the diagonal coproduct; a DG-coalgebra is a graded coalgebra whose counit and coproduct are chain maps; its homology is again a graded coalgebra, and primitive elements form a chain subcomplex
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Introduces graded/DG coalgebra structure needed below: Λ^*(V) has the diagonal coproduct; a DG-coalgebra is a graded coalgebra whose counit and coproduct are chain maps; its homology is again a graded coalgebra, and primitive elements form a chain subcomplex Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Proposition 9.10.9
The chain complex L_=H_0(sl(k);Λgl(R)) is a differential graded coalgebra, and its primitive subcomplex is the shifted cyclic complex C_{-1}(R)=R{⊗}/∼.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: The chain complex L_=H_0(sl(k);Λgl(R)) is a differential graded coalgebra, and its primitive subcomplex is the shifted cyclic complex C_{-1}(R)=R{⊗}/∼. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.
Theorem 9.10.10
Over a characteristic-zero field, Prim H_n(gl(R);k)≅HC_{n-1}(R) via the trace map, and H_*(gl(R);k) is the free graded-commutative Hopf algebra on the shifted cyclic homology of R.
Not formalized. none; partial adjacent tensor, Kähler, smoothness, Morita, coalgebra, Lie, group-homology, or homological infrastructure only — As of 2026-09-06, no checked A/P/H/T/open/indexed Lean declaration realizes the whole source bundle: Over a characteristic-zero field, Prim H_n(gl(R);k)≅HC_{n-1}(R) via the trace map, and H_*(gl(R);k) is the free graded-commutative Hopf algebra on the shifted cyclic homology of R. Under strict bundle semantics, adjacent prerequisites, a narrower hypothesis set, an analogous construction, or a proper subset do not own the row.