def SingularCohomology.SingularCochain (n : ℕ) (X : Type u_1) [TopologicalSpace X] (N : Type u_2) [AddCommGroup N] : Type (max u_1 u_2)

Definition 26.3. A singular $n$-cochain on $X$ with values in an abelian group $N$ is a function $\operatorname{Sin}_n(X) \to N$.

@[implicit_reducible]

instance SingularCohomology.instAddCommGroupSingularCochain (n : ℕ) (X : Type u_1) [TopologicalSpace X] (N : Type u_2) [AddCommGroup N] : AddCommGroup (SingularCochain n X N)

Pointwise addition makes singular $n$-cochains into an abelian group.

noncomputable def SingularCohomology.singularCohomology (R : Type) [CommRing R] (X : TopCat) (G : ModuleCat R) (n : ℕ) : ModuleCat R

Definition 26.5. The $n$th singular cohomology $H^n(X; G) = H^n(\operatorname{Hom}_R(S_*(X; R), G))$ of $X$ with coefficients in an $R$-module $G$.

noncomputable def SingularCohomology.singularCochainComplex (R : Type) [CommRing R] (X : TopCat) (G : ModuleCat R) : CochainComplex (ModuleCat R) ℕ

The singular cochain complex $S^*(X; G) = \operatorname{Hom}_R(S_*(X; R), G)$, the underlying cochain complex computing singular cohomology.

noncomputable def SingularCohomology.restrictionCochainMap (R : Type) [CommRing R] (G : ModuleCat R) {X A : TopCat} (i : A ⟶ X) : singularCochainComplex R X G ⟶ singularCochainComplex R A G

The restriction map of cochain complexes $S^*(X; G) \to S^*(A; G)$ induced by an inclusion $A \hookrightarrow X$.

noncomputable def SingularCohomology.relativeSingularCochainComplex (R : Type) [CommRing R] (G : ModuleCat R) {X A : TopCat} (i : A ⟶ X) : CochainComplex (ModuleCat R) ℕ

Definition 26.8. The relative singular cochain complex $S^n(X, A; N) = \ker(S^n(X; N) \to S^n(A; N))$.

noncomputable def SingularCohomology.relativeSingularCohomology (R : Type) [CommRing R] (X A : TopCat) (i : A ⟶ X) (G : ModuleCat R) (n : ℕ) : ModuleCat R

Definition 26.8 (cohomology version). Relative singular cohomology $H^n(X, A; N) = H^n(S^*(X, A; N))$.

@[reducible, inline]

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

The $n$th singular homology module $H_n(X; R)$, as an object of ModuleCat R.

@[reducible, inline]

abbrev SingularCohomology.singularHomologyFamily (R : Type) [CommRing R] (X : TopCat) : ℕ → Type

The graded family of underlying types $n \mapsto H_n(X; R)$.

@[reducible, inline]

abbrev SingularCohomology.totalSingularHomology (R : Type) [CommRing R] (X : TopCat) : Type

The total singular homology $H_*(X; R) = \bigoplus_n H_n(X; R)$ as a graded $R$-module.

def SingularCohomology.TopCat.diag (X : TopCat) : X ⟶ TopCat.of (↑X × ↑X)

The diagonal $X \to X \times X$, $x \mapsto (x, x)$.

noncomputable def SingularCohomology.diagHomology (R : Type) [CommRing R] (X : TopCat) (n : ℕ) : singularHomologyFamily R X n →ₗ[R] singularHomologyFamily R (TopCat.of (↑X × ↑X)) n

The map on $n$th homology induced by the diagonal $X \to X \times X$.

noncomputable def SingularCohomology.totalDiagMap (R : Type) [CommRing R] (X : TopCat) : totalSingularHomology R X →ₗ[R] totalSingularHomology R (TopCat.of (↑X × ↑X))

The total map on graded homology $H_*(X) \to H_*(X \times X)$ induced by the diagonal, half of the comultiplication on the graded coalgebra $H_*(X; R)$ of Corollary 26.2.

noncomputable def homologyCrossProductDeg (R : Type) [CommRing R] (X Y : TopCat) (p q : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (SingularCohomology.singularHomologyModule R X p) (SingularCohomology.singularHomologyModule R Y q) ⟶ SingularCohomology.singularHomologyModule R (TopCat.of (↑X × ↑Y)) (p + q)

The homology cross product in a fixed bidegree: $H_p(X) \otimes_R H_q(Y) \to H_{p+q}(X \times Y)$.

noncomputable def kunnethIso (R : Type) [CommRing R] [IsPrincipalIdealRing R] (X Y : TopCat) (hfreeX : ∀ (n : ℕ), Module.Free R (SingularCohomology.singularHomologyFamily R X n)) (hfreeY : ∀ (n : ℕ), Module.Free R (SingularCohomology.singularHomologyFamily R Y n)) : TensorProduct R (SingularCohomology.totalSingularHomology R X) (SingularCohomology.totalSingularHomology R Y) ≃ₗ[R] SingularCohomology.totalSingularHomology R (TopCat.of (↑X × ↑Y))

Künneth theorem (Theorem 25.15). When $R$ is a PID and $H_*(X; R), H_*(Y; R)$ are free over $R$, the cross product is an isomorphism $H_*(X; R) \otimes_R H_*(Y; R) \xrightarrow{\sim} H_*(X \times Y; R)$.

noncomputable def toTerminal (X : TopCat) : X ⟶ TopCat.of PUnit.{1}

The unique continuous map $X \to \{\ast\}$ to the one-point space.

noncomputable def h0MapToTerminal (R : Type) [CommRing R] (X : TopCat) : SingularCohomology.singularHomologyModule R X 0 ⟶ SingularCohomology.singularHomologyModule R (TopCat.of PUnit.{1}) 0

The map $H_0(X; R) \to H_0(\{\ast\}; R)$ induced by collapsing $X$ to a point.

noncomputable def h0TerminalIsoCoproduct (R : Type) [CommRing R] : SingularCohomology.singularHomologyModule R (TopCat.of PUnit.{1}) 0 ≅ ∐ fun (x : ↑(TopCat.of PUnit.{1})) => ModuleCat.of R R

The zeroth homology of the singleton, identified with a coproduct of one copy of $R$.

noncomputable def coproductPUnitFold (R : Type) [CommRing R] : (∐ fun (x : ↑(TopCat.of PUnit.{1})) => ModuleCat.of R R) ⟶ ModuleCat.of R R

The fold map collapsing a one-element coproduct of $R$ to $R$.

noncomputable def augmentationH0 (R : Type) [CommRing R] (X : TopCat) : SingularCohomology.singularHomologyModule R X 0 ⟶ ModuleCat.of R R

The augmentation $H_0(X; R) \to R$, obtained by collapsing $X$ to a point.

noncomputable def augmentation (R : Type) [CommRing R] (X : TopCat) : SingularCohomology.totalSingularHomology R X →ₗ[R] R

The counit $\varepsilon : H_*(X; R) \to R$ for the graded coalgebra structure of Corollary 26.2: project to the degree-$0$ component and then augment.

theorem kunneth_coassoc (R : Type) [CommRing R] [IsPrincipalIdealRing R] (X : TopCat) (hfree : ∀ (n : ℕ), Module.Free R (SingularCohomology.singularHomologyFamily R X n)) : have comul := ↑(kunnethIso R X X hfree hfree).symm ∘ₗ SingularCohomology.totalDiagMap R X; ↑(TensorProduct.assoc R (SingularCohomology.totalSingularHomology R X) (SingularCohomology.totalSingularHomology R X) (SingularCohomology.totalSingularHomology R X)) ∘ₗ LinearMap.rTensor (SingularCohomology.totalSingularHomology R X) comul ∘ₗ comul = LinearMap.lTensor (SingularCohomology.totalSingularHomology R X) comul ∘ₗ comul

Coassociativity of the comultiplication on $H_*(X; R)$: $(\Delta \otimes 1) \circ \Delta = (1 \otimes \Delta) \circ \Delta$.

theorem kunneth_rTensor_counit (R : Type) [CommRing R] [IsPrincipalIdealRing R] (X : TopCat) (hfree : ∀ (n : ℕ), Module.Free R (SingularCohomology.singularHomologyFamily R X n)) : have comul := ↑(kunnethIso R X X hfree hfree).symm ∘ₗ SingularCohomology.totalDiagMap R X; LinearMap.rTensor (SingularCohomology.totalSingularHomology R X) (augmentation R X) ∘ₗ comul = (TensorProduct.mk R R (SingularCohomology.totalSingularHomology R X)) 1

Right counit law for the graded coalgebra structure on $H_*(X; R)$.

theorem kunneth_lTensor_counit (R : Type) [CommRing R] [IsPrincipalIdealRing R] (X : TopCat) (hfree : ∀ (n : ℕ), Module.Free R (SingularCohomology.singularHomologyFamily R X n)) : have comul := ↑(kunnethIso R X X hfree hfree).symm ∘ₗ SingularCohomology.totalDiagMap R X; LinearMap.lTensor (SingularCohomology.totalSingularHomology R X) (augmentation R X) ∘ₗ comul = (TensorProduct.mk R (SingularCohomology.totalSingularHomology R X) R).flip 1

Left counit law for the graded coalgebra structure on $H_*(X; R)$.

theorem kunneth_graded (R : Type) [CommRing R] [IsPrincipalIdealRing R] (X : TopCat) (hfree : ∀ (n : ℕ), Module.Free R (SingularCohomology.singularHomologyFamily R X n)) (n : ℕ) (x : SingularCohomology.singularHomologyFamily R X n) (p q : ℕ) (hpq : p + q ≠ n) : have comul := ↑(kunnethIso R X X hfree hfree).symm ∘ₗ SingularCohomology.totalDiagMap R X; (DirectSum.component R (ℕ × ℕ) (fun (pq : ℕ × ℕ) => TensorProduct R (SingularCohomology.singularHomologyFamily R X pq.1) (SingularCohomology.singularHomologyFamily R X pq.2)) (p, q)) ((TensorProduct.directSum R R (SingularCohomology.singularHomologyFamily R X) (SingularCohomology.singularHomologyFamily R X)) (comul ((DirectSum.lof R ℕ (SingularCohomology.singularHomologyFamily R X) n) x))) = 0

Gradedness of the comultiplication: for $x \in H_n(X)$, the $H_p \otimes H_q$ component of $\Delta(x)$ vanishes whenever $p + q \ne n$.

theorem kunneth_gradedComm (R : Type) [CommRing R] [IsPrincipalIdealRing R] (X : TopCat) (hfree : ∀ (n : ℕ), Module.Free R (SingularCohomology.singularHomologyFamily R X n)) : have comul := ↑(kunnethIso R X X hfree hfree).symm ∘ₗ SingularCohomology.totalDiagMap R X; ↑(TensorProduct.gradedComm R (SingularCohomology.singularHomologyFamily R X) (SingularCohomology.singularHomologyFamily R X)) ∘ₗ comul = comul

Graded cocommutativity: the comultiplication on $H_*(X; R)$ commutes with the graded twist $\tau(x \otimes y) = (-1)^{|x| \cdot |y|} y \otimes x$.

theorem SingularCohomology.singularHomology_commGradedCoalgebra (R : Type) [CommRing R] [IsPrincipalIdealRing R] (X : TopCat) (hfree : ∀ (n : ℕ), Module.Free R (singularHomologyFamily R X n)) : ∃ (inst : Coalgebra R (totalSingularHomology R X)), (∀ (n : ℕ) (x : singularHomologyFamily R X n) (p q : ℕ), p + q ≠ n → (DirectSum.component R (ℕ × ℕ) (fun (pq : ℕ × ℕ) => TensorProduct R (singularHomologyFamily R X pq.1) (singularHomologyFamily R X pq.2)) (p, q)) ((TensorProduct.directSum R R (singularHomologyFamily R X) (singularHomologyFamily R X)) (CoalgebraStruct.comul ((DirectSum.lof R ℕ (singularHomologyFamily R X) n) x))) = 0) ∧ ↑(TensorProduct.gradedComm R (singularHomologyFamily R X) (singularHomologyFamily R X)) ∘ₗ CoalgebraStruct.comul = CoalgebraStruct.comul

Corollary 26.2. If $R$ is a PID and $H_*(X; R)$ is free over $R$, then $H_*(X; R)$ is a commutative graded coalgebra over $R$ (Definition 26.1): the comultiplication is induced by the diagonal via Künneth, the augmentation is the counit, and the structure is graded cocommutative.

noncomputable def SingularCohomology.inducedCochainMap (R : Type) [CommRing R] {X Y : TopCat} (f : X ⟶ Y) : singularCochainComplex R Y (ModuleCat.of R R) ⟶ singularCochainComplex R X (ModuleCat.of R R)

The cochain map $S^*(Y; R) \to S^*(X; R)$ induced (contravariantly) by $f : X \to Y$.

noncomputable def SingularCohomology.singularCohomologyMap (R : Type) [CommRing R] {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) : singularCohomology R Y (ModuleCat.of R R) n ⟶ singularCohomology R X (ModuleCat.of R R) n

The induced map on $n$th singular cohomology $f^* : H^n(Y; R) \to H^n(X; R)$.

def SingularCohomology.awFrontFace (p q : ℕ) : SimplexCategory.mk p ⟶ SimplexCategory.mk (p + q)

The Alexander–Whitney "front face" $\alpha_p : [p] \to [p+q]$ sending $i \mapsto i$.

def SingularCohomology.awBackFace (p q : ℕ) : SimplexCategory.mk q ⟶ SimplexCategory.mk (p + q)

The Alexander–Whitney "back face" $\omega_q : [q] \to [p+q]$ sending $j \mapsto j + p$.

noncomputable def SingularCohomology.awFront (Z : TopCat) (p q : ℕ) (σ : (TopCat.toSSet.obj Z).obj (Opposite.op (SimplexCategory.mk (p + q)))) : (TopCat.toSSet.obj Z).obj (Opposite.op (SimplexCategory.mk p))

The Alexander–Whitney "front" $\sigma \mapsto \sigma \circ \alpha_p$ of a $(p+q)$-simplex.

noncomputable def SingularCohomology.awBack (Z : TopCat) (p q : ℕ) (σ : (TopCat.toSSet.obj Z).obj (Opposite.op (SimplexCategory.mk (p + q)))) : (TopCat.toSSet.obj Z).obj (Opposite.op (SimplexCategory.mk q))

The Alexander–Whitney "back" $\sigma \mapsto \sigma \circ \omega_q$ of a $(p+q)$-simplex.

noncomputable def SingularCohomology.evalGen (R : Type) [CommRing R] {α : Type} (φ : (∐ fun (x : α) => ModuleCat.of R R) ⟶ ModuleCat.of R R) (σ : α) : R

Evaluate a morphism from a coproduct of copies of $R$ at a fixed index $\sigma$.

noncomputable def SingularCohomology.evalAtSimplex (R : Type) [CommRing R] {n : ℕ} (Z : TopCat) (σ : (TopCat.toSSet.obj Z).obj (Opposite.op (SimplexCategory.mk n))) : ↑((singularCochainComplex R Z (ModuleCat.of R R)).X n) →ₗ[R] R

Evaluation of a singular $n$-cochain at a singular $n$-simplex $\sigma$, as an $R$-linear map $S^n(Z; R) \to R$.

theorem SingularCohomology.ofHom_add_hom_eq (R : Type) [CommRing R] (f g : R →ₗ[R] R) : ModuleCat.Hom.hom (ModuleCat.ofHom f + ModuleCat.ofHom g) = f + g

Glue lemma: $(f + g)$ in ModuleCat.ofHom agrees with $f + g$ on underlying linear maps.

noncomputable def SingularCohomology.cupBilinear (R : Type) [CommRing R] (Z : TopCat) (p q : ℕ) : ↑((singularCochainComplex R Z (ModuleCat.of R R)).X p) →ₗ[R] ↑((singularCochainComplex R Z (ModuleCat.of R R)).X q) →ₗ[R] ↑((singularCochainComplex R Z (ModuleCat.of R R)).X (p + q))

The Alexander–Whitney bilinear cup product on cochains: $(f \cup g)(\sigma) = f(\sigma \circ \alpha_p) \cdot g(\sigma \circ \omega_q)$.

noncomputable def SingularCohomology.awCochainPairingHom (R : Type) [CommRing R] (Z : TopCat) (p q : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj ((singularCochainComplex R Z (ModuleCat.of R R)).X p) ((singularCochainComplex R Z (ModuleCat.of R R)).X q) ⟶ (singularCochainComplex R Z (ModuleCat.of R R)).X (p + q)

The Alexander–Whitney cup product on cochains, packaged as a morphism out of the tensor product $S^p(Z) \otimes S^q(Z) \to S^{p+q}(Z)$.

theorem SingularCohomology.awCochainPairingHom_leibniz (R : Type) [CommRing R] (Z : TopCat) (p q : ℕ) : CategoryTheory.CategoryStruct.comp (awCochainPairingHom R Z p q) ((singularCochainComplex R Z (ModuleCat.of R R)).d (p + q) (p + q + 1)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ((singularCochainComplex R Z (ModuleCat.of R R)).d p (p + 1)) (CategoryTheory.CategoryStruct.id ((singularCochainComplex R Z (ModuleCat.of R R)).X q))) (CategoryTheory.CategoryStruct.comp (awCochainPairingHom R Z (p + 1) q) (HomologicalComplex.XIsoOfEq (singularCochainComplex R Z (ModuleCat.of R R)) ⋯).hom) + (-1) ^ p • CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id ((singularCochainComplex R Z (ModuleCat.of R R)).X p)) ((singularCochainComplex R Z (ModuleCat.of R R)).d q (q + 1))) (awCochainPairingHom R Z p (q + 1))

The Leibniz rule for the cup product on cochains: $d(f \cup g) = df \cup g + (-1)^p f \cup dg$.

theorem SingularCohomology.awCup_cocycle_comp_d (R : Type) [CommRing R] (Z : TopCat) (p q : ℕ) : let K := singularCochainComplex R Z (ModuleCat.of R R); CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (HomologicalComplex.iCycles K p) (HomologicalComplex.iCycles K q)) (CategoryTheory.CategoryStruct.comp (awCochainPairingHom R Z p q) (K.d (p + q) (p + q + 1))) = 0

The cup product of two cocycles is a cocycle, by the Leibniz rule.

theorem SingularCohomology.awCup_factors_through_homology (R : Type) [CommRing R] (Z : TopCat) (p q : ℕ) : let K := singularCochainComplex R Z (ModuleCat.of R R); have cupToH := CategoryTheory.CategoryStruct.comp (HomologicalComplex.liftCycles K (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (HomologicalComplex.iCycles K p) (HomologicalComplex.iCycles K q)) (awCochainPairingHom R Z p q)) (p + q + 1) ⋯ ⋯) (HomologicalComplex.homologyπ K (p + q)); CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (CategoryTheory.MonoidalCategoryStruct.tensorHom (HomologicalComplex.homologyπ K p) (HomologicalComplex.homologyπ K q))) cupToH = 0

The Alexander–Whitney cup pairing on cochains descends through the tensor product of cohomology projections: the kernel of the tensored projection is annihilated by the map to H^{p+q}.

noncomputable def SingularCohomology.awCupPairing (R : Type) [CommRing R] (Z : TopCat) (p q : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (singularCohomology R Z (ModuleCat.of R R) p) (singularCohomology R Z (ModuleCat.of R R) q) ⟶ singularCohomology R Z (ModuleCat.of R R) (p + q)

The Alexander–Whitney cup pairing on cohomology H^p(Z) ⊗ H^q(Z) → H^{p+q}(Z), obtained by descending the cochain-level pairing through the epimorphism H^p ⊗ H^q ↠ (H^p ⊗ H^q).

noncomputable def SingularCohomology.cohomologyCrossProduct (R : Type) [CommRing R] (X Y : TopCat) (p q : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (singularCohomology R X (ModuleCat.of R R) p) (singularCohomology R Y (ModuleCat.of R R) q) ⟶ singularCohomology R (X ⨯ Y) (ModuleCat.of R R) (p + q)

The cohomology cross product H^p(X) ⊗ H^q(Y) → H^{p+q}(X × Y), obtained by pulling back along the two projections and applying the Alexander–Whitney cup pairing on X × Y.

noncomputable def SingularCohomology.cupProduct (R : Type) [CommRing R] (X : TopCat) (p q : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (singularCohomology R X (ModuleCat.of R R) p) (singularCohomology R X (ModuleCat.of R R) q) ⟶ singularCohomology R X (ModuleCat.of R R) (p + q)

The cup product H^p(X) ⊗ H^q(X) → H^{p+q}(X) (Definition 28.2), obtained from the cohomology cross product by pulling back along the diagonal X → X × X.

noncomputable def SingularCohomology.singularCohomologyZeroIsoKer (X : TopCat) (N : ModuleCat ℤ) : singularCohomology ℤ X N 0 ≅ ModuleCat.of ℤ ↥(ModuleCat.Hom.hom (HomologicalComplex.sc' (singularCochainComplex ℤ X N) 0 0 1).g).ker

The zeroth singular cohomology H^0(X; N) is naturally isomorphic to the kernel of the coboundary d^0 : C^0(X; N) → C^1(X; N).

def SingularCohomology.pathConstantSubmodule (X : TopCat) (N : ModuleCat ℤ) : Submodule ℤ (↑X → ↑N)

The submodule of N-valued functions on X that are constant on path components: f x = f y whenever x and y are joined by a path.

noncomputable def SingularCohomology.pathConstantSubmoduleEquivPi0Func (X : TopCat) (N : ModuleCat ℤ) : ↥(pathConstantSubmodule X N) ≃ₗ[ℤ] ZerothHomotopy ↑X → ↑N

A function constant on path components is the same as a function on the set of path components π₀(X).

noncomputable def SingularCohomology.pathConstantEquivPi0Func (X : TopCat) (N : ModuleCat ℤ) : ↥(pathConstantSubmodule X N) ≃ₗ[ℤ] ZerothHomotopy ↑X → ↑N

Convenience alias for pathConstantSubmoduleEquivPi0Func viewed as a linear equivalence on the coerced submodule.

@[reducible, inline]

abbrev SingularCohomology.Sing (n : ℕ) (X : TopCat) : Type

The set of singular n-simplices in X: continuous maps Δ^n → X.

noncomputable def SingularCohomology.sing0EquivX (X : TopCat) : Sing 0 X ≃ ↑X

A singular 0-simplex in X is the same data as a point of X.

noncomputable def SingularCohomology.face₀ (X : TopCat) (σ : Sing 1 X) : Sing 0 X

The 0-th face of a singular 1-simplex (its endpoint).

noncomputable def SingularCohomology.face₁ (X : TopCat) (σ : Sing 1 X) : Sing 0 X

The 1-st face of a singular 1-simplex (its starting point).

noncomputable def SingularCohomology.oneSimplexOfPath (X : TopCat) {x y : ↑X} (γ : Path x y) : Sing 1 X

The singular 1-simplex obtained from a path γ : Path x y by composing with the canonical homeomorphism Δ^1 ≃ [0,1].

theorem SingularCohomology.sing0EquivX_face_eq (X : TopCat) (i : Fin 2) (σ : Sing 1 X) : (sing0EquivX X) ((TopCat.toSSet.obj X).map (SimplexCategory.δ i).op σ) = ((X.toSSetObjEquiv (Opposite.op (SimplexCategory.mk 1))) σ).toFun (stdSimplex.map (⇑(SimplexCategory.Hom.toOrderHom (SimplexCategory.δ i))) default)

Identifying a face of σ with a point of X agrees with evaluating the underlying continuous map at the corresponding vertex of Δ^1.

theorem SingularCohomology.stdSimplex_map_δ1_default : stdSimplex.map (⇑(SimplexCategory.Hom.toOrderHom (SimplexCategory.δ 1))) default = ⟨Pi.single 0 1, ⋯⟩

The image of the standard 0-simplex under δ_1 : Δ^0 → Δ^1 is the first standard basis point e₀.

theorem SingularCohomology.stdSimplex_map_δ0_default : stdSimplex.map (⇑(SimplexCategory.Hom.toOrderHom (SimplexCategory.δ 0))) default = ⟨Pi.single 1 1, ⋯⟩

The image of the standard 0-simplex under δ_0 : Δ^0 → Δ^1 is the second standard basis point e₁.

theorem SingularCohomology.face₁_oneSimplexOfPath (X : TopCat) {x y : ↑X} (γ : Path x y) : (sing0EquivX X) (face₁ X (oneSimplexOfPath X γ)) = x

The 1-st face of the singular 1-simplex of a path γ : Path x y is the starting point x.

theorem SingularCohomology.face₀_oneSimplexOfPath (X : TopCat) {x y : ↑X} (γ : Path x y) : (sing0EquivX X) (face₀ X (oneSimplexOfPath X γ)) = y

The 0-th face of the singular 1-simplex of a path γ : Path x y is the endpoint y.

theorem SingularCohomology.joined_of_one_simplex (X : TopCat) (σ : Sing 1 X) : Joined ((sing0EquivX X) (face₁ X σ)) ((sing0EquivX X) (face₀ X σ))

Any singular 1-simplex σ realises a path joining its two faces.

@[reducible, inline]

noncomputable abbrev SingularCohomology.d0Hom (X : TopCat) (N : ModuleCat ℤ) : ↑(HomologicalComplex.sc' (singularCochainComplex ℤ X N) 0 0 1).X₂ →ₗ[ℤ] ↑(HomologicalComplex.sc' (singularCochainComplex ℤ X N) 0 0 1).X₃

The underlying linear map of the zeroth coboundary d^0 : C^0(X; N) → C^1(X; N).

@[reducible, inline]

noncomputable abbrev SingularCohomology.singularChainZ (X : TopCat) : ChainComplex (ModuleCat ℤ) ℕ

The integral singular chain complex C_*(X; ℤ) of X.

noncomputable def SingularCohomology.cochainEvalN (X : TopCat) (N : ModuleCat ℤ) (n : ℕ) (f : ↑((singularCochainComplex ℤ X N).X n)) (σ : Sing n X) : ↑N

Evaluate a singular n-cochain f : C^n(X; N) on a singular n-simplex σ, returning the corresponding element of N.

theorem SingularCohomology.singularChainZ_ι_comp_d (X : TopCat) (σ : Sing 1 X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : Sing 1 X) => ModuleCat.of ℤ ℤ) σ) ((singularChainZ X).d 1 0) = CategoryTheory.Limits.Sigma.ι (fun (x : Sing 0 X) => ModuleCat.of ℤ ℤ) (face₀ X σ) - CategoryTheory.Limits.Sigma.ι (fun (x : Sing 0 X) => ModuleCat.of ℤ ℤ) (face₁ X σ)

Boundary formula for a singular 1-simplex: ∂σ = face₀(σ) − face₁(σ).

theorem SingularCohomology.coboundary_zero_eval (X : TopCat) (N : ModuleCat ℤ) (f : ↑((singularCochainComplex ℤ X N).X 0)) (σ : Sing 1 X) : cochainEvalN X N 1 ((CategoryTheory.ConcreteCategory.hom ((singularCochainComplex ℤ X N).d 0 1)) f) σ = cochainEvalN X N 0 f (face₀ X σ) - cochainEvalN X N 0 f (face₁ X σ)

Dual formula: for a 0-cochain f, the value of d^0 f on a singular 1-simplex σ is f(face₀ σ) − f(face₁ σ).

noncomputable def SingularCohomology.cochainOfFunc (X : TopCat) (N : ModuleCat ℤ) (g : ↑X → ↑N) : ↑((singularCochainComplex ℤ X N).X 0)

Build a singular 0-cochain C^0(X; N) from a function g : X → N, sending each singular 0-simplex σ₀ to the linear map 1 ↦ g(σ₀).

theorem SingularCohomology.cochainOfFunc_eval (X : TopCat) (N : ModuleCat ℤ) (g : ↑X → ↑N) (σ₀ : Sing 0 X) : cochainEvalN X N 0 (cochainOfFunc X N g) σ₀ = g ((sing0EquivX X) σ₀)

Evaluating the cochain cochainOfFunc X N g on a 0-simplex σ₀ returns g evaluated at the corresponding point.

theorem SingularCohomology.moduleCat_int_hom_ext {N : ModuleCat ℤ} (φ ψ : ModuleCat.of ℤ ℤ ⟶ N) (h : (ModuleCat.Hom.hom φ) 1 = (ModuleCat.Hom.hom ψ) 1) : φ = ψ

Two morphisms ℤ ⟶ N of ℤ-modules that agree on 1 are equal.

theorem SingularCohomology.cochain_ext (X : TopCat) (N : ModuleCat ℤ) (f₁ f₂ : ↑((singularCochainComplex ℤ X N).X 0)) (h : ∀ (σ₀ : Sing 0 X), cochainEvalN X N 0 f₁ σ₀ = cochainEvalN X N 0 f₂ σ₀) : f₁ = f₂

Two 0-cochains are equal iff they take the same value on every singular 0-simplex.

theorem SingularCohomology.cochain1_eq_zero_iff (X : TopCat) (N : ModuleCat ℤ) (f : ↑((singularCochainComplex ℤ X N).X 1)) : f = 0 ↔ ∀ (σ : Sing 1 X), cochainEvalN X N 1 f σ = 0

A 1-cochain vanishes iff it evaluates to zero on every singular 1-simplex.

noncomputable def SingularCohomology.kerD0EquivPathConstant (X : TopCat) (N : ModuleCat ℤ) : ↥(d0Hom X N).ker ≃ₗ[ℤ] ↥(pathConstantSubmodule X N)

A 0-cocycle is the same data as a function X → N that is constant on path components. This is the key linear equivalence underlying H^0(X; N) ≅ Map(π₀(X), N).

noncomputable def SingularCohomology.singularCohomologyKerEquivPi0Map (X : TopCat) (N : ModuleCat ℤ) : ↥(d0Hom X N).ker ≃ₗ[ℤ] ZerothHomotopy ↑X → ↑N

Composing the kernel-vs-path-constant equivalence with the path-constant-vs-π₀ equivalence: ker(d^0) ≃ Map(π₀(X), N).

noncomputable def SingularCohomology.singularCohomology_zero_eq_map_pi0 (X : TopCat) (N : ModuleCat ℤ) : singularCohomology ℤ X N 0 ≅ ModuleCat.of ℤ (ZerothHomotopy ↑X → ↑N)

Lemma 26.6: the zeroth singular cohomology with coefficients in N is naturally isomorphic to the module of functions from π₀(X) to N.