structure CupProduct.GradedRAlgebra (R : Type u_1) [CommRing R] : Type (max u_1 (u_2 + 1))

Definition 29.1. A graded $R$-algebra (for $R$ a commutative ring) is a $\mathbb{Z}$-graded $R$-module $A_*$ equipped with multiplication maps $A_p \otimes_R A_q \to A_{p+q}$ and a unit $\eta : R \to A_0$ satisfying the usual associativity and unit diagrams.

This bundles a family of $R$-modules with the graded-semiring/graded-algebra data taken from Mathlib's DirectSum / GAlgebra API.

• A : ℤ → Type u_2
• instAddCommGroup (i : ℤ) : AddCommGroup (self.A i)
• instModule (i : ℤ) : Module R (self.A i)
• instGSemiring : DirectSum.GSemiring self.A
• instGAlgebra : DirectSum.GAlgebra R self.A

def CupProduct.GradedRAlgebra.mul {R : Type u_1} [CommRing R] (GA : GradedRAlgebra R) {p q : ℤ} (x : GA.A p) (y : GA.A q) : GA.A (p + q)

Multiplication in a graded $R$-algebra: $A_p \otimes A_q \to A_{p + q}$.

def CupProduct.GradedRAlgebra.unit {R : Type u_1} [CommRing R] (GA : GradedRAlgebra R) : R →+ GA.A 0

The unit map $\eta : R \to A_0$ of a graded $R$-algebra.

structure CupProduct.GradedRAlgebra.IsGradedCommutative {R : Type u_1} [CommRing R] (GA : GradedRAlgebra R) : Prop

A graded $R$-algebra $A$ is (graded) commutative if the twist isomorphism satisfies $\tau(x \otimes y) = (-1)^{pq} y \otimes x$, i.e. $$x \cdot y = (-1)^{pq} y \cdot x$$ for $x \in A_p$ and $y \in A_q$. This is the Koszul sign rule, as used for example in singular cohomology under cup product.

• mul_comm (p q : ℤ) (x : GA.A p) (y : GA.A q) : GradedMonoid.GMul.mul x y = ↑(p * q).negOnePow • cast ⋯ (GradedMonoid.GMul.mul y x)

structure SingularCohomology.CupProductAlgebra (R : Type) [CommRing R] (X : TopCat) : Type

The total cohomology ring $H^*(X; R) = \bigoplus_{n \ge 0} H^n(X; R)$ of a space $X$ with coefficients in $R$, as a wrapper around the direct sum of singular cohomology groups. It will be given the structure of a graded $R$-algebra via the cup product.

• toDirectSum : DirectSum ℕ fun (n : ℕ) => ↑(singularCohomology R X (ModuleCat.of R R) n)

@[reducible, inline]

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

The graded family $n \mapsto H^n(X; R)$ of singular cohomology groups, viewed as plain types indexed by $\mathbb{N}$.

@[implicit_reducible]

noncomputable instance SingularCohomology.instAddCommGroupSingularCohomologyFamily (R : Type) [CommRing R] (X : TopCat) (n : ℕ) : AddCommGroup (singularCohomologyFamily R X n)

The additive group structure on each cohomology group $H^n(X; R)$, inherited from its ModuleCat representation.

noncomputable def SingularCohomology.cupMul (R : Type) [CommRing R] (X : TopCat) {p q : ℕ} (x : singularCohomologyFamily R X p) (y : singularCohomologyFamily R X q) : singularCohomologyFamily R X (p + q)

The cup product on singular cohomology, as a graded multiplication $\smile : H^p(X) \otimes H^q(X) \to H^{p + q}(X)$.

@[implicit_reducible]

noncomputable instance SingularCohomology.instGMulCohomologyFamily (R : Type) [CommRing R] (X : TopCat) : GradedMonoid.GMul (singularCohomologyFamily R X)

The cup product as a graded-monoid multiplication on $H^*(X; R)$.

noncomputable def SingularCohomology.augmentationCocycle (R : Type) [CommRing R] (X : TopCat) : ↑((singularCochainComplex R X (ModuleCat.of R R)).X 0)

The augmentation cocycle $\varepsilon \in C^0(X; R)$: the singular $0$-cochain assigning $1 \in R$ to every singular $0$-simplex. Its cohomology class is the unit of $H^*(X; R)$.

theorem SingularCohomology.augmentationCocycle_coboundary_zero (R : Type) [CommRing R] (X : TopCat) : CategoryTheory.CategoryStruct.comp ((((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj (ModuleCat.of R R)).obj X).d 1 0) (augmentationCocycle R X) = 0

The augmentation cocycle $\varepsilon$ is indeed a $0$-cocycle: its coboundary vanishes, since for each $1$-simplex $\sigma$ both endpoints map to $1 \in R$ and cancel. Used to lift $\varepsilon$ to a cohomology class.

noncomputable def SingularCohomology.cohomologyUnit (R : Type) [CommRing R] (X : TopCat) : singularCohomologyFamily R X 0

The unit $1 \in H^0(X; R)$ of the cohomology ring, obtained as the cohomology class of the augmentation cocycle $\varepsilon$.

@[implicit_reducible]

noncomputable instance SingularCohomology.instGOneCohomologyFamily (R : Type) [CommRing R] (X : TopCat) : GradedMonoid.GOne (singularCohomologyFamily R X)

The cohomology unit cohomologyUnit as the graded-monoid identity of $H^*(X; R)$.

theorem SingularCohomology.cupProduct_unit_left (R : Type) [CommRing R] (X : TopCat) (q : ℕ) (y : singularCohomologyFamily R X q) : cast ⋯ ((ModuleCat.Hom.hom (cupProduct R X 0 q)) (cohomologyUnit R X ⊗ₜ[R] y)) = y

Left unit law for the cup product: $1 \smile y = y$ for every $y \in H^q(X; R)$, where $1 \in H^0(X; R)$ is the class of the augmentation cocycle.

theorem SingularCohomology.cupProduct_one_mul (R : Type) [CommRing R] (X : TopCat) (a : GradedMonoid (singularCohomologyFamily R X)) : 1 * a = a

Graded-monoid form of cupProduct_unit_left: $1 \cdot a = a$ in $H^*(X; R)$.

theorem SingularCohomology.cupProduct_graded_comm (R : Type) [CommRing R] (X : TopCat) (p q : ℕ) (x : singularCohomologyFamily R X p) (y : singularCohomologyFamily R X q) : GradedMonoid.GMul.mul x y = ↑(↑p * ↑q).negOnePow • cast ⋯ (GradedMonoid.GMul.mul y x)

Graded commutativity (Koszul sign rule) for the cup product: $x \smile y = (-1)^{pq}\, y \smile x$ for $x \in H^p(X; R)$, $y \in H^q(X; R)$.

theorem SingularCohomology.cupProduct_mul_one (R : Type) [CommRing R] (X : TopCat) (a : GradedMonoid (singularCohomologyFamily R X)) : a * 1 = a

Right unit law for the cup product: $a \cdot 1 = a$. Deduced from cupProduct_one_mul by graded commutativity (the sign is trivially $+1$ in degree $0$).

theorem SingularCohomology.cupProduct_hom_assoc (R : Type) [CommRing R] (X : TopCat) (p q r : ℕ) (x : singularCohomologyFamily R X p) (y : singularCohomologyFamily R X q) (z : singularCohomologyFamily R X r) : cast ⋯ ((ModuleCat.Hom.hom (cupProduct R X (p + q) r)) ((ModuleCat.Hom.hom (cupProduct R X p q)) (x ⊗ₜ[R] y) ⊗ₜ[R] z)) = (ModuleCat.Hom.hom (cupProduct R X p (q + r))) (x ⊗ₜ[R] (ModuleCat.Hom.hom (cupProduct R X q r)) (y ⊗ₜ[R] z))

Associativity of the cup product on cochain-level homs: $(x \smile y) \smile z = x \smile (y \smile z)$ in $H^{p + q + r}(X; R)$.

theorem SingularCohomology.cupProduct_mul_assoc (R : Type) [CommRing R] (X : TopCat) (a b c : GradedMonoid (singularCohomologyFamily R X)) : a * b * c = a * (b * c)

Graded-monoid form of associativity: $(a \cdot b) \cdot c = a \cdot (b \cdot c)$ in the total cohomology $H^*(X; R)$.

theorem SingularCohomology.cupProduct_mul_zero (R : Type) [CommRing R] (X : TopCat) {i j : ℕ} (a : singularCohomologyFamily R X i) : GradedMonoid.GMul.mul a 0 = 0

Right annihilator: cup product with $0$ on the right vanishes, since the underlying linear map is $R$-bilinear.

theorem SingularCohomology.cupProduct_zero_mul (R : Type) [CommRing R] (X : TopCat) {i j : ℕ} (b : singularCohomologyFamily R X j) : GradedMonoid.GMul.mul 0 b = 0

Left annihilator: cup product with $0$ on the left vanishes.

theorem SingularCohomology.cupProduct_mul_add (R : Type) [CommRing R] (X : TopCat) {i j : ℕ} (a : singularCohomologyFamily R X i) (b c : singularCohomologyFamily R X j) : GradedMonoid.GMul.mul a (b + c) = GradedMonoid.GMul.mul a b + GradedMonoid.GMul.mul a c

Right distributivity of the cup product: $a \smile (b + c) = a \smile b + a \smile c$.

theorem SingularCohomology.cupProduct_add_mul (R : Type) [CommRing R] (X : TopCat) {i j : ℕ} (a b : singularCohomologyFamily R X i) (c : singularCohomologyFamily R X j) : GradedMonoid.GMul.mul (a + b) c = GradedMonoid.GMul.mul a c + GradedMonoid.GMul.mul b c

Left distributivity of the cup product: $(a + b) \smile c = a \smile c + b \smile c$.

def SingularCohomology.cupProduct_natCast (R : Type) [CommRing R] (X : TopCat) : ℕ → singularCohomologyFamily R X 0

The natural-number cast $\mathbb{N} \to H^0(X; R)$, defined recursively as $n \mapsto n \cdot 1_{H^*(X; R)}$. Provides the natCast field for the graded ring structure on $H^*(X; R)$.

theorem SingularCohomology.cupProduct_natCast_zero (R : Type) [CommRing R] (X : TopCat) : cupProduct_natCast R X 0 = 0

Base case for the natural-number cast: $0 \in \mathbb{N}$ maps to $0 \in H^0(X; R)$.

theorem SingularCohomology.cupProduct_natCast_succ (R : Type) [CommRing R] (X : TopCat) (n : ℕ) : cupProduct_natCast R X (n + 1) = cupProduct_natCast R X n + GradedMonoid.GOne.one

Successor case for the natural-number cast: the cast of $n + 1$ is the cast of $n$ plus the cohomology unit.

noncomputable def SingularCohomology.cupProduct_intCast (R : Type) [CommRing R] (X : TopCat) : ℤ → singularCohomologyFamily R X 0

The integer cast $\mathbb{Z} \to H^0(X; R)$, extending the natural-number cast by negation on negative integers. Provides the intCast field for the graded ring structure.

theorem SingularCohomology.cupProduct_intCast_ofNat (R : Type) [CommRing R] (X : TopCat) (n : ℕ) : cupProduct_intCast R X ↑n = cupProduct_natCast R X n

Compatibility of the integer cast with the natural-number cast on non-negative integers $n \ge 0$.

theorem SingularCohomology.cupProduct_intCast_negSucc (R : Type) [CommRing R] (X : TopCat) (n : ℕ) : cupProduct_intCast R X (Int.negSucc n) = -cupProduct_natCast R X (n + 1)

Behaviour of the integer cast on a negative integer $-(n + 1)$: it returns $-(n + 1) \cdot 1$ in $H^0(X; R)$.

@[implicit_reducible]

noncomputable instance SingularCohomology.instGRingCohomologyFamily (R : Type) [CommRing R] (X : TopCat) : DirectSum.GRing (singularCohomologyFamily R X)

Graded ring structure on the cohomology family $n \mapsto H^n(X; R)$, assembling unit, associativity, distributivity and the natural/integer casts proved above. This is what promotes $H^*(X; R) = \bigoplus_n H^n(X; R)$ to a ring under cup product.

noncomputable def SingularCohomology.cohomologyAlgebraMap (R : Type) [CommRing R] (X : TopCat) : R →+ singularCohomologyFamily R X 0

The unit map $R \to H^0(X; R)$ of the cohomology algebra, sending $r \in R$ to $r \cdot 1_{H^*(X; R)}$.

theorem SingularCohomology.cohomologyAlgebraMap_one (R : Type) [CommRing R] (X : TopCat) : (cohomologyAlgebraMap R X) 1 = GradedMonoid.GOne.one

The cohomology algebra map sends $1 \in R$ to the cohomology unit $1 \in H^0(X; R)$.

theorem SingularCohomology.cohomologyAlgebraMap_mul (R : Type) [CommRing R] (X : TopCat) (r s : R) : GradedMonoid.mk 0 ((cohomologyAlgebraMap R X) (r * s)) = GradedMonoid.mk (0 + 0) (GradedMonoid.GMul.mul ((cohomologyAlgebraMap R X) r) ((cohomologyAlgebraMap R X) s))

Multiplicativity of the cohomology algebra map: $\eta(rs) = \eta(r) \smile \eta(s)$, using the idempotence $1 \smile 1 = 1$ of the cohomology unit and bilinearity.

theorem SingularCohomology.cohomologyAlgebraMap_commutes (R : Type) [CommRing R] (X : TopCat) (r : R) (x : GradedMonoid (singularCohomologyFamily R X)) : GradedMonoid.mk 0 ((cohomologyAlgebraMap R X) r) * x = x * GradedMonoid.mk 0 ((cohomologyAlgebraMap R X) r)

Central commutativity: scalars from $R$ commute with every cohomology class. Required to view $H^*(X; R)$ as an $R$-algebra.

theorem SingularCohomology.cast_smul_family {R : Type} [CommRing R] {X : TopCat} {n m : ℕ} (h : n = m) (r : R) (z : singularCohomologyFamily R X n) : cast ⋯ (r • z) = r • cast ⋯ z

Casting along an equality of degrees commutes with scalar multiplication: $\mathrm{cast}_h(r \cdot z) = r \cdot \mathrm{cast}_h(z)$ in the cohomology family.

theorem SingularCohomology.cohomologyAlgebraMap_smul_def (R : Type) [CommRing R] (X : TopCat) (r : R) (x : GradedMonoid (singularCohomologyFamily R X)) : r • x = GradedMonoid.mk 0 ((cohomologyAlgebraMap R X) r) * x

Compatibility of $R$-scalar multiplication with the algebra map: $r \cdot x = \eta(r) \smile x$. Together with the previous lemmas this gives the $R$-algebra structure on $H^*(X; R)$.

@[implicit_reducible]

noncomputable instance SingularCohomology.instGAlgebraCohomologyFamily (R : Type) [CommRing R] (X : TopCat) : DirectSum.GAlgebra R (singularCohomologyFamily R X)

Graded $R$-algebra structure on $H^*(X; R)$, bundling the cohomology unit map, its multiplicativity, central commutativity, and compatibility with scalar multiplication.

def SingularCohomology.CupProductAlgebra.equiv (R : Type) [CommRing R] (X : TopCat) : CupProductAlgebra R X ≃ DirectSum ℕ (singularCohomologyFamily R X)

The wrapper structure CupProductAlgebra R X is canonically equivalent to the underlying direct sum $\bigoplus_n H^n(X; R)$, used to transfer ring/algebra instances onto it.

@[reducible]

noncomputable instance SingularCohomology.instRingCupProductAlgebra (R : Type) [CommRing R] (X : TopCat) : Ring (CupProductAlgebra R X)

The ring structure on $H^*(X; R) = \bigoplus_n H^n(X; R)$, transferred from the direct sum along CupProductAlgebra.equiv.

@[reducible]

noncomputable instance SingularCohomology.instAlgebraCupProductAlgebra (R : Type) [CommRing R] (X : TopCat) : Algebra R (CupProductAlgebra R X)

The $R$-algebra structure on the cohomology ring $H^*(X; R)$, also transferred from the direct sum along CupProductAlgebra.equiv.

structure SingularCohomology.KoszulTensorAlgebra (R : Type) [CommRing R] (X Y : TopCat) : Type

The Koszul tensor algebra $H^*(X; R) \otimes_R H^*(X; R)$, wrapping the $R$-tensor product of two cohomology rings. The cohomology cross product will be defined as a ring homomorphism out of this algebra.

• toTensorProduct : TensorProduct R (CupProductAlgebra R X) (CupProductAlgebra R Y)

@[implicit_reducible]

noncomputable instance SingularCohomology.instRingKoszulTensorAlgebra (R : Type) [CommRing R] (X Y : TopCat) : Ring (KoszulTensorAlgebra R X Y)

Ring structure on the Koszul tensor algebra, induced by the graded-commutative ring structures on $H^*(X; R)$ and $H^*(Y; R)$ together with the Koszul sign rule.

@[implicit_reducible]

noncomputable instance SingularCohomology.instAlgebraKoszulTensorAlgebra (R : Type) [CommRing R] (X Y : TopCat) : Algebra R (KoszulTensorAlgebra R X Y)

$R$-algebra structure on the Koszul tensor algebra.

noncomputable def SingularCohomology.crossProduct_ringHom_core (R : Type) [CommRing R] (X Y : TopCat) : KoszulTensorAlgebra R X Y →+* CupProductAlgebra R (TopCat.of (↑X × ↑Y))

The cohomology cross product assembled as a ring homomorphism $H^*(X; R) \otimes_R H^*(Y; R) \to H^*(X \times Y; R)$. The cross product of $a \in H^p(X)$ and $b \in H^q(Y)$ is $\mathrm{pr}_X^* a \smile \mathrm{pr}_Y^* b$.

theorem SingularCohomology.crossProduct_commutes_algebraMap_core (R : Type) [CommRing R] (X Y : TopCat) (r : R) : (crossProduct_ringHom_core R X Y) ((algebraMap R (KoszulTensorAlgebra R X Y)) r) = (algebraMap R (CupProductAlgebra R (TopCat.of (↑X × ↑Y)))) r

The cross-product ring homomorphism is compatible with the $R$-algebra unit: $\eta_{X \times Y}(r) = \mathrm{cross}(\eta_X(r) \otimes 1) = \mathrm{cross}(1 \otimes \eta_Y(r))$. This is needed to upgrade crossProduct_ringHom_core to an algebra map.

noncomputable def SingularCohomology.crossProduct_algHom (R : Type) [CommRing R] (X Y : TopCat) : KoszulTensorAlgebra R X Y →ₐ[R] CupProductAlgebra R (TopCat.of (↑X × ↑Y))

The cohomology cross product packaged as an $R$-algebra homomorphism $H^*(X; R) \otimes_R H^*(Y; R) \to H^*(X \times Y; R)$.

noncomputable def SingularCohomology.cohomologyCrossProductLinear (R : Type) [CommRing R] (X Y : TopCat) : KoszulTensorAlgebra R X Y →ₗ[R] CupProductAlgebra R (TopCat.of (↑X × ↑Y))

Proposition 29.2 (cohomology cross product, linear form). The cohomology cross product, viewed merely as an $R$-linear map $$H^*(X; R) \otimes_R H^*(Y; R) \longrightarrow H^*(X \times Y; R).$$ Obtained from the algebra map crossProduct_algHom by forgetting the multiplicative structure.

theorem SingularCohomology.crossProduct_map_mul (R : Type) [CommRing R] (X Y : TopCat) (a b : KoszulTensorAlgebra R X Y) : (cohomologyCrossProductLinear R X Y) (a * b) = (cohomologyCrossProductLinear R X Y) a * (cohomologyCrossProductLinear R X Y) b

Proposition 29.2 (multiplicativity of the cross product). The cohomology cross product is multiplicative: $$(a \times b) \cdot (a' \times b') = (-1)^{|b||a'|}\,(a \smile a') \times (b \smile b').$$ In compact form: the linear map cohomologyCrossProductLinear preserves products.

@[reducible, inline]

noncomputable abbrev CupProduct.singCochains (R : Type) [CommRing R] (G : ModuleCat R) (X : TopCat) : CochainComplex (ModuleCat R) ℕ

The singular cochain complex $C^*(X; G) = \mathrm{Hom}_R(C_*(X; R), G)$ of a topological space $X$ with coefficients in an $R$-module $G$, as an object of CochainComplex (ModuleCat R) ℕ.

@[reducible, inline]

noncomputable abbrev CupProduct.singCohom (R : Type) [CommRing R] (G : ModuleCat R) (X : TopCat) (n : ℕ) : ModuleCat R

The $n$-th singular cohomology $H^n(X; G)$ as an $R$-module, defined as the homology of the cochain complex singCochains R G X in degree $n$.

noncomputable def CupProduct.pullbackCochainMap (R : Type) [CommRing R] (G : ModuleCat R) {X Y : TopCat} (f : X ⟶ Y) : singCochains R G Y ⟶ singCochains R G X

Contravariant action of a continuous map $f : X \to Y$ on singular cochains: the pullback $f^* : C^*(Y; G) \to C^*(X; G)$ defined by precomposition with the induced chain map on $C_*(-; R)$.

noncomputable def CupProduct.cohomPullback (R : Type) [CommRing R] (G : ModuleCat R) {X Y : TopCat} (f : X ⟶ Y) (n : ℕ) : singCohom R G Y n ⟶ singCohom R G X n

The induced map $f^* : H^n(Y; G) \to H^n(X; G)$ on singular cohomology, obtained from pullbackCochainMap by passing to homology in degree $n$.

@[reducible, inline]

noncomputable abbrev CupProduct.sphereChainZ (m : ℕ) : ChainComplex (ModuleCat ℤ) ℕ

The singular chain complex $C_*(S^m; \mathbb{Z})$ of the $m$-sphere with integer coefficients, packaged as an object of ChainComplex (ModuleCat ℤ) ℕ.

noncomputable def CupProduct.sphereTopCatIso (m : ℕ) : TopCat.sphere m ≅ TopCat.of (SphereHomology.Sphere m)

Identification of the Mathlib sphere TopCat.sphere m with the SphereHomology.Sphere m used elsewhere in Atlas, via the canonical ULift homeomorphism.

theorem CupProduct.sphereChainZ_free (m i : ℕ) : Module.Free ℤ ↑((sphereChainZ m).X i)

Each chain group $C_i(S^m; \mathbb{Z})$ is a free $\mathbb{Z}$-module, being the direct sum of copies of $\mathbb{Z}$ indexed by singular simplices.

noncomputable def CupProduct.singularChainComplexFunctor_forget₂_iso (X : TopCat) : ((CategoryTheory.forget₂ (ModuleCat ℤ) AddCommGrpCat).mapHomologicalComplex (ComplexShape.down ℕ)).obj (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat ℤ)).obj (ModuleCat.of ℤ ℤ)).obj X) ≅ ((AlgebraicTopology.singularChainComplexFunctor AddCommGrpCat).obj (AddCommGrpCat.of ℤ)).obj X

Compatibility of the singular chain complex functor with the forgetful functor $\mathrm{Mod}_{\mathbb{Z}} \to \mathrm{Ab}$: forgetting the $\mathbb{Z}$-module structure on $C_*(X; \mathbb{Z})$ recovers the singular chain complex of $X$ valued in abelian groups.

theorem CupProduct.moduleCat_singularHomology_isZero_iff (X : TopCat) (n : ℕ) : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat ℤ)).obj (ModuleCat.of ℤ ℤ)).obj X) n) ↔ CategoryTheory.Limits.IsZero (HomologicalComplex.homology (((AlgebraicTopology.singularChainComplexFunctor AddCommGrpCat).obj (AddCommGrpCat.of ℤ)).obj X) n)

Vanishing of singular homology with $\mathbb{Z}$-module coefficients is equivalent to vanishing of the abelian-group-valued singular homology, allowing us to transfer known vanishing results from SphereHomology into the ModuleCat setting.

theorem CupProduct.sphereChainZ_homology_isZero (m n : ℕ) (hn_lt : n < m) (hn_pos : 0 < n) : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (sphereChainZ m) n)

Vanishing of sphere homology: $H_n(S^m; \mathbb{Z}) = 0$ for $0 < n < m$. Obtained by transporting SphereHomology.sphere_homology_vanishing from abelian-group coefficients to $\mathbb{Z}$-module coefficients.

theorem CupProduct.isZero_Ext_of_isZero {X : ModuleCat ℤ} (hX : CategoryTheory.Limits.IsZero X) (Y : ModuleCat ℤ) (n : ℕ) : CategoryTheory.Limits.IsZero (((Ext ℤ (ModuleCat ℤ) n).obj (Opposite.op X)).obj Y)

All Ext groups out of a zero object vanish: $\mathrm{Ext}^n(0, Y) = 0$ for every $n \ge 0$ and every $\mathbb{Z}$-module $Y$.

theorem CupProduct.sphereChainZ_homology_zero_projective (m : ℕ) (hm : m ≥ 2) : CategoryTheory.Projective (HomologicalComplex.homology (sphereChainZ m) 0)

For $m \ge 2$, the degree-$0$ homology $H_0(S^m; \mathbb{Z}) \cong \mathbb{Z}$ is a projective $\mathbb{Z}$-module (indeed free), so its Ext groups vanish in positive degree.

theorem CupProduct.sphereChainZ_ext1_isZero (m n : ℕ) (hn_lt : n < m) (hn_pos : 0 < n) : CategoryTheory.Limits.IsZero (((Ext ℤ (ModuleCat ℤ) 1).obj (Opposite.op (HomologicalComplex.homology (sphereChainZ m) (n - 1)))).obj (ModuleCat.of ℤ ℤ))

Vanishing of the $\mathrm{Ext}^1$ term appearing in the UCT for $H^n(S^m; \mathbb{Z})$ when $0 < n < m$: either $n - 1 > 0$ and the previous homology vanishes, or $n = 1$ and $H_0(S^m; \mathbb{Z})$ is projective.

theorem CupProduct.sphereChainZ_ext0_isZero (m n : ℕ) (hn_lt : n < m) (hn_pos : 0 < n) : CategoryTheory.Limits.IsZero (((Ext ℤ (ModuleCat ℤ) 0).obj (Opposite.op (HomologicalComplex.homology (sphereChainZ m) n))).obj (ModuleCat.of ℤ ℤ))

Vanishing of the $\mathrm{Ext}^0 = \mathrm{Hom}$ term in the UCT for $H^n(S^m; \mathbb{Z})$ when $0 < n < m$: this $\mathrm{Hom}$ vanishes because $H_n(S^m; \mathbb{Z}) = 0$ in that range.

theorem CupProduct.sphere_cohom_isZero (m n : ℕ) (hn_lt : n < m) (hn_pos : 0 < n) : CategoryTheory.Limits.IsZero (singCohom ℤ (ModuleCat.of ℤ ℤ) (TopCat.sphere m) n)

Vanishing of sphere cohomology in intermediate degrees: $H^n(S^m; \mathbb{Z}) = 0$ for $0 < n < m$. Combines the UCT short exact sequence with the vanishing of the relevant Ext terms.

theorem CupProduct.kunneth_pullback_factors (p q : ℕ) (f : TopCat.sphere (p + q) ⟶ TopCat.sphere p ⨯ TopCat.sphere q) : ∃ (g : singCohom ℤ (ModuleCat.of ℤ ℤ) (TopCat.sphere p ⨯ TopCat.sphere q) (p + q) ⟶ singCohom ℤ (ModuleCat.of ℤ ℤ) (TopCat.sphere (p + q)) p) (h : singCohom ℤ (ModuleCat.of ℤ ℤ) (TopCat.sphere (p + q)) p ⟶ singCohom ℤ (ModuleCat.of ℤ ℤ) (TopCat.sphere (p + q)) (p + q)), cohomPullback ℤ (ModuleCat.of ℤ ℤ) f (p + q) = CategoryTheory.CategoryStruct.comp g h

Factorisation supplied by the Künneth/cup-product structure on the cohomology of $S^p \times S^q$: the pullback $f^* : H^{p+q}(S^p \times S^q) \to H^{p+q}(S^{p+q})$ factors as a composition $g \circ h$ through $H^p(S^{p+q})$, reflecting that any top-degree class on the product is a cup product of $p$- and $q$-dimensional classes.

theorem CupProduct.pullback_zero_of_cup_factors (p q : ℕ) (_hp : 0 < p) (_hq : 0 < q) (f : TopCat.sphere (p + q) ⟶ TopCat.sphere p ⨯ TopCat.sphere q) (hp_zero : CategoryTheory.Limits.IsZero (singCohom ℤ (ModuleCat.of ℤ ℤ) (TopCat.sphere (p + q)) p)) (_hq_zero : CategoryTheory.Limits.IsZero (singCohom ℤ (ModuleCat.of ℤ ℤ) (TopCat.sphere (p + q)) q)) : cohomPullback ℤ (ModuleCat.of ℤ ℤ) f (p + q) = 0

If $f^*$ factors through the (zero) group $H^p(S^{p+q})$, then $f^*$ itself vanishes. The technical bridge between kunneth_pullback_factors and the main corollary.

theorem CupProduct.sphere_product_pullback_zero (p q : ℕ) (hp : 0 < p) (hq : 0 < q) (f : TopCat.sphere (p + q) ⟶ TopCat.sphere p ⨯ TopCat.sphere q) : cohomPullback ℤ (ModuleCat.of ℤ ℤ) f (p + q) = 0

Corollary 29.4. For any continuous map $f : S^{p+q} \to S^p \times S^q$ with $p, q > 0$, the induced pullback on top-degree cohomology vanishes: $$f^* : H^{p+q}(S^p \times S^q; \mathbb{Z}) \longrightarrow H^{p+q}(S^{p+q}; \mathbb{Z}) \quad \text{is the zero map.}$$ Consequence: the top cohomology class $\alpha \times \beta$ of the product cannot be pulled back nontrivially to a sphere, ruling out an $H$-space structure on spheres other than $S^1, S^3, S^7$ (the classical application).

noncomputable def SphereHomology.sphereTopCatIso (m : ℕ) : TopCat.sphere m ≅ TopCat.of (Sphere m)

Identification of the Mathlib sphere TopCat.sphere m with the local SphereHomology.Sphere m, repeated here in the SphereHomology namespace for ergonomic access.

noncomputable def SphereHomology.singularChainComplexZ_iso_of_topIso {X Y : TopCat} (e : X ≅ Y) : AlgebraicTopologyI.singularChainComplexZ X ≅ AlgebraicTopologyI.singularChainComplexZ Y

Functoriality of the singular chain complex with $\mathbb{Z}$-coefficients: a homeomorphism (or TopCat-iso) $X \simeq Y$ induces an isomorphism of chain complexes $C_*(X; \mathbb{Z}) \simeq C_*(Y; \mathbb{Z})$.