structure HomologyCrossProduct.GradedBilinearMap (A : ExactSequence.IntChainComplex) (B : ExactSequence.IntChainComplex) (C : ExactSequence.IntChainComplex) : Type (max (max u_1 u_2) u_3)

A graded bilinear pairing of integer-indexed chain complexes A_* × B_* → C_*: in every bidegree (p, q) a bilinear map A_p × B_q → C_{p+q} satisfying the Leibniz rule d(a × b) = (da) × b + (-1)^p a × db together with the boundary conditions that cross-multiplying a boundary with a cycle (in either argument) lands in the boundaries. These are exactly the data needed by Lemma 7.1 to induce a bilinear pairing on homology.

• cross (p q : ℤ) : A.X p →+ B.X q →+ C.X (p + q)
• leibniz_d (p q : ℤ) (a : A.X p) (b : B.X q) : (C.d (p + q)) (((self.cross p q) a) b) = (C.castHom ⋯) (((self.cross (p - 1) q) ((A.d p) a)) b) + (-1) ^ p.toNat • (C.castHom ⋯) (((self.cross p (q - 1)) a) ((B.d q) b))
• cross_boundary_left (p q : ℤ) (a_bar : A.X (p + 1)) (b : B.X q) : b ∈ B.cycles q → ((self.cross p q) ((A.d' p) a_bar)) b ∈ C.boundaries (p + q)
• cross_boundary_right (p q : ℤ) (a : A.X p) (b_bar : B.X (q + 1)) : a ∈ A.cycles p → ((self.cross p q) a) ((B.d' q) b_bar) ∈ C.boundaries (p + q)

theorem HomologyCrossProduct.GradedBilinearMap.cross_mem_cycles {A : ExactSequence.IntChainComplex} {B : ExactSequence.IntChainComplex} {C : ExactSequence.IntChainComplex} (μ : GradedBilinearMap A B C) {p q : ℤ} {a : A.X p} {b : B.X q} (ha : a ∈ A.cycles p) (hb : b ∈ B.cycles q) : ((μ.cross p q) a) b ∈ C.cycles (p + q)

The cross product of two cycles is a cycle: if da = 0 and db = 0, the Leibniz rule forces d(a × b) = 0.

def HomologyCrossProduct.GradedBilinearMap.cross_on_cycles {A : ExactSequence.IntChainComplex} {B : ExactSequence.IntChainComplex} {C : ExactSequence.IntChainComplex} (μ : GradedBilinearMap A B C) (p q : ℤ) (a : ↥(A.cycles p)) (b : ↥(B.cycles q)) : ↥(C.cycles (p + q))

Restriction of the bidegree-(p, q) cross product to cycles, packaged so that its codomain is the subgroup of cycles in C_{p+q}.

noncomputable def HomologyCrossProduct.GradedBilinearMap.homology_cross_product {A : ExactSequence.IntChainComplex} {B : ExactSequence.IntChainComplex} {C : ExactSequence.IntChainComplex} (μ : GradedBilinearMap A B C) (p q : ℤ) : A.homologyGroup p →+ B.homologyGroup q →+ C.homologyGroup (p + q)

Lemma 7.1. Given chain complexes A_*, B_*, C_* and a bilinear pairing A_p × B_q → C_{p+q} satisfying the Leibniz formula, the induced map on homology is a bilinear pairing H_p(A) × H_q(B) → H_{p+q}(C). This is the descent of cross_on_cycles to homology groups, using that cycles cross-multiply to cycles and that boundaries cross-multiply (against cycles) to boundaries.

structure HomologyCrossProduct.HomologyCrossProductSingular : Type 1

Theorem 7.2 (Homology cross product). Bundle packaging the existence of a natural, bilinear, and normalized homology cross product × : H_p(X) × H_q(Y) → H_{p+q}(X × Y) for singular homology. It supplies a chain-level cross product chainCross, an integer-indexed chain complex singularIntComplex X for each space, a GradedBilinearMap packaging the Leibniz formula and boundary conditions for the chain cross product, and the induced homology pairing homologyCross shown equal to the descent provided by Lemma 7.1 (homologyCross_eq_lemma71), together with the naturality and normalization properties inherited from the chain-level cross product.

• chainCross : AlgebraicTopologyI.CrossProduct
• singularIntComplex (X : Type) [TopologicalSpace X] : ExactSequence.IntChainComplex
• gradedBilinear (X Y : Type) [TopologicalSpace X] [TopologicalSpace Y] : GradedBilinearMap (self.singularIntComplex X) (self.singularIntComplex Y) (self.singularIntComplex (X × Y))
• homologyCross (p q : ℤ) (X Y : Type) [TopologicalSpace X] [TopologicalSpace Y] : (self.singularIntComplex X).homologyGroup p →+ (self.singularIntComplex Y).homologyGroup q →+ (self.singularIntComplex (X × Y)).homologyGroup (p + q)
• homologyCross_eq_lemma71 (p q : ℤ) (X Y : Type) [TopologicalSpace X] [TopologicalSpace Y] : self.homologyCross p q X Y = (self.gradedBilinear X Y).homology_cross_product p q
• naturality (p q : ℕ) (X X' Y Y' : Type) [TopologicalSpace X] [TopologicalSpace X'] [TopologicalSpace Y] [TopologicalSpace Y'] (f : C(X, X')) (g : C(Y, Y')) (a : AlgebraicTopologyI.SingularChains p X) (b : AlgebraicTopologyI.SingularChains q Y) : ((self.chainCross.crossMap p q X' Y') ((AlgebraicTopologyI.SingularChains.map f) a)) ((AlgebraicTopologyI.SingularChains.map g) b) = (AlgebraicTopologyI.SingularChains.map (f.prodMap g)) (((self.chainCross.crossMap p q X Y) a) b)
• normalization_left (q : ℕ) (X Y : Type) [TopologicalSpace X] [TopologicalSpace Y] (x : X) (b : AlgebraicTopologyI.SingularChains q Y) : (AlgebraicTopologyI.SingularChains.castIdx ⋯) (((self.chainCross.crossMap 0 q X Y) (AlgebraicTopologyI.constChain x)) b) = (AlgebraicTopologyI.SingularChains.map (AlgebraicTopologyI.inclusionRight x)) b
• normalization_right (p : ℕ) (X Y : Type) [TopologicalSpace X] [TopologicalSpace Y] (y : Y) (a : AlgebraicTopologyI.SingularChains p X) : ((self.chainCross.crossMap p 0 X Y) a) (AlgebraicTopologyI.constChain y) = (AlgebraicTopologyI.SingularChains.map (AlgebraicTopologyI.inclusionLeft y)) a

theorem HomologyCrossProduct.hom_cast_apply_singular (X : Type) [TopologicalSpace X] (m n k : ℕ) (h1 : m + 1 = n) (h2 : m = k) (f : AlgebraicTopologyI.SingularChains (m + 1) X →+ AlgebraicTopologyI.SingularChains m X) (x : AlgebraicTopologyI.SingularChains n X) : (h1 ▸ h2 ▸ f) x = cast ⋯ (f (cast ⋯ x))

Technical cast lemma: rewriting an additive map SingularChains (m+1) X →+ SingularChains m X along equalities of natural-number indices behaves like casting the input and output through the corresponding equalities on the chain groups.

theorem HomologyCrossProduct.cast_singularChains_eq_zero (X : Type) [TopologicalSpace X] {m n : ℕ} (h : m = n) (x : AlgebraicTopologyI.SingularChains m X) : cast ⋯ x = 0 ↔ x = 0

Casting a chain along an equality of degrees gives zero iff the original chain was zero.

theorem HomologyCrossProduct.cast_boundaryMap_eq (X : Type) [TopologicalSpace X] (m k : ℕ) (h : m = k + 1) (y : AlgebraicTopologyI.SingularChains (m + 1) X) : (AlgebraicTopologyI.boundaryMap k X) (cast ⋯ ((AlgebraicTopologyI.boundaryMap m X) y)) = (AlgebraicTopologyI.boundaryMap k X) ((AlgebraicTopologyI.boundaryMap (k + 1) X) (cast ⋯ y))

Compatibility lemma between the boundary map and casting along an index equality m = k + 1: applying boundaryMap k after casting boundaryMap m y through h agrees with the composition boundaryMap k ∘ boundaryMap (k+1) applied to the appropriate cast of y.

noncomputable def HomologyCrossProduct.singularIntBoundary (X : Type) [TopologicalSpace X] (n : ℤ) : AlgebraicTopologyI.SingularChains n.toNat X →+ AlgebraicTopologyI.SingularChains (n - 1).toNat X

Integer-indexed boundary map on singular chains: for n ≥ 1 it is the usual boundary S_{n.toNat}(X) → S_{n.toNat - 1}(X) transported along the identifications n.toNat - 1 + 1 = n.toNat and n.toNat - 1 = (n - 1).toNat; for n < 1 it is zero. This is the data used to view singular chains as an IntChainComplex.

theorem HomologyCrossProduct.singularIntBoundary_comp (X : Type) [TopologicalSpace X] (n : ℤ) : (singularIntBoundary X (n - 1)).comp (singularIntBoundary X n) = 0

The integer-indexed boundary squares to zero, so the singular chains assembled with singularIntBoundary form an honest chain complex over ℤ.

noncomputable def HomologyCrossProduct.singularIntComplex (X : Type) [TopologicalSpace X] : ExactSequence.IntChainComplex

Singular chains of a topological space X packaged as an IntChainComplex: in degree n the group is SingularChains n.toNat X, with differential singularIntBoundary X n, vanishing in negative degrees.

noncomputable def HomologyCrossProduct.singularGradedBilinear (cp : AlgebraicTopologyI.CrossProduct) (X Y : Type) [TopologicalSpace X] [TopologicalSpace Y] : GradedBilinearMap (singularIntComplex X) (singularIntComplex Y) (singularIntComplex (X × Y))

Promotion of a chain-level singular cross product cp (Theorem 6.2) to a GradedBilinearMap between the integer-indexed singular chain complexes of X, Y, and X × Y: the bilinearity and Leibniz formula are inherited from cp, providing the input data for Lemma 7.1.

theorem HomologyCrossProduct.homologyCrossProduct_singular_exists : Nonempty HomologyCrossProductSingular

Existence of the singular homology cross product (Theorem 7.2). A HomologyCrossProductSingular package exists: combine the chain-level cross product from Theorem 6.2 with the descent to homology supplied by Lemma 7.1 to produce a natural, bilinear, and normalized homology cross product H_p(X) × H_q(Y) → H_{p+q}(X × Y) on singular homology.