Documentation

Atlas.AlgebraicTopologyI.code.Section33

@[reducible, inline]

The singular chain complex $S_\bullet(X; R)$ of a topological space X with coefficients in the ring R, as a chain complex of R-modules.

Instances For
    @[reducible, inline]
    noncomputable abbrev SingularCohomology.singularCohomologyR (R : Type) [CommRing R] (X : TopCat) (p : ) :

    The $p$-th singular cohomology module $H^p(X; R)$ of X with coefficients in R, computed as the $p$-th cohomology of the dual cochain complex $\mathrm{Hom}_R(S_\bullet(X; R), R)$.

    Instances For
      noncomputable def SingularCohomology.homologyPushforward (R : Type) [CommRing R] (X Y : TopCat) (f : X Y) (p : ) :

      The pushforward $f_* : H_p(X; R) \to H_p(Y; R)$ on singular homology induced by a continuous map f : X → Y.

      Instances For

        The cochain-level pullback $f^\# : S^\bullet(Y; R) \to S^\bullet(X; R)$ dual to the chain pushforward induced by f : X → Y.

        Instances For
          noncomputable def SingularCohomology.cohomologyPullback (R : Type) [CommRing R] (X Y : TopCat) (f : X Y) (p : ) :

          The pullback $f^* : H^p(Y; R) \to H^p(X; R)$ on singular cohomology induced by a continuous map f : X → Y.

          Instances For

            Index-shape compatibility lemma: for the descending complex shape on , the predecessor of p equals the successor of p for the ascending shape. Both equal p + 1. Used to reconcile homological and cohomological indexing.

            Index-shape compatibility lemma: for the descending complex shape on , the successor of p equals the predecessor of p for the ascending shape. Used to reconcile homological and cohomological indexing.

            The Kronecker pairing $\langle -, - \rangle : H^p(X; R) \otimes_R H_p(X; R) \to R$: a cohomology class β ∈ H^p(X; R) is represented by a cocycle, a homology class x ∈ H_p(X; R) is represented by a cycle, and the pairing evaluates the cocycle on the cycle. The construction passes to homology by verifying that cocycles vanish on boundaries and that coboundaries vanish on cycles.

            Instances For

              Claim 33.1 (naturality of the Kronecker pairing). For a continuous map $f : X \to Y$, a class $b \in H^p(Y; R)$ and a class $x \in H_p(X; R)$, $\langle f^* b, x \rangle = \langle b, f_* x \rangle$.

              noncomputable def SingularCohomology.homologyCross (R : Type) [CommRing R] (X Y : TopCat) (p q : ) :

              The homology cross product $\times : H_p(X; R) \otimes_R H_q(Y; R) \to H_{p+q}(X \times Y; R)$, constructed via the Eilenberg–Zilber / Alexander–Whitney machinery.

              Instances For
                noncomputable def SingularCohomology.cohomologyCross (R : Type) [CommRing R] (X Y : TopCat) (p q : ) :

                The cohomology cross product $\times : H^p(X; R) \otimes_R H^q(Y; R) \to H^{p+q}(X \times Y; R)$, defined via the Alexander–Whitney cup product on the categorical product followed by transport along TopCat.prodIsoProd.

                Instances For
                  theorem SingularCohomology.kroneckerPairing_prodIsoProd_compat (R : Type) [CommRing R] (X Y : TopCat) (n : ) (c : (singularCohomology R (X Y) (ModuleCat.of R R) n)) (h : (singularHomologyModule R (TopCat.of (X × Y)) n)) :
                  ((kroneckerPairing R (TopCat.of (X × Y)) n) ((ModuleCat.Hom.hom (singularCohomologyMap R (X.prodIsoProd Y).inv n)) c)) h = ((kroneckerPairing R (X Y) n) c) ((ModuleCat.Hom.hom (homologyPushforward R (TopCat.of (X × Y)) (X Y) (X.prodIsoProd Y).inv n)) h)

                  Compatibility of the Kronecker pairing with TopCat.prodIsoProd: an instance of kroneckerPairing_natural applied to the canonical comparison isomorphism between the categorical product X ⨯ Y and the topological product X × Y.

                  theorem SingularCohomology.awCupPairing_kronecker_eval (R : Type) [CommRing R] (X Y : TopCat) (p q : ) (a : (singularCohomology R X (ModuleCat.of R R) p)) (b : (singularCohomology R Y (ModuleCat.of R R) q)) (x : (singularHomologyModule R X p)) (y : (singularHomologyModule R Y q)) :
                  ((kroneckerPairing R (X Y) (p + q)) ((ModuleCat.Hom.hom (cohomologyCrossProduct R X Y p q)) (((TensorProduct.mk R (singularCohomology R X (ModuleCat.of R R) p) (singularCohomology R Y (ModuleCat.of R R) q)) a) b))) ((ModuleCat.Hom.hom (homologyPushforward R (TopCat.of (X × Y)) (X Y) (X.prodIsoProd Y).inv (p + q))) ((homologyCross R X Y p q) (((TensorProduct.mk R (singularHomologyModule R X p) (singularHomologyModule R Y q)) x) y))) = (-1) ^ (p * q) * ((kroneckerPairing R X p) a) x * ((kroneckerPairing R Y q) b) y

                  Cochain-level form of Lemma 33.2: the Kronecker pairing of the Alexander–Whitney cup product cohomology cross product with the pushforward of a homology cross product equals $(-1)^{pq}$ times the product of the individual Kronecker pairings.

                  theorem SingularCohomology.kroneckerPairing_cross_chain_compat (R : Type) [CommRing R] (X Y : TopCat) (p q : ) (a : (singularCohomology R X (ModuleCat.of R R) p)) (b : (singularCohomology R Y (ModuleCat.of R R) q)) (x : (singularHomologyModule R X p)) (y : (singularHomologyModule R Y q)) :
                  ((kroneckerPairing R (TopCat.of (X × Y)) (p + q)) ((cohomologyCross R X Y p q) (((TensorProduct.mk R (singularCohomology R X (ModuleCat.of R R) p) (singularCohomology R Y (ModuleCat.of R R) q)) a) b))) ((homologyCross R X Y p q) (((TensorProduct.mk R (singularHomologyModule R X p) (singularHomologyModule R Y q)) x) y)) = (-1) ^ (p * q) * ((kroneckerPairing R X p) a) x * ((kroneckerPairing R Y q) b) y

                  Intermediate form of Lemma 33.2 using cohomologyCross directly: same $(-1)^{pq}$ formula after rewriting the AW cup product through prodIsoProd.

                  theorem SingularCohomology.kroneckerPairing_cross (R : Type) [CommRing R] (X Y : TopCat) (p q : ) (a : (singularCohomology R X (ModuleCat.of R R) p)) (b : (singularCohomology R Y (ModuleCat.of R R) q)) (x : (singularHomologyModule R X p)) (y : (singularHomologyModule R Y q)) :
                  ((kroneckerPairing R (TopCat.of (X × Y)) (p + q)) ((cohomologyCross R X Y p q) (((TensorProduct.mk R (singularCohomology R X (ModuleCat.of R R) p) (singularCohomology R Y (ModuleCat.of R R) q)) a) b))) ((homologyCross R X Y p q) (((TensorProduct.mk R (singularHomologyModule R X p) (singularHomologyModule R Y q)) x) y)) = (-1) ^ (p * q) * ((kroneckerPairing R X p) a) x * ((kroneckerPairing R Y q) b) y

                  Lemma 33.2 (Kronecker pairing of cross products). The Kronecker pairing satisfies $\langle a \times b, x \times y \rangle = (-1)^{pq} \langle a, x \rangle \langle b, y \rangle$ for $a \in H^p(X; R)$, $b \in H^q(Y; R)$, $x \in H_p(X; R)$, $y \in H_q(Y; R)$.