noncomputable def ExtR (R : Type u_1) [CommRing R] (n : ℕ) (M N : ModuleCat R) : ModuleCat R

Definition 27.2. The Ext-functor $\mathrm{Ext}^n_R(M, N)$ at level $n$, packaged as a ModuleCat R. Concretely, this is the $n$-th cohomology of $\mathrm{Hom}_R(F_*, N)$ for any free resolution $0 \leftarrow M \leftarrow F_0 \leftarrow F_1 \leftarrow \cdots$, realised here via the derived functor Ext on the abelian category of R-modules.

theorem UniversalCoefficientTheorem.splitting_from_biprod_iso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] {A B D : C} [CategoryTheory.Limits.HasBinaryBiproduct A D] (φ : A ⊞ D ≅ B) : ∃ (S : CategoryTheory.ShortComplex C), S.X₁ = A ∧ S.X₂ = B ∧ S.X₃ = D ∧ S.ShortExact ∧ Nonempty S.Splitting

From an iso $A \oplus D \cong B$, manufacture a short exact sequence $0 \to A \to B \to D \to 0$ together with a splitting. Used to package the UCT biproduct decomposition as the split short exact sequence appearing in Theorem 27.1.

noncomputable def UniversalCoefficientTheorem.uct_iso (R : Type) [CommRing R] [IsPrincipalIdealRing R] (C : ChainComplex (ModuleCat R) ℕ) (N : ModuleCat R) (hfree : ∀ (i : ℕ), Module.Free R ↑(C.X i)) (n : ℕ) : ((Ext R (ModuleCat R) 1).obj (Opposite.op (HomologicalComplex.homology C (n - 1)))).obj N ⊞ ((Ext R (ModuleCat R) 0).obj (Opposite.op (HomologicalComplex.homology C n))).obj N ≅ HomologicalComplex.homology (C.linearYonedaObj R N) n

The underlying biproduct isomorphism behind the UCT: for a free chain complex $C_*$ over a PID $R$ and a coefficient module $N$, there is an iso $\mathrm{Ext}^1(H_{n-1}, N) \oplus \mathrm{Hom}(H_n, N) \cong H^n(\mathrm{Hom}(C_*, N))$. This is the unsplit form of Theorem 27.1, from which the split short exact sequence is extracted by splitting_from_biprod_iso.

theorem UniversalCoefficientTheorem.cohomologyUCT (R : Type) [CommRing R] [IsPrincipalIdealRing R] (C : ChainComplex (ModuleCat R) ℕ) (N : ModuleCat R) (hfree : ∀ (i : ℕ), Module.Free R ↑(C.X i)) (n : ℕ) : ∃ (S : CategoryTheory.ShortComplex (ModuleCat R)), S.X₁ = ((Ext R (ModuleCat R) 1).obj (Opposite.op (HomologicalComplex.homology C (n - 1)))).obj N ∧ S.X₂ = HomologicalComplex.homology (C.linearYonedaObj R N) n ∧ S.X₃ = ((Ext R (ModuleCat R) 0).obj (Opposite.op (HomologicalComplex.homology C n))).obj N ∧ S.ShortExact ∧ Nonempty S.Splitting

Theorem 27.1 (Mixed-variance Universal Coefficient Theorem). For a chain complex $C_*$ of free $R$-modules over a PID $R$ and any coefficient module $N$, there is a (non-naturally) split short exact sequence $$0 \to \mathrm{Ext}^1_R(H_{n-1}(C_*), N) \to H^n(\mathrm{Hom}_R(C_*, N)) \to \mathrm{Hom}_R(H_n(C_*), N) \to 0.$$

def UniversalCoefficientTheorem.uctInducedChainMap (R : Type) [CommRing R] {C D : ChainComplex (ModuleCat R) ℕ} (N : ModuleCat R) (φ : C ⟶ D) : D.linearYonedaObj R N ⟶ C.linearYonedaObj R N

The cochain map $\mathrm{Hom}(D_*, N) \to \mathrm{Hom}(C_*, N)$ induced by a chain map $\varphi : C_* \to D_*$, used to phrase naturality of the UCT in the chain-complex variable.

def UniversalCoefficientTheorem.uctInducedCoefficientMap (R : Type) [CommRing R] (C : ChainComplex (ModuleCat R) ℕ) {N N' : ModuleCat R} (f : N ⟶ N') : C.linearYonedaObj R N ⟶ C.linearYonedaObj R N'

The cochain map $\mathrm{Hom}(C_*, N) \to \mathrm{Hom}(C_*, N')$ induced by a coefficient map $f : N \to N'$, used to phrase naturality of the UCT in the coefficient variable.

theorem UniversalCoefficientTheorem.uct_iso_natural_chain (R : Type) [CommRing R] [IsPrincipalIdealRing R] (C D : ChainComplex (ModuleCat R) ℕ) (N : ModuleCat R) (hfreeC : ∀ (i : ℕ), Module.Free R ↑(C.X i)) (hfreeD : ∀ (i : ℕ), Module.Free R ↑(D.X i)) (φ : C ⟶ D) (n : ℕ) : CategoryTheory.CategoryStruct.comp (uct_iso R D N hfreeD n).hom (HomologicalComplex.homologyMap (uctInducedChainMap R N φ) n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (((Ext R (ModuleCat R) 1).map (HomologicalComplex.homologyMap φ (n - 1)).op).app N) (((Ext R (ModuleCat R) 0).map (HomologicalComplex.homologyMap φ n).op).app N)) (uct_iso R C N hfreeC n).hom

Naturality of the UCT biproduct isomorphism in the chain-complex variable: a chain map $\varphi : C_* \to D_*$ induces compatible maps on $\mathrm{Ext}^1(H_{n-1}(-), N)$, $\mathrm{Hom}(H_n(-), N)$, and $H^n(\mathrm{Hom}(-, N))$, making the obvious square commute.

theorem UniversalCoefficientTheorem.uct_iso_natural_coeff (R : Type) [CommRing R] [IsPrincipalIdealRing R] (C : ChainComplex (ModuleCat R) ℕ) (N N' : ModuleCat R) (hfree : ∀ (i : ℕ), Module.Free R ↑(C.X i)) (f : N ⟶ N') (n : ℕ) : CategoryTheory.CategoryStruct.comp (uct_iso R C N hfree n).hom (HomologicalComplex.homologyMap (uctInducedCoefficientMap R C f) n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (((Ext R (ModuleCat R) 1).obj (Opposite.op (HomologicalComplex.homology C (n - 1)))).map f) (((Ext R (ModuleCat R) 0).obj (Opposite.op (HomologicalComplex.homology C n))).map f)) (uct_iso R C N' hfree n).hom

Naturality of the UCT biproduct isomorphism in the coefficient variable: a coefficient map $f : N \to N'$ induces compatible maps on $\mathrm{Ext}^1(H_{n-1}, -)$, $\mathrm{Hom}(H_n, -)$, and $H^n(\mathrm{Hom}(C_*, -))$, making the obvious square commute.

noncomputable def SingularCohomology.capProduct (R : Type) [CommRing R] (X : TopCat) (n p : ℕ) : ↑(singularCohomology R X (ModuleCat.of R R) p) →ₗ[R] ↑(singularHomologyModule R X n) →ₗ[R] ↑(singularHomologyModule R X (n - p))

The cap product $\cap : H^p(X; R) \otimes H_n(X; R) \to H_{n-p}(X; R)$ expressed as the curried $R$-bilinear map $H^p(X; R) \to (H_n(X; R) \to H_{n-p}(X; R))$. Used downstream for capping with the fundamental class in Poincaré duality.

@[reducible, inline]

noncomputable abbrev SingularCohomology.singularChains (R : Type) [CommRing R] (X : TopCat) : ChainComplex (ModuleCat R) ℕ

The singular chain complex $S_*(X; R)$ of a topological space $X$ with coefficients in $R$, packaged as a chain complex of R-modules indexed by ℕ.

theorem SingularCohomology.singularChains_free (R : Type) [CommRing R] (X : TopCat) (i : ℕ) : Module.Free R ↑((singularChains R X).X i)

Each module of singular chains $S_i(X; R)$ is free over $R$ (with basis the singular $i$-simplices). This is the hypothesis needed to apply the UCT (cohomologyUCT) to the singular chain complex.