Documentation

Atlas.AlgebraicTopologyI.code.CohomologyKunneth

@[reducible, inline]

Total singular cohomology of X with coefficients in R, assembled as the direct sum ⨁_{n : ℕ} H^n(X; R) over natural-number degrees.

Instances For

    The bidegree-(p, q) component of the cohomology cross product, viewed as a linear map from H^p(X; R) ⊗ H^q(Y; R) into the total cohomology ⨁_n H^n(X × Y; R) by landing in the degree p + q summand.

    Instances For

      The total cohomology cross product × : H^*(X; R) ⊗_R H^*(Y; R) → H^*(X × Y; R), built by distributing the tensor product over the direct-sum decompositions and assembling the bidegree components componentCrossMap.

      Instances For

        Auxiliary statement of the bijectivity of the Kronecker pairing H^n(X; R) → Hom_R(H_n(X; R), R) when R is a PID and every singular homology module of X is finitely generated and free. This is the universal coefficient isomorphism in this special case.

        Public version of kroneckerPairing_bijective_of_free_aux: when R is a PID and H_*(X; R) is finitely generated free in every degree, the Kronecker pairing H^n(X; R) → Hom_R(H_n(X; R), R) is bijective.

        Packaging of kroneckerPairing_bijective_of_free as an explicit linear equivalence H^n(X; R) ≃ₗ[R] Hom_R(H_n(X; R), R).

        Instances For
          @[reducible, inline]

          Total dual of singular homology: the direct sum ⨁_{n : ℕ} Hom_R(H_n(X; R), R). Under the universal coefficient theorem this is naturally isomorphic to totalSingularCohomology whenever H_*(X; R) is free.

          Instances For

            The bidegree-(p, q) component of an inverse to the homology Künneth map in degree n = p + q: pick a splitting of the Künneth short exact sequence on X and Y and project the resulting retraction onto the H_p(X; R) ⊗ H_q(Y; R) summand.

            Instances For

              Bidegree-(p, q) component of the left edge of the commuting diagram used to prove bijectivity of the cohomology cross product: apply the Kronecker pairings on each factor, distribute the tensor product through the dual, and dualize the Künneth inverse component.

              Instances For

                The total left edge of the comparison diagram: a linear map H^*(X; R) ⊗_R H^*(Y; R) → ⨁_n Hom_R(H_n(X × Y; R), R) assembled from the bidegree components componentDiagramLeftMap.

                Instances For

                  The total right edge of the comparison diagram: apply the Kronecker pairing in each degree to convert H^*(X × Y; R) into the direct sum of duals ⨁_n Hom_R(H_n(X × Y; R), R).

                  Instances For

                    Pointwise commutativity of the comparison diagram on simple tensors and a single homology class: the Kronecker pairing of the cohomology cross product a × b against a class z ∈ H_{p+q}(X × Y; R) agrees with the dual pairing obtained by routing z through the Künneth inverse.

                    Bidegree-(p, q) commutativity of the comparison diagram: composing the Kronecker pairing with the cohomology cross product agrees with componentDiagramLeftMap on H^p(X; R) ⊗ H^q(Y; R).

                    The total comparison square commutes: diagramRightMaptotalCohomologyCrossProduct = diagramLeftMap. This is the totalized version of diagram_comm_component.

                    The assembly map underlying diagramLeftMap (the direct-sum gluing of all componentDiagramLeftMap) is bijective; this is the technical core of the Künneth bijectivity argument on the left edge.

                    The left edge diagramLeftMap is bijective: combining the bijectivity of the assembly map with the tensor-direct-sum distributivity equivalence.

                    theorem CohomologyKunneth.directSum_toModule_lof_comp_bijective {R' : Type} [CommRing R'] {ι : Type} [DecidableEq ι] {M : ιType} [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R' (M i)] {N : ιType} [(i : ι) → AddCommGroup (N i)] [(i : ι) → Module R' (N i)] (f : (i : ι) → M i →ₗ[R'] N i) (hf : ∀ (i : ι), Function.Bijective (f i)) :
                    Function.Bijective (DirectSum.toModule R' ι (DirectSum ι N) fun (n : ι) => DirectSum.lof R' ι N n ∘ₗ f n)

                    Generic helper: if f i : M i →ₗ[R'] N i is bijective for every index i, then the assembled map ⨁ M i → ⨁ N i built by composing each f i with the direct-sum inclusion lof is bijective.

                    The tensor-product term ⨁_{p+q=m} H_p(X) ⊗_R H_q(Y) appearing in the homology Künneth short exact sequence is free over the PID R whenever H_*(X; R) is finitely generated and free in every degree.

                    The Tor term ⨁_{p+q=m-1} Tor^R_1(H_p(X), H_q(Y)) in the homology Künneth short exact sequence is free over the PID R under the same hypotheses; in fact, when H_*(X; R) is free this Tor vanishes.

                    If H_*(X; R) is finitely generated free over a PID R, then H_m(X × Y; R) is also free, obtained as a direct sum of the (free) Künneth tensor and Tor terms via a splitting of the Künneth short exact sequence.

                    Finiteness analogue of kunnethTensorTerm_free: the tensor term in the homology Künneth sequence is finitely generated over R when each H_n(X; R) is.

                    Finiteness analogue of kunnethTorTerm_free: the Tor term in the homology Künneth sequence is finitely generated over R.

                    Companion of productHomology_free: H_m(X × Y; R) is finitely generated over R whenever each H_n(X; R) is, using a splitting of the Künneth short exact sequence.

                    The right edge diagramRightMap is bijective: under the freeness and finiteness assumptions on H_*(X; R), the product homology H_*(X × Y; R) is also free and finitely generated, so the Kronecker pairing on X × Y is a bijection in every degree, and bijectivity assembles to the direct sum.

                    Diagram-chase proof of the cohomology Künneth theorem: combining the commutativity diagram_comm with the bijectivity of the left and right edges forces the total cohomology cross product to be bijective.

                    The assembly map ⨁_{(p, q)} (H^p(X; R) ⊗ H^q(Y; R)) → H^*(X × Y; R) built from the bidegree cross-product components is bijective. This is extracted from the bijectivity of the total cross product by cancelling the tensor-direct-sum distributivity equivalence.

                    Cohomology Künneth theorem (Theorem 33.3). Let R be a PID and suppose every singular homology module H_n(X; R) is finitely generated and free. Then the cohomology cross product × : H^*(X; R) ⊗_R H^*(Y; R) → H^*(X × Y; R) is a bijection.