Documentation

TauCeti.AlgebraicTopology.Cohomology.Cup

The cup product in singular cohomology #

Let C be a k-linear preadditive monoidal category with coproducts. For a space X, the cup product of singular cochains is the cup product of cochains (TauCeti.ChainComplex.cupCochain) along the Alexander–Whitney diagonal X.alexanderWhitneyDiagonal u : C(X; T) ⟶ C(X; R) ⊗ C(X; S) of a coefficient morphism u : T ⟶ R ⊗ S (TopCat.alexanderWhitneyDiagonal), for a pairing μ : M ⊗ N ⟶ P of coefficient objects: a cochain φ of degree p with values in M and a cochain ψ of degree q with values in N give the cochain of degree n = p + q with values in P whose value on a singular simplex σ is μ (φ (σ|[0, …, p]) ⊗ ψ (σ|[p, …, n])), precomposed with u (TopCat.ιChainComplex_cupCochain_alexanderWhitneyDiagonal). It satisfies the Leibniz rule TauCeti.ChainComplex.d_comp_cupCochain, and so, when C is moreover abelian, descends to the k-bilinear cup product TopCat.singularCup on singular cohomology, which is natural in X.

For the cohomology of X with coefficients in modules over a commutative ring k, take C := ModuleCat k, R = S = T = 𝟙_ (ModuleCat k) (the module k) and u = (λ_ _).inv; then φ ⌣ ψ evaluates σ to μ (φ (σ|[0, …, p]) ⊗ ψ (σ|[p, …, n])), the cup product of Hatcher, Section 3.2.

The cup product is associative and unital. Associativity relates cup products along four diagonals and four pairings, and holds when the coefficient morphisms are coassociative and the pairings associative up to the associators; both sides then evaluate a simplex on its front, middle and back faces. The unit is the class of the constant 0-cocycle TopCat.constSingularCocycle whose value is the unit of the pairing.

Main definitions and results #

References #

source
theorem TopCat.ιChainComplex_cupCochain_alexanderWhitneyDiagonal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {k : Type u_1} [CommSemiring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] {R S T M N P : C} (X : TopCat) (u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) (p q n : ℕ) (h : p + q = n) (φ : ((toSSet.obj X).chainComplex R).X p ⟶ M) (ψ : ((toSSet.obj X).chainComplex S).X q ⟶ N) (σ : (toSSet.obj X).obj (Opposite.op { len := n })) :
CategoryTheory.CategoryStruct.comp ((toSSet.obj X).ιChainComplex σ) (((TauCeti.ChainComplex.cupCochain k (X.alexanderWhitneyDiagonal u) μ p q n h) φ) ψ) = CategoryTheory.CategoryStruct.comp u (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp ((toSSet.obj X).ιChainComplex ((CategoryTheory.ConcreteCategory.hom ((toSSet.obj X).map (SimplexCategory.subinterval 0 p ⋯).op)) σ)) φ) (CategoryTheory.CategoryStruct.comp ((toSSet.obj X).ιChainComplex ((CategoryTheory.ConcreteCategory.hom ((toSSet.obj X).map (SimplexCategory.subinterval p q ⋯).op)) σ)) ψ)) μ)

The cup product of singular cochains on a simplex: for cochains φ of degree p and ψ of degree q, the value of φ ⌣ ψ on a singular (p + q)-simplex σ is φ of the front p-face of σ tensored with ψ of its back q-face, followed by μ, after the coefficient morphism u.

source
theorem TopCat.cupCochain_alexanderWhitneyDiagonal_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {k : Type u_1} [CommSemiring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] {T P R₁ R₂ R₃ T₁₂ T₂₃ M₁ M₂ M₃ M₁₂ M₂₃ : C} (X : TopCat) {u₁₂ : T₁₂ ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R₁ R₂} {u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj T₁₂ R₃} {u₂₃ : T₂₃ ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R₂ R₃} {u' : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R₁ T₂₃} (hu : CategoryTheory.CategoryStruct.comp u (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight u₁₂ R₃) (CategoryTheory.MonoidalCategoryStruct.associator R₁ R₂ R₃).hom) = CategoryTheory.CategoryStruct.comp u' (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R₁ u₂₃)) {μ₁₂ : CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ M₂ ⟶ M₁₂} {μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M₁₂ M₃ ⟶ P} {μ₂₃ : CategoryTheory.MonoidalCategoryStruct.tensorObj M₂ M₃ ⟶ M₂₃} {μ' : CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ M₂₃ ⟶ P} (hμ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight μ₁₂ M₃) μ = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M₁ M₂ M₃).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M₁ μ₂₃) μ')) {p q r m m' n : ℕ} (h₁₂ : p + q = m) (h : m + r = n) (h₂₃ : q + r = m') (h' : p + m' = n) (φ₁ : ((toSSet.obj X).chainComplex R₁).X p ⟶ M₁) (φ₂ : ((toSSet.obj X).chainComplex R₂).X q ⟶ M₂) (φ₃ : ((toSSet.obj X).chainComplex R₃).X r ⟶ M₃) :
((TauCeti.ChainComplex.cupCochain k (X.alexanderWhitneyDiagonal u) μ m r n h) (((TauCeti.ChainComplex.cupCochain k (X.alexanderWhitneyDiagonal u₁₂) μ₁₂ p q m h₁₂) φ₁) φ₂)) φ₃ = ((TauCeti.ChainComplex.cupCochain k (X.alexanderWhitneyDiagonal u') μ' p m' n h') φ₁) (((TauCeti.ChainComplex.cupCochain k (X.alexanderWhitneyDiagonal u₂₃) μ₂₃ q r m' h₂₃) φ₂) φ₃)

Associativity of the cup product of singular cochains: (φ₁ ⌣ φ₂) ⌣ φ₃ = φ₁ ⌣ (φ₂ ⌣ φ₃), for coefficient morphisms that are coassociative up to the associator (hu) and pairings that are associative up to the associator (hμ). Both sides evaluate a singular simplex on its front p-face, its middle q-face and its back r-face. In the usual case, where every coefficient object is 𝟙_ C and every coefficient morphism is (λ_ _).inv, hu holds by monoidal coherence and hμ is the associativity of a ring object of coefficients.

source
theorem TopCat.cupCochain_constCochain_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {k : Type u_1} [CommSemiring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] {R S M N : C} (X : TopCat) {u : S ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S} {μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ N} {e : R ⟶ M} {η : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ M} (hu : CategoryTheory.CategoryStruct.comp u (CategoryTheory.MonoidalCategoryStruct.whiskerRight e S) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor S).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight η S)) (hμ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight η N) μ = (CategoryTheory.MonoidalCategoryStruct.leftUnitor N).hom) {q : ℕ} (h : 0 + q = q) (ψ : ((toSSet.obj X).chainComplex S).X q ⟶ N) :
((TauCeti.ChainComplex.cupCochain k (X.alexanderWhitneyDiagonal u) μ 0 q q h) ((toSSet.obj X).constCochain e)) ψ = ψ

The left unit law for the cup product of singular cochains: the constant 0-cochain with value e is a left unit, provided that u followed by e is the left unitor followed by some η : 𝟙_ C ⟶ M which is a left unit for the pairing μ. For coefficients in a ring object M with unit η, take R = S = 𝟙_ C, u = (λ_ _).inv and e = η.

source
theorem TopCat.cupCochain_constCochain_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {k : Type u_1} [CommSemiring k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] {R S M N : C} (X : TopCat) {u : R ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S} {μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ M} {e : S ⟶ N} {η : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ N} (hu : CategoryTheory.CategoryStruct.comp u (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R e) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor R).inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R η)) (hμ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M η) μ = (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom) {p : ℕ} (h : p + 0 = p) (φ : ((toSSet.obj X).chainComplex R).X p ⟶ M) :
((TauCeti.ChainComplex.cupCochain k (X.alexanderWhitneyDiagonal u) μ p 0 p h) φ) ((toSSet.obj X).constCochain e) = φ

The right unit law for the cup product of singular cochains: the constant 0-cochain with value e is a right unit, provided that u followed by e is the right unitor followed by some η : 𝟙_ C ⟶ N which is a right unit for the pairing μ. For coefficients in a ring object N with unit η, take R = S = 𝟙_ C, u = (ρ_ _).inv (which is (λ_ _).inv) and e = η.

source
noncomputable def TopCat.singularCup {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {R S T M N P : C} (X : TopCat) (k : Type u_1) [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) (p q n : ℕ) (h : p + q = n) :
↑(TopCat.singularCohomology R k M X p) →ₗ[k] ↑(TopCat.singularCohomology S k N X q) →ₗ[k] ↑(TopCat.singularCohomology T k P X n)

The cup product on singular cohomology, Hᵖ(X; R, M) × H^q(X; S, N) ⟶ Hⁿ(X; T, P) for p + q = n: the cup product of cohomology classes along the Alexander–Whitney diagonal X.alexanderWhitneyDiagonal u and the pairing μ : M ⊗ N ⟶ P, k-bilinear and natural in X (TopCat.singularCup_naturality).

Equations
Instances For
    source
    @[simp]
    theorem TopCat.singularCup_homologyπ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {R S T M N P : C} (X : TopCat) (k : Type u_1) [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) (p q n : ℕ) (h : p + q = n) (a : ↑(HomologicalComplex.cycles (singularCochainComplex R k M X) p)) (b : ↑(HomologicalComplex.cycles (singularCochainComplex S k N X) q)) :
    ((X.singularCup k u μ p q n h) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (singularCochainComplex R k M X) p)) a)) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (singularCochainComplex S k N X) q)) b) = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (singularCochainComplex T k P X) n)) (((TauCeti.ChainComplex.cupCycles k (X.alexanderWhitneyDiagonal u) μ p q n h) a) b)

    The cup product of the classes of two singular cocycles is the class of their cup product.

    source
    theorem TopCat.singularCup_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {R S T M N P : C} {X Y : TopCat} (f : X ⟶ Y) (k : Type u_1) [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] (u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) (p q n : ℕ) (h : p + q = n) (α : ↑(TopCat.singularCohomology R k M Y p)) (β : ↑(TopCat.singularCohomology S k N Y q)) :
    ((X.singularCup k u μ p q n h) ((CategoryTheory.ConcreteCategory.hom (TopCat.singularCohomologyMap f p)) α)) ((CategoryTheory.ConcreteCategory.hom (TopCat.singularCohomologyMap f q)) β) = (CategoryTheory.ConcreteCategory.hom (TopCat.singularCohomologyMap f n)) (((Y.singularCup k u μ p q n h) α) β)

    Naturality of the cup product: for a continuous map f : X ⟶ Y, pulling back two cohomology classes of Y along f and cupping them is pulling back their cup product.

    source
    theorem TopCat.singularCup_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {T P R₁ R₂ R₃ T₁₂ T₂₃ M₁ M₂ M₃ M₁₂ M₂₃ : C} (X : TopCat) (k : Type u_1) [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] {u₁₂ : T₁₂ ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R₁ R₂} {u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj T₁₂ R₃} {u₂₃ : T₂₃ ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R₂ R₃} {u' : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R₁ T₂₃} (hu : CategoryTheory.CategoryStruct.comp u (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight u₁₂ R₃) (CategoryTheory.MonoidalCategoryStruct.associator R₁ R₂ R₃).hom) = CategoryTheory.CategoryStruct.comp u' (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R₁ u₂₃)) {μ₁₂ : CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ M₂ ⟶ M₁₂} {μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M₁₂ M₃ ⟶ P} {μ₂₃ : CategoryTheory.MonoidalCategoryStruct.tensorObj M₂ M₃ ⟶ M₂₃} {μ' : CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ M₂₃ ⟶ P} (hμ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight μ₁₂ M₃) μ = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M₁ M₂ M₃).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M₁ μ₂₃) μ')) {p q r m m' n : ℕ} (h₁₂ : p + q = m) (h : m + r = n) (h₂₃ : q + r = m') (h' : p + m' = n) (a : ↑(TopCat.singularCohomology R₁ k M₁ X p)) (b : ↑(TopCat.singularCohomology R₂ k M₂ X q)) (c : ↑(TopCat.singularCohomology R₃ k M₃ X r)) :
    ((X.singularCup k u μ m r n h) (((X.singularCup k u₁₂ μ₁₂ p q m h₁₂) a) b)) c = ((X.singularCup k u' μ' p m' n h') a) (((X.singularCup k u₂₃ μ₂₃ q r m' h₂₃) b) c)

    Associativity of the cup product on singular cohomology: (a ⌣ b) ⌣ c = a ⌣ (b ⌣ c), for coefficient morphisms that are coassociative up to the associator (hu) and pairings that are associative up to the associator (hμ), as in TopCat.cupCochain_alexanderWhitneyDiagonal_assoc.

    source
    theorem TopCat.singularCup_constSingularCocycle_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {R S M N : C} (X : TopCat) (k : Type u_1) [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] {u : S ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S} {μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ N} {e : R ⟶ M} {η : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ M} (hu : CategoryTheory.CategoryStruct.comp u (CategoryTheory.MonoidalCategoryStruct.whiskerRight e S) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor S).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight η S)) (hμ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight η N) μ = (CategoryTheory.MonoidalCategoryStruct.leftUnitor N).hom) {q : ℕ} (h : 0 + q = q) (b : ↑(TopCat.singularCohomology S k N X q)) :
    ((X.singularCup k u μ 0 q q h) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (singularCochainComplex R k M X) 0)) (X.constSingularCocycle k e))) b = b

    The left unit law for the cup product on singular cohomology: the class of the constant 0-cocycle with value e is a left unit, under the hypotheses of TopCat.cupCochain_constCochain_left.

    source
    theorem TopCat.singularCup_constSingularCocycle_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] {R S M N : C} (X : TopCat) (k : Type u_1) [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] {u : R ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S} {μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ M} {e : S ⟶ N} {η : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ N} (hu : CategoryTheory.CategoryStruct.comp u (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R e) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor R).inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R η)) (hμ : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M η) μ = (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).hom) {p : ℕ} (h : p + 0 = p) (a : ↑(TopCat.singularCohomology R k M X p)) :
    ((X.singularCup k u μ p 0 p h) a) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (singularCochainComplex S k N X) 0)) (X.constSingularCocycle k e)) = a

    The right unit law for the cup product on singular cohomology: the class of the constant 0-cocycle with value e is a right unit, under the hypotheses of TopCat.cupCochain_constCochain_right.

    source
    theorem TauCeti.singularCup_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (k : Type u_1) [CommRing k] [CategoryTheory.Linear k C] [CategoryTheory.MonoidalLinear k C] {X : TopCat} {R S T M N P : C} (u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S) (μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ P) (p q n : ℕ) (h : p + q = n) :
    X.singularCup k u μ p q n h = ChainComplex.cup k (X.alexanderWhitneyDiagonal u) μ p q n h

    The singular cup product is the cohomological product along the Alexander–Whitney diagonal.