The chain complex obtained from $C_*$ by tensoring degreewise on the right with the $R$-module $M$: $(C_* \otimes M)_n = C_n \otimes M$ with the induced differential.
Instances For
Functoriality of tensorComplex in the chain complex argument: a chain map
$\varphi : C \to D$ tensored with the identity on $M$.
Instances For
Tensoring on the right with a fixed module $M$ preserves colimits; obtained by
transporting along the symmetry isomorphism with tensorLeft M.
In the downward $\mathbb{N}$-indexed complex shape, the successor n + 1 has
next = n.
In the downward $\mathbb{N}$-indexed complex shape, the successor n + 1 has
prev = n + 2.
The image of the cycles inclusion $Z_{n+1}(C) \hookrightarrow C_{n+1}$ under the functor $- \otimes M$ vanishes when followed by the differential of $C \otimes M$. Used to lift the cycles into the homology of the tensor complex.
The map $Z_{n+1}(C) \otimes M \to H_{n+1}(C \otimes M)$ obtained by lifting through the cycles of the tensor complex and then quotienting by boundaries. This is the building block of the UCT map $\alpha$.
Instances For
The composition of the canonical map into cycles with cyclesToHomologyTC vanishes;
i.e. boundaries are killed. This is the relation needed to descend cyclesToHomologyTC
along the cokernel description of homology.
The UCT map $\alpha : H_{n+1}(C) \otimes M \to H_{n+1}(C \otimes M)$, defined by descending the cycles-to-homology map through the cokernel presentation of $H_{n+1}(C)$ (valid because tensoring with $M$ preserves the relevant cokernel for free $C$).
Instances For
The defining property of uctAlpha: precomposing with the canonical projection from
cycles to homology recovers the basic cyclesToHomologyTC map. This is the universal
property of the cokernel description of homology.
The defining property of uctAlpha: precomposing with the canonical projection from
cycles to homology recovers the basic cyclesToHomologyTC map. This is the universal
property of the cokernel description of homology.
Naturality of the UCT map $\alpha$ in the chain complex variable: $\alpha$ commutes with the maps induced by a chain map $\varphi : C \to D$ between free chain complexes.
Packaged data of the Universal Coefficient Theorem in degree $n+1$: for every free chain complex $C_*$ over a PID $R$ and every $R$-module $M$, a natural split short exact sequence $$0 \to H_{n+1}(C_*) \otimes M \xrightarrow{\alpha} H_{n+1}(C_* \otimes M) \xrightarrow{\beta} \operatorname{Tor}_1^R(H_n(C_*), M) \to 0,$$ together with naturality of $\alpha$ and $\beta$ in $C_*$.
- α (C : ChainComplex (ModuleCat R) ℕ) : (∀ (i : ℕ), Module.Free R ↑(C.X i)) → (CategoryTheory.MonoidalCategoryStruct.tensorObj (HomologicalComplex.homology C (n + 1)) M ⟶ HomologicalComplex.homology (tensorComplex R C M) (n + 1))
- β (C : ChainComplex (ModuleCat R) ℕ) : (∀ (i : ℕ), Module.Free R ↑(C.X i)) → (HomologicalComplex.homology (tensorComplex R C M) (n + 1) ⟶ ((CategoryTheory.Tor (ModuleCat R) 1).obj (HomologicalComplex.homology C n)).obj M)
- zero (C : ChainComplex (ModuleCat R) ℕ) (hfree : ∀ (i : ℕ), Module.Free R ↑(C.X i)) : CategoryTheory.CategoryStruct.comp (self.α C hfree) (self.β C hfree) = 0
- shortExact (C : ChainComplex (ModuleCat R) ℕ) (hfree : ∀ (i : ℕ), Module.Free R ↑(C.X i)) : { X₁ := CategoryTheory.MonoidalCategoryStruct.tensorObj (HomologicalComplex.homology C (n + 1)) M, X₂ := HomologicalComplex.homology (tensorComplex R C M) (n + 1), X₃ := ((CategoryTheory.Tor (ModuleCat R) 1).obj (HomologicalComplex.homology C n)).obj M, f := self.α C hfree, g := self.β C hfree, zero := ⋯ }.ShortExact
- splitting (C : ChainComplex (ModuleCat R) ℕ) (hfree : ∀ (i : ℕ), Module.Free R ↑(C.X i)) : Nonempty { X₁ := CategoryTheory.MonoidalCategoryStruct.tensorObj (HomologicalComplex.homology C (n + 1)) M, X₂ := HomologicalComplex.homology (tensorComplex R C M) (n + 1), X₃ := ((CategoryTheory.Tor (ModuleCat R) 1).obj (HomologicalComplex.homology C n)).obj M, f := self.α C hfree, g := self.β C hfree, zero := ⋯ }.Splitting
- α_natural (C D : ChainComplex (ModuleCat R) ℕ) (hfreeC : ∀ (i : ℕ), Module.Free R ↑(C.X i)) (hfreeD : ∀ (i : ℕ), Module.Free R ↑(D.X i)) (φ : C ⟶ D) : CategoryTheory.CategoryStruct.comp (self.α C hfreeC) (HomologicalComplex.homologyMap (tensorComplexMap R φ M) (n + 1)) = CategoryTheory.CategoryStruct.comp (((CategoryTheory.MonoidalCategory.tensoringRight (ModuleCat R)).obj M).map (HomologicalComplex.homologyMap φ (n + 1))) (self.α D hfreeD)
- β_natural (C D : ChainComplex (ModuleCat R) ℕ) (hfreeC : ∀ (i : ℕ), Module.Free R ↑(C.X i)) (hfreeD : ∀ (i : ℕ), Module.Free R ↑(D.X i)) (φ : C ⟶ D) : CategoryTheory.CategoryStruct.comp (self.β C hfreeC) (((CategoryTheory.Tor (ModuleCat R) 1).map (HomologicalComplex.homologyMap φ n)).app M) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (tensorComplexMap R φ M) (n + 1)) (self.β D hfreeD)
Instances For
Tor as the homology of a projective resolution: for any projective resolution $P_\bullet$ of $M$, $$\operatorname{Tor}_1(X, M) \cong H_1(X \otimes P_\bullet).$$ Used to identify the connecting map of the UCT short exact sequence with the Tor term.
Instances For
In a projective resolution $P_\bullet \to M$, the composition $d_1 \circ \pi_0 = 0$: the augmentation kills the image of the first differential.
The short complex of chain complexes obtained by tensoring $C_*$ degreewise with the short exact sequence $0 \to P_1 \to P_0 \to M \to 0$ extracted from a projective resolution $P_\bullet$ of $M$.
Instances For
Over a PID, every projective resolution of an $R$-module can be chosen to have
length one, so $d_{2,1} = 0$. Used to upgrade the right end of resSES into a short
exact sequence.
Consequence of projRes_d_two_one_eq_zero: in a PID projective resolution the map
$P_1 \to P_0$ is a monomorphism, so $0 \to P_1 \to P_0 \to M \to 0$ is short exact.
For a free chain complex $C_*$ over a PID and a projective resolution $P_\bullet$ of
$M$, the short complex resSES R C M P obtained by tensoring with the length-one
resolution is short exact in every degree.
The natural identification of the homology in degree $n$ of the chain complex $C_* \otimes P_1$ with $\operatorname{Tor}_1^R(H_n(C_*), M)$, where $P_\bullet$ is a projective (in fact length-one) resolution of $M$.
Instances For
Naturality of torIdentification in the chain complex variable.
The UCT connecting map
$\beta : H_{n+1}(C_* \otimes M) \to \operatorname{Tor}_1^R(H_n(C_*), M)$,
built as the connecting homomorphism of resSES composed with torIdentification.
Instances For
Naturality of cyclesToHomologyTC in the module variable $M$: the construction
commutes with maps $f : M_1 \to M_2$. Used to relate $\alpha$ with the connecting map
of the tensored resolution.
The composition $\beta \circ \alpha = 0$, i.e. the maps in the UCT short complex form a complex.
For a free chain complex over a PID, the cokernel of $Z_n \hookrightarrow C_n$ — i.e. the boundary group $B_{n-1}(C)$ identified inside $C_{n-1}$ — is projective. This rests on the fact that submodules of free modules over a PID are free.
A splitting of the inclusion $Z_n(C) \hookrightarrow C_n$ for a free chain complex over a PID, obtained from the short exact sequence $0 \to Z_n \to C_n \to \mathrm{cok}(Z_n \hookrightarrow C_n) \to 0$ together with projectivity of the cokernel.
Instances For
Noncomputable variant of iCycles_splitMono: the same splitting of
$Z_n(C) \hookrightarrow C_n$, packaged for use in contexts where computability is not
required.
Instances For
A retraction (split-mono witness) of the UCT map $\alpha_n$, constructed from a splitting of $Z_{n+1}(C) \hookrightarrow C_{n+1}$. This is the key ingredient making the UCT short exact sequence split.
Instances For
The identification of $\mathrm{Tor}_1(H_n(C), M)$ with a kernel of an induced homology map is an isomorphism on the relevant kernel, providing the bridge between the abstract Tor functor and the concrete connecting homomorphism appearing in the UCT.
The UCT map $\beta_n : H_{n+1}(C \otimes M) \to \mathrm{Tor}_1(H_n(C), M)$ is an epimorphism. This is the surjectivity claim in the UCT short exact sequence.
Exactness of the UCT short complex at its middle term: the image of $\alpha_n$ equals the kernel of $\beta_n$, giving the exact middle of the universal coefficient sequence.
The UCT short exact sequence splits: a (non-natural) splitting of the sequence
$0 \to H_n(C) \otimes M \to H_n(C \otimes M) \to \mathrm{Tor}_1(H_{n-1}(C), M) \to 0$,
obtained from the retraction uctAlpha_retraction together with exactness.
The UCT sequence is short exact: combining injectivity of $\alpha_n$, exactness in
the middle, and surjectivity of $\beta_n$ into a single ShortExact package.
Naturality of the UCT connecting map $\beta_n$ in the chain complex variable: a chain map $\varphi : C \to D$ between free complexes induces a commuting square between the UCT $\beta$'s for $C$ and $D$.
Theorem 24.1 (Universal Coefficient Theorem). For a PID $R$, a chain complex of free $R$-modules $C$, and an $R$-module $M$, there is a natural split short exact sequence $$0 \to H_n(C) \otimes_R M \to H_n(C \otimes_R M) \to \mathrm{Tor}_1^R(H_{n-1}(C), M) \to 0.$$ This bundles the maps $\alpha_n, \beta_n$, exactness, splitting, and naturality.