The tensor product of two chain complexes of $R$-modules, with the Leibniz differential $d(x \otimes y) = dx \otimes y + (-1)^{|x|} x \otimes dy$. This is the algebraic side of the Künneth formula.
Instances For
The canonical inclusion of the bidegree $(p,q)$ summand $C_p \otimes D_q$ into the total complex $(C \otimes D)_n$ for $p + q = n$.
Instances For
The index set of pairs $(p, q)$ of nonnegative integers with $p + q = n$, used to index the bidegree summands of the total complex of a tensor product.
Instances For
Every $R$-module $M$ admits a projective (in particular free) resolution; this is the existence input needed to define $\mathrm{Tor}$.
The Künneth decomposition isomorphism at the level of homology: for chain complexes $C, D$ of $R$-modules over a PID $R$ with $C$ free, the homology of the tensor product splits as a direct sum $$H_n(C \otimes D) \;\cong\; \bigoplus_{p + q = n} H_p(C) \otimes H_q(D) \;\oplus\; \bigoplus_{p + q = n - 1} \mathrm{Tor}_1(H_p(C), H_q(D)).$$
Instances For
Theorem 25.2 (Algebraic Künneth formula). Over a PID $R$, with $C$ a chain complex of free $R$-modules, there is a natural split short exact sequence $$0 \to \bigoplus_{p+q=n} H_p(C) \otimes H_q(D) \to H_n(C \otimes D) \to \bigoplus_{p+q=n-1} \mathrm{Tor}_1(H_p(C), H_q(D)) \to 0.$$
Naturality of the algebraic Künneth short exact sequence with respect to chain maps $f : C \to C'$ and $g : D \to D'$: the induced map on $H_n(C \otimes D)$ extends to a morphism of the corresponding short exact sequences.
The category $\mathrm{ModuleCat}\,R$ of $R$-modules has projective resolutions; an instance reused throughout the Tor / UCT / Künneth development.
Definition 25.7 ($\mathcal{M}$-epi). A natural transformation $\eta : F \to G$ between functors $\mathcal{C} \to \mathrm{Ab}$ is $\mathcal{M}$-epi if its component $\eta_M : F(M) \to G(M)$ is surjective for every $M$ in the family of models $\mathcal{M} \subseteq \mathcal{C}$.
Instances For
Definition 25.7 ($\mathcal{M}$-exact). A sequence $G' \xrightarrow{\eta} G \xrightarrow{\psi} G''$ of functors $\mathcal{C} \to \mathrm{Ab}$ is $\mathcal{M}$-exact if, on every model $M \in \mathcal{M}$, the composite is zero and the image of $\eta_M$ equals the kernel of $\psi_M$.
Instances For
The free-abelian-coyoneda functor at a model $M$: the composite of $\mathrm{Hom}(M, -)$ with the free abelian group functor, sending $X$ to $\mathbb{Z}\langle \mathrm{Hom}(M, X) \rangle$. This is the basic building block of an $\mathcal{M}$-free functor.
Instances For
Definition 25.4 ($\mathcal{M}$-free). A functor $F : \mathcal{C} \to \mathrm{Ab}$ is $\mathcal{M}$-free if it is naturally isomorphic to a direct sum of free-abelian-coyoneda functors indexed by some family of models in $\mathcal{M}$. Such functors lift against $\mathcal{M}$-epis.
Instances For
The natural transformation $\mathbb{Z}\langle \mathrm{Hom}(M, -) \rangle \to G'$ classified by an element $c \in G'(M)$: it sends a morphism $\varphi : M \to X$ to $G'(\varphi)(c)$. This is the universal property of the free-abelian-coyoneda functor.
Instances For
The free-abelian-coyoneda functor sends $\mathrm{id}_M$ to the generator $\mathrm{id}_M \in \mathbb{Z}\langle \mathrm{Hom}(M, M) \rangle$, and sends $\varphi$ applied to this generator to $\varphi \in \mathbb{Z}\langle \mathrm{Hom}(M, X) \rangle$.
Lifting property of free-abelian-coyoneda functors: any natural transformation $f : \mathbb{Z}\langle \mathrm{Hom}(M, -)\rangle \to G$ lifts through an $\mathcal{M}$-epi $\eta : G' \to G$, provided $M \in \mathcal{M}$.
Lifting property of $\mathcal{M}$-free functors: any natural transformation
$f : F \to G$ from an $\mathcal{M}$-free $F$ lifts through an $\mathcal{M}$-epi
$\eta : G' \to G$. Generalises freeAbelianCoyoneda_hasLiftingProperty to arbitrary
direct sums of corepresentables.
Exact-sequence version of the lifting property for free-abelian-coyoneda functors: in an $\mathcal{M}$-exact sequence $G' \xrightarrow{\eta} G \xrightarrow{\psi} G''$, any natural transformation $f : \mathbb{Z}\langle \mathrm{Hom}(M, -) \rangle \to G$ killed by $\psi$ factors through $\eta$.
Exact-sequence lifting property for $\mathcal{M}$-free functors: any natural transformation $f : F \to G$ from an $\mathcal{M}$-free $F$ that is killed by $\psi$ factors through $\eta$, given $\eta, \psi$ form an $\mathcal{M}$-exact sequence.
An augmented chain-complex-valued functor: a functor $\mathcal{C} \to \mathrm{Ch}_*$ together with an augmentation $F_0 \to T$ to a target functor $T : \mathcal{C} \to \mathrm{Ab}$. This is the input data on which the acyclic models theorem operates.
- chainFun : CategoryTheory.Functor 𝒞 (HomologicalComplex AddCommGrpCat (ComplexShape.down ℕ))
- target : CategoryTheory.Functor 𝒞 AddCommGrpCat
- augmentation : self.chainFun.comp (HomologicalComplex.eval AddCommGrpCat (ComplexShape.down ℕ) 0) ⟶ self.target
Instances For
The degree-$n$ component of an augmented chain-complex functor as a functor $\mathcal{C} \to \mathrm{Ab}$, obtained by composing with the evaluation functor at $n$.
Instances For
An augmented chain-complex functor is $\mathcal{M}$-exact (acyclic on models) if on each model $M \in \mathcal{M}$ the augmented chain complex is exact: higher exactness in positive degrees, surjectivity of the augmentation, and exactness at degree 0. This is the acyclicity hypothesis in the acyclic models theorem.
Instances For
The natural transformation $F_i \Rightarrow F_j$ induced by the differential $d_{ij}$ of the underlying chain complex, viewed in the functor category.
Instances For
The augmentation of an $\mathcal{M}$-exact augmented chain-complex functor is an
$\mathcal{M}$-epi: extraction of the surjectivity clause from IsMExactAugmented.
Consecutive differentials of an $\mathcal{M}$-exact augmented functor form an $\mathcal{M}$-exact pair in positive degrees: extraction of the higher-exactness clause.
The differential $d_{1,0}$ and the augmentation form an $\mathcal{M}$-exact pair: the
zero-degree exactness clause of IsMExactAugmented.
The covering condition: a chain map $\varphi : F \to G$ between augmented chain-complex functors covers a natural transformation $\theta : F_{\mathrm{aug}} \to G_{\mathrm{aug}}$ of targets iff the obvious square commutes on every object $X$.
Instances For
A natural transformation between functors valued in chain complexes is a natural
chain-homotopy equivalence if there is a natural inverse and, on every object, the pair
$(\varphi_X, \psi_X)$ assembles into a HomotopyEquiv.
Instances For
Two natural transformations of chain-complex functors are objectwise chain homotopic if, for every $X \in \mathcal{C}$, the components $\Phi_X$ and $\Psi_X$ are chain homotopic as ordinary chain maps.
Instances For
The shape of homotopy data used in the acyclic models uniqueness proof: a family of
natural transformations $s_n : F_n \to G_{n+1}$, evaluated at $X$ and re-indexed to match
the ComplexShape.down ℕ relation.
Instances For
The objectwise chain homotopy between $\Phi_1$ and $\Phi_2$ associated to a family of natural transformations $s_n : F_n \to G_{n+1}$ satisfying the chain-homotopy identity $\Phi_1 - \Phi_2 = d \circ s + s \circ d$ as a null-homotopic map.
Instances For
Acyclic models yields a natural chain-homotopy equivalence: if $F$ and $G$ are both $\mathcal{M}$-free and $\mathcal{M}$-exact on a common family of models, then any natural transformation $\varphi : F \to G$ covering an isomorphism of augmentations is a natural chain-homotopy equivalence.
Acyclic Models — existence. Given an $\mathcal{M}$-free augmented chain functor $F$ and an $\mathcal{M}$-exact augmented chain functor $G$, any natural transformation $\theta$ between their targets is covered by a chain map $F \to G$. The proof builds the chain map degree-by-degree using the lifting properties of $\mathcal{M}$-free functors.
Acyclic Models — uniqueness. Any two natural chain maps $F \to G$ covering the same augmentation morphism are objectwise chain homotopic. The proof again proceeds by induction, using the exact lifting property of $\mathcal{M}$-free functors to build the chain homotopy degree-by-degree.
Theorem 25.11 (Acyclic Models). Combining existence and uniqueness: for an $\mathcal{M}$-free augmented functor $F$ and an $\mathcal{M}$-exact augmented functor $G$, any natural transformation between their targets is covered by a chain map that is unique up to objectwise chain homotopy.
The singular chain complex of a topological space with coefficients in $R$ is free in each degree, since it is the free $R$-module on the set of singular simplices.
Bundling of homology / tensor-product instances for the singular chain complexes of two spaces $X, Y$: each has homology in every degree, their tensor product exists, and the tensor product has homology in every degree.
The Künneth tensor map (cross product on homology with $R$ coefficients): $\bigoplus_{p+q=n} H_p(X; R) \otimes H_q(Y; R) \to H_n(X \times Y; R)$, obtained as the composite of the algebraic Künneth map and the Eilenberg–Zilber isomorphism.
Instances For
The Künneth boundary map: $H_n(X \times Y; R) \to \bigoplus_{p+q=n-1} \mathrm{Tor}_1^R(H_p(X; R), H_q(Y; R))$, obtained from the Eilenberg–Zilber map and the algebraic Künneth connecting morphism.
Instances For
The composite of the Künneth tensor map and the Künneth boundary map vanishes, witnessing the chain-complex structure of the topological Künneth sequence.
The Künneth short complex of $R$-modules: $\bigoplus_{p+q=n} H_p(X) \otimes H_q(Y) \to H_n(X \times Y) \to \bigoplus_{p+q=n-1} \mathrm{Tor}_1(H_p(X), H_q(Y))$.
Instances For
The Künneth short complex is short exact: the topological Künneth sequence is exact in the middle, with the Künneth map injective and the boundary map surjective.
The topological Künneth sequence splits (non-naturally): a splitting of the short exact sequence is given by the corresponding algebraic Künneth splitting transported through the Eilenberg–Zilber isomorphism.
Naturality of the topological Künneth sequence: continuous maps $f : X \to X'$, $g : Y \to Y'$ induce a morphism of the corresponding Künneth short complexes whose middle component equals the induced map on $H_n(X \times Y) \to H_n(X' \times Y')$.
Theorem 25.15 (Topological Künneth formula). For a PID $R$ and spaces $X, Y$, there is a natural split short exact sequence $$0 \to \bigoplus_{p+q=n} H_p(X; R) \otimes_R H_q(Y; R) \to H_n(X \times Y; R) \to \bigoplus_{p+q=n-1} \mathrm{Tor}_1^R(H_p(X; R), H_q(Y; R)) \to 0.$$ A consequence of the Eilenberg–Zilber theorem and the algebraic Künneth formula.