Relative cup and cross products in singular cohomology #
Relative cup products are cup products along the descents of the Alexander–Whitney diagonal to
relative chains (TauCeti/AlgebraicTopology/Singular/AlexanderWhitney/RelativeCup.lean).
- Absolute–relative product. For a pair
(X, A), a cochain onXcupped with a cochain vanishing onAvanishes onA. This givesTopPair.singularCup : Hᵖ(X; R, M) × H^q(X, A; S, N) ⟶ Hⁿ(X, A; T, L), which needs no hypothesis onA. It is associative and unital, so it makesH*(X, A)a module overH*(X); it is natural in maps of pairs and maps to the absolute cup product underH*(X, A) ⟶ H*(X). - Relative cup product. For subsets
UandVofX, a cochain vanishing onUcupped with a cochain vanishing onVvanishes on the chainsC(U) + C(V)of the singular simplices lying inUor inV, but not in general on the chains ofU ∪ V. WhenUandVare open inU ∪ V, the small-chain theorem shows that restricting cochains fromC(X, U ∪ V)toC(X)/(C(U) + C(V))is an isomorphism on cohomology. Its inverse givesTopCat.singularRelativeCup : Hᵖ(X, U) × H^q(X, V) ⟶ Hⁿ(X, U ∪ V), natural in maps carryingUandVintoU'andV', and mapping to the absolute cup product. Some such hypothesis is needed: for arbitrary subsets the singular cochains vanishing onU ∪ Vneed not compute the cohomology of the quotient byC(U) + C(V). - Relative cross product. For open
A ⊆ XandB ⊆ Y, the cross productTauCeti.singularRelativeCross : Hᵖ(X, A) × H^q(Y, B) ⟶ Hⁿ(X × Y, A × Y ∪ X × B)is the relative cup product of the pullbacks along the two projections, whereA × YandX × Bare the preimages ofAandB. It is natural in both pairs and maps to the absolute cross productTauCeti.singularCross. WhenAandBare the complements of the zero sections of two vector bundles, this is the pairing on the cohomology of their Thom pairs.
Main definitions and results #
TopPair.d_comp_cupCochain_rightAlexanderWhitneyDiagonal: the Leibniz rule against a relative cocycle.TopPair.singularChainComplexMap_f_cupCochain_rightAlexanderWhitneyDiagonal: the cup product of absolute and relative cochains is natural in maps of pairs.TopPair.singularCup, withTopPair.singularCup_homologyπcomputing it on classes of cocycles,TopPair.singularCohomologyπ_singularCupits compatibility with the absolute cup product,TopPair.singularCup_naturality, and the module lawsTopPair.singularCup_assocandTopPair.singularCup_constSingularCocycle_left.TopCat.singularRelativeCup, characterized byTopCat.homologyMap_cochainComplexMap_singularRelativeCup, withTopCat.singularCohomologyπ_singularRelativeCupandTopCat.singularRelativeCup_naturality.TauCeti.singularRelativeCross, withTauCeti.singularRelativeCross_apply,TauCeti.singularCohomologyπ_singularRelativeCrossandTauCeti.singularRelativeCross_naturality.
References #
- A. Hatcher, Algebraic Topology,
Section 3.2, the relative cup products
Hᵏ(X) × Hˡ(X, A) ⟶ Hᵏ⁺ˡ(X, A)andHᵏ(X, A) × Hˡ(X, B) ⟶ Hᵏ⁺ˡ(X, A ∪ B)forAandBopen, and the relative cross productHᵏ(X, A) × Hˡ(Y, B) ⟶ Hᵏ⁺ˡ(X × Y, A × Y ∪ X × B)forAandBopen.
The action of absolute cohomology on relative cohomology #
theorem
TopPair.singularChainComplexπ_f_cupCochain_rightAlexanderWhitneyDiagonal
{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 L : C}
{k : Type u_1}
[CommSemiring k]
[CategoryTheory.Linear k C]
[CategoryTheory.MonoidalLinear k C]
(P : TopPair)
(u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S)
(μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ L)
(p q n : ℕ)
(h : p + q = n)
(φ : ((TopCat.toSSet.obj fst).chainComplex R).X p ⟶ M)
(ψ : (P.singularChainComplex S).X q ⟶ N)
:
CategoryTheory.CategoryStruct.comp ((P.singularChainComplexπ T).f n)
(((TauCeti.ChainComplex.cupCochain k (P.rightAlexanderWhitneyDiagonal u) μ p q n h) φ) ψ) = ((TauCeti.ChainComplex.cupCochain k (fst.alexanderWhitneyDiagonal u) μ p q n h) φ)
(CategoryTheory.CategoryStruct.comp ((P.singularChainComplexπ S).f q) ψ)
Precomposed with the quotient map to relative chains, the cup product of an absolute cochain
φ with a relative cochain ψ along the right relative Alexander–Whitney diagonal is the absolute
cup product of φ with ψ pulled back to absolute chains.
theorem
TopPair.singularChainComplexMap_f_cupCochain_rightAlexanderWhitneyDiagonal
{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 L : C}
{k : Type u_1}
[CommSemiring k]
[CategoryTheory.Linear k C]
[CategoryTheory.MonoidalLinear k C]
{P P' : TopPair}
(f : P ⟶ P')
(u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S)
(μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ L)
(p q n : ℕ)
(h : p + q = n)
(φ : ((TopCat.toSSet.obj fst).chainComplex R).X p ⟶ M)
(ψ : (P'.singularChainComplex S).X q ⟶ N)
:
CategoryTheory.CategoryStruct.comp ((singularChainComplexMap f T).f n)
(((TauCeti.ChainComplex.cupCochain k (P'.rightAlexanderWhitneyDiagonal u) μ p q n h) φ) ψ) = ((TauCeti.ChainComplex.cupCochain k (P.rightAlexanderWhitneyDiagonal u) μ p q n h)
(CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap (TopCat.toSSet.map (Hom.fst f)) R).f p) φ))
(CategoryTheory.CategoryStruct.comp ((singularChainComplexMap f S).f q) ψ)
Naturality of the cup product of absolute and relative cochains in maps of pairs: pulling
back φ ⌣ ψ along f : P ⟶ P' is the cup product of the pull-backs of φ and ψ.
theorem
TopPair.d_comp_cupCochain_rightAlexanderWhitneyDiagonal
{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 L : C}
{k : Type u_1}
[CommSemiring k]
[CategoryTheory.Linear k C]
[CategoryTheory.MonoidalLinear k C]
(P : TopPair)
(u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S)
(μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ L)
{p q n : ℕ}
(h : p + q = n)
(h' : p + 1 + q = n + 1)
(φ : ((TopCat.toSSet.obj fst).chainComplex R).X p ⟶ M)
(ψ : (P.singularChainComplex S).X q ⟶ N)
(hψ : CategoryTheory.CategoryStruct.comp ((P.singularChainComplex S).d (q + 1) q) ψ = 0)
:
CategoryTheory.CategoryStruct.comp ((P.singularChainComplex T).d (n + 1) n)
(((TauCeti.ChainComplex.cupCochain k (P.rightAlexanderWhitneyDiagonal u) μ p q n h) φ) ψ) = ((TauCeti.ChainComplex.cupCochain k (P.rightAlexanderWhitneyDiagonal u) μ (p + 1) q (n + 1) h')
(CategoryTheory.CategoryStruct.comp (((TopCat.toSSet.obj fst).chainComplex R).d (p + 1) p) φ))
ψ
The Leibniz rule against a relative cocycle: if ψ is a cocycle, the coboundary of
φ ⌣ ψ is δφ ⌣ ψ.
theorem
TopPair.cupCochain_rightAlexanderWhitneyDiagonal_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.MonoidalPreadditive C]
{S T L : C}
{k : Type u_1}
[CommSemiring k]
[CategoryTheory.Linear k C]
[CategoryTheory.MonoidalLinear k C]
{R₁ R₂ T₁₂ T₂₃ M₁ M₂ M₃ M₁₂ M₂₃ : C}
(P : TopPair)
{u₁₂ : T₁₂ ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R₁ R₂}
{u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj T₁₂ S}
{u₂₃ : T₂₃ ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R₂ S}
{u' : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R₁ T₂₃}
(hu :
CategoryTheory.CategoryStruct.comp u
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight u₁₂ S)
(CategoryTheory.MonoidalCategoryStruct.associator R₁ R₂ S).hom) = CategoryTheory.CategoryStruct.comp u' (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R₁ u₂₃))
{μ₁₂ : CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ M₂ ⟶ M₁₂}
{μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M₁₂ M₃ ⟶ L}
{μ₂₃ : CategoryTheory.MonoidalCategoryStruct.tensorObj M₂ M₃ ⟶ M₂₃}
{μ' : CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ M₂₃ ⟶ L}
(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)
(φ₁ : ((TopCat.toSSet.obj fst).chainComplex R₁).X p ⟶ M₁)
(φ₂ : ((TopCat.toSSet.obj fst).chainComplex R₂).X q ⟶ M₂)
(ψ : (P.singularChainComplex S).X r ⟶ M₃)
:
((TauCeti.ChainComplex.cupCochain k (P.rightAlexanderWhitneyDiagonal u) μ m r n h)
(((TauCeti.ChainComplex.cupCochain k (fst.alexanderWhitneyDiagonal u₁₂) μ₁₂ p q m h₁₂) φ₁) φ₂))
ψ = ((TauCeti.ChainComplex.cupCochain k (P.rightAlexanderWhitneyDiagonal u') μ' p m' n h') φ₁)
(((TauCeti.ChainComplex.cupCochain k (P.rightAlexanderWhitneyDiagonal u₂₃) μ₂₃ q r m' h₂₃) φ₂) ψ)
Associativity of the action of absolute cochains on relative cochains:
(φ₁ ⌣ φ₂) ⌣ ψ = φ₁ ⌣ (φ₂ ⌣ ψ) for absolute cochains φ₁, φ₂ and a relative cochain ψ, under
the coassociativity and associativity hypotheses of
TopCat.cupCochain_alexanderWhitneyDiagonal_assoc.
theorem
TopPair.cupCochain_rightAlexanderWhitneyDiagonal_constCochain_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}
{k : Type u_1}
[CommSemiring k]
[CategoryTheory.Linear k C]
[CategoryTheory.MonoidalLinear k C]
(P : TopPair)
{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)
(ψ : (P.singularChainComplex S).X q ⟶ N)
:
((TauCeti.ChainComplex.cupCochain k (P.rightAlexanderWhitneyDiagonal u) μ 0 q q h)
((TopCat.toSSet.obj fst).constCochain e))
ψ = ψ
The unit law for the action of absolute cochains on relative cochains: the constant
0-cochain with value e acts as the identity, under the hypotheses of
TopCat.cupCochain_constCochain_left.
noncomputable def
TopPair.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 L : C}
(k : Type u_1)
[CommRing k]
[CategoryTheory.Linear k C]
[CategoryTheory.MonoidalLinear k C]
(P : TopPair)
(u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S)
(μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ L)
(p q n : ℕ)
(h : p + q = n)
:
↑(TopCat.singularCohomology R k M fst p) →ₗ[k] ↑(P.singularCohomology S k N q) →ₗ[k] ↑(P.singularCohomology T k L n)
The cup product of absolute and relative singular cohomology,
Hᵖ(X; R, M) × H^q(X, A; S, N) ⟶ Hⁿ(X, A; T, L) for a pair (X, A) and p + q = n: the cup
product along the right relative Alexander–Whitney diagonal P.rightAlexanderWhitneyDiagonal u
and the pairing μ : M ⊗ N ⟶ L. It makes relative cohomology a module over absolute cohomology
(TopPair.singularCup_assoc and TopPair.singularCup_constSingularCocycle_left).
Instances For
theorem
TopPair.singularCup_def
{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 L : C}
(k : Type u_1)
[CommRing k]
[CategoryTheory.Linear k C]
[CategoryTheory.MonoidalLinear k C]
(P : TopPair)
(u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S)
(μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ L)
(p q n : ℕ)
(h : p + q = n)
:
singularCup k P u μ p q n h = TauCeti.ChainComplex.cup k (P.rightAlexanderWhitneyDiagonal u) μ p q n h
The cup product of absolute and relative singular cohomology is the cohomological cup product along the right relative Alexander–Whitney diagonal.
@[simp]
theorem
TopPair.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 L : C}
(k : Type u_1)
[CommRing k]
[CategoryTheory.Linear k C]
[CategoryTheory.MonoidalLinear k C]
(P : TopPair)
(u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S)
(μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ L)
(p q n : ℕ)
(h : p + q = n)
(a : ↑(HomologicalComplex.cycles (TopCat.singularCochainComplex R k M fst) p))
(b : ↑(HomologicalComplex.cycles (P.singularCochainComplex S k N) q))
:
((singularCup k P u μ p q n h)
((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (TopCat.singularCochainComplex R k M fst) p))
a))
((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (P.singularCochainComplex S k N) q)) b) = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (P.singularCochainComplex T k L) n))
(((TauCeti.ChainComplex.cupCycles k (P.rightAlexanderWhitneyDiagonal u) μ p q n h) a) b)
The cup product of the classes of an absolute and a relative cocycle is the class of their cup product.
@[simp]
theorem
TopPair.singularCohomologyπ_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 L : C}
(k : Type u_1)
[CommRing k]
[CategoryTheory.Linear k C]
[CategoryTheory.MonoidalLinear k C]
(P : TopPair)
(u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S)
(μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ L)
(p q n : ℕ)
(h : p + q = n)
(a : ↑(TopCat.singularCohomology R k M fst p))
(b : ↑(P.singularCohomology S k N q))
:
(CategoryTheory.ConcreteCategory.hom (P.singularCohomologyπ T k L n)) (((singularCup k P u μ p q n h) a) b) = ((fst.singularCup k u μ p q n h) a) ((CategoryTheory.ConcreteCategory.hom (P.singularCohomologyπ S k N q)) b)
Compatibility with the absolute cup product: the image in Hⁿ(X) of the cup product of
a ∈ Hᵖ(X) with b ∈ H^q(X, A) is the cup product of a with the image of b in H^q(X).
theorem
TopPair.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 L : C}
(k : Type u_1)
[CommRing k]
[CategoryTheory.Linear k C]
[CategoryTheory.MonoidalLinear k C]
{P P' : TopPair}
(f : P ⟶ P')
(u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S)
(μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ L)
(p q n : ℕ)
(h : p + q = n)
(a : ↑(TopCat.singularCohomology R k M fst p))
(b : ↑(P'.singularCohomology S k N q))
:
((singularCup k P u μ p q n h) ((CategoryTheory.ConcreteCategory.hom (TopCat.singularCohomologyMap (Hom.fst f) p)) a))
((CategoryTheory.ConcreteCategory.hom (TopPair.singularCohomologyMap f q)) b) = (CategoryTheory.ConcreteCategory.hom (TopPair.singularCohomologyMap f n)) (((singularCup k P' u μ p q n h) a) b)
Naturality of the cup product of absolute and relative cohomology in maps of pairs.
theorem
TopPair.singularCup_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.Limits.HasCoproducts C]
[CategoryTheory.MonoidalCategory C]
[CategoryTheory.MonoidalPreadditive C]
{S T L : C}
(k : Type u_1)
[CommRing k]
[CategoryTheory.Linear k C]
[CategoryTheory.MonoidalLinear k C]
{R₁ R₂ T₁₂ T₂₃ M₁ M₂ M₃ M₁₂ M₂₃ : C}
(P : TopPair)
{u₁₂ : T₁₂ ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R₁ R₂}
{u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj T₁₂ S}
{u₂₃ : T₂₃ ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R₂ S}
{u' : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R₁ T₂₃}
(hu :
CategoryTheory.CategoryStruct.comp u
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight u₁₂ S)
(CategoryTheory.MonoidalCategoryStruct.associator R₁ R₂ S).hom) = CategoryTheory.CategoryStruct.comp u' (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R₁ u₂₃))
{μ₁₂ : CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ M₂ ⟶ M₁₂}
{μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M₁₂ M₃ ⟶ L}
{μ₂₃ : CategoryTheory.MonoidalCategoryStruct.tensorObj M₂ M₃ ⟶ M₂₃}
{μ' : CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ M₂₃ ⟶ L}
(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₁ fst p))
(b : ↑(TopCat.singularCohomology R₂ k M₂ fst q))
(c : ↑(P.singularCohomology S k M₃ r))
:
((singularCup k P u μ m r n h) (((fst.singularCup k u₁₂ μ₁₂ p q m h₁₂) a) b)) c = ((singularCup k P u' μ' p m' n h') a) (((singularCup k P u₂₃ μ₂₃ q r m' h₂₃) b) c)
Associativity of the action of absolute cohomology on relative cohomology:
(a ⌣ b) ⌣ c = a ⌣ (b ⌣ c) for a, b absolute and c relative, under the hypotheses of
TopCat.singularCup_assoc.
theorem
TopPair.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}
(k : Type u_1)
[CommRing k]
[CategoryTheory.Linear k C]
[CategoryTheory.MonoidalLinear k C]
(P : TopPair)
{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 : ↑(P.singularCohomology S k N q))
:
((singularCup k P u μ 0 q q h)
((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (TopCat.singularCochainComplex R k M fst) 0))
(fst.constSingularCocycle k e)))
b = b
The unit law for the action of absolute cohomology on relative cohomology: the class of
the constant 0-cocycle with value e acts as the identity, under the hypotheses of
TopCat.cupCochain_constCochain_left.
The relative cup product of an excisive couple #
noncomputable def
TopCat.singularRelativeCup
{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 L : C}
(k : Type u_1)
[CommRing k]
[CategoryTheory.Linear k C]
[CategoryTheory.MonoidalLinear k C]
{X : TopCat}
(u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S)
(μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ L)
(U V : Set ↑X)
(hU : IsOpen (Subtype.val ⁻¹' U))
(hV : IsOpen (Subtype.val ⁻¹' V))
(p q n : ℕ)
(h : p + q = n)
:
↑((TopPair.ofSubset U).singularCohomology R k M p) →ₗ[k] ↑((TopPair.ofSubset V).singularCohomology S k N q) →ₗ[k] ↑((TopPair.ofSubset (U ∪ V)).singularCohomology T k L n)
The relative cup product Hᵖ(X, U; R, M) × H^q(X, V; S, N) ⟶ Hⁿ(X, U ∪ V; T, L) for
subsets U and V of X which are open in U ∪ V, and p + q = n: the cup product along the
relative Alexander–Whitney diagonal TopCat.relativeAlexanderWhitneyDiagonal U V u and the pairing
μ : M ⊗ N ⟶ L, which lands in the cohomology of the chains of X relative to its singular
simplices lying in U or in V, followed by the inverse of the small-chain isomorphism with the
cohomology of (X, U ∪ V) (TopCat.homologyMap_cochainComplexMap_singularRelativeCup).
Instances For
@[simp]
theorem
TopCat.homologyMap_cochainComplexMap_singularRelativeCup
{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 L : C}
(k : Type u_1)
[CommRing k]
[CategoryTheory.Linear k C]
[CategoryTheory.MonoidalLinear k C]
{X : TopCat}
(u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S)
(μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ L)
(U V : Set ↑X)
(hU : IsOpen (Subtype.val ⁻¹' U))
(hV : IsOpen (Subtype.val ⁻¹' V))
(p q n : ℕ)
(h : p + q = n)
(a : ↑((TopPair.ofSubset U).singularCohomology R k M p))
(b : ↑((TopPair.ofSubset V).singularCohomology S k N q))
:
(CategoryTheory.ConcreteCategory.hom
(HomologicalComplex.homologyMap (SSetPair.cochainComplexMap (smallSingularSubcomplexPairToUnion U V)) n))
(((singularRelativeCup k u μ U V hU hV p q n h) a) b) = ((TauCeti.ChainComplex.cup k (relativeAlexanderWhitneyDiagonal U V u) μ p q n h) a) b
The relative cup product is characterized by its image under the small-chain isomorphism: the cup product along the relative Alexander–Whitney diagonal.
@[simp]
theorem
TopCat.singularCohomologyπ_singularRelativeCup
{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 L : C}
(k : Type u_1)
[CommRing k]
[CategoryTheory.Linear k C]
[CategoryTheory.MonoidalLinear k C]
{X : TopCat}
(u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S)
(μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ L)
(U V : Set ↑X)
(hU : IsOpen (Subtype.val ⁻¹' U))
(hV : IsOpen (Subtype.val ⁻¹' V))
(p q n : ℕ)
(h : p + q = n)
(a : ↑((TopPair.ofSubset U).singularCohomology R k M p))
(b : ↑((TopPair.ofSubset V).singularCohomology S k N q))
:
(CategoryTheory.ConcreteCategory.hom ((TopPair.ofSubset (U ∪ V)).singularCohomologyπ T k L n))
(((singularRelativeCup k u μ U V hU hV p q n h) a) b) = ((X.singularCup k u μ p q n h)
((CategoryTheory.ConcreteCategory.hom ((TopPair.ofSubset U).singularCohomologyπ R k M p)) a))
((CategoryTheory.ConcreteCategory.hom ((TopPair.ofSubset V).singularCohomologyπ S k N q)) b)
Compatibility with the absolute cup product: the image in Hⁿ(X) of the relative cup
product of a ∈ Hᵖ(X, U) and b ∈ H^q(X, V) is the cup product of the images of a in Hᵖ(X) and
of b in H^q(X).
theorem
TopCat.singularRelativeCup_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 L : C}
(k : Type u_1)
[CommRing k]
[CategoryTheory.Linear k C]
[CategoryTheory.MonoidalLinear k C]
{X Y : TopCat}
(u : T ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj R S)
(μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ L)
{U V : Set ↑X}
{U' V' : Set ↑Y}
(hU : IsOpen (Subtype.val ⁻¹' U))
(hV : IsOpen (Subtype.val ⁻¹' V))
(hU' : IsOpen (Subtype.val ⁻¹' U'))
(hV' : IsOpen (Subtype.val ⁻¹' V'))
(f : X ⟶ Y)
(hfU : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) U U')
(hfV : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) V V')
(p q n : ℕ)
(h : p + q = n)
(a : ↑((TopPair.ofSubset U').singularCohomology R k M p))
(b : ↑((TopPair.ofSubset V').singularCohomology S k N q))
:
((singularRelativeCup k u μ U V hU hV p q n h)
((CategoryTheory.ConcreteCategory.hom (TopPair.singularCohomologyMap (TopPair.ofSubsetMap f hfU) p)) a))
((CategoryTheory.ConcreteCategory.hom (TopPair.singularCohomologyMap (TopPair.ofSubsetMap f hfV) q)) b) = (CategoryTheory.ConcreteCategory.hom (TopPair.singularCohomologyMap (TopPair.ofSubsetMap f ⋯) n))
(((singularRelativeCup k u μ U' V' hU' hV' p q n h) a) b)
Naturality of the relative cup product in maps f : X ⟶ Y carrying U into U' and V
into V'.
The relative cross product #
noncomputable def
TauCeti.singularRelativeCross
{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 L : C}
(k : Type u_1)
[CommRing k]
[CategoryTheory.Linear k C]
[CategoryTheory.MonoidalLinear k C]
(X Y : TopCat)
{A : Set ↑X}
{B : Set ↑Y}
(hA : IsOpen A)
(hB : IsOpen B)
(μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ L)
(p q n : ℕ)
(h : p + q = n)
:
↑((TopPair.ofSubset A).singularCohomology R k M p) →ₗ[k] ↑((TopPair.ofSubset B).singularCohomology S k N q) →ₗ[k] ↑((TopPair.ofSubset
(⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)) ⁻¹' A ∪
⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)) ⁻¹' B)).singularCohomology
(CategoryTheory.MonoidalCategoryStruct.tensorObj R S) k L n)
The relative cross product Hᵖ(X, A; R, M) × H^q(Y, B; S, N) ⟶ Hⁿ(X × Y, A × Y ∪ X × B; R ⊗ S, L) for open subsets A ⊆ X and B ⊆ Y, and p + q = n: the
relative cup product (TopCat.singularRelativeCup) of the pullbacks of the two classes along the
projections (X × Y, A × Y) ⟶ (X, A) and (X × Y, X × B) ⟶ (Y, B). Here A × Y and X × B are
the preimages of A and B under the projections, which are open, so the relative cup product
applies. It maps to the absolute cross product TauCeti.singularCross
(TauCeti.singularCohomologyπ_singularRelativeCross).
Instances For
theorem
TauCeti.singularRelativeCross_apply
{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 L : C}
(k : Type u_1)
[CommRing k]
[CategoryTheory.Linear k C]
[CategoryTheory.MonoidalLinear k C]
(X Y : TopCat)
{A : Set ↑X}
{B : Set ↑Y}
(hA : IsOpen A)
(hB : IsOpen B)
(μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ L)
(p q n : ℕ)
(h : p + q = n)
(a : ↑((TopPair.ofSubset A).singularCohomology R k M p))
(b : ↑((TopPair.ofSubset B).singularCohomology S k N q))
:
((singularRelativeCross k X Y hA hB μ p q n h) a) b = ((TopCat.singularRelativeCup k
(CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj R S)) μ
(⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)) ⁻¹' A)
(⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)) ⁻¹' B) ⋯ ⋯ p q n
h)
((CategoryTheory.ConcreteCategory.hom
(TopPair.singularCohomologyMap (TopPair.ofSubsetMap (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y) ⋯)
p))
a))
((CategoryTheory.ConcreteCategory.hom
(TopPair.singularCohomologyMap (TopPair.ofSubsetMap (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y) ⋯)
q))
b)
The relative cross product is the relative cup product of the pullbacks along the two projections.
@[simp]
theorem
TauCeti.singularCohomologyπ_singularRelativeCross
{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 L : C}
(k : Type u_1)
[CommRing k]
[CategoryTheory.Linear k C]
[CategoryTheory.MonoidalLinear k C]
(X Y : TopCat)
{A : Set ↑X}
{B : Set ↑Y}
(hA : IsOpen A)
(hB : IsOpen B)
(μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ L)
(p q n : ℕ)
(h : p + q = n)
(a : ↑((TopPair.ofSubset A).singularCohomology R k M p))
(b : ↑((TopPair.ofSubset B).singularCohomology S k N q))
:
(CategoryTheory.ConcreteCategory.hom
((TopPair.ofSubset
(⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)) ⁻¹' A ∪
⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)) ⁻¹' B)).singularCohomologyπ
(CategoryTheory.MonoidalCategoryStruct.tensorObj R S) k L n))
(((singularRelativeCross k X Y hA hB μ p q n h) a) b) = ((singularCross k X Y μ p q n h)
((CategoryTheory.ConcreteCategory.hom ((TopPair.ofSubset A).singularCohomologyπ R k M p)) a))
((CategoryTheory.ConcreteCategory.hom ((TopPair.ofSubset B).singularCohomologyπ S k N q)) b)
Compatibility with the absolute cross product: the image in Hⁿ(X × Y) of the relative
cross product of a ∈ Hᵖ(X, A) and b ∈ H^q(Y, B) is the cross product of the images of a in
Hᵖ(X) and of b in H^q(Y).
theorem
TauCeti.singularRelativeCross_naturality
{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 L : C}
(k : Type u_1)
[CommRing k]
[CategoryTheory.Linear k C]
[CategoryTheory.MonoidalLinear k C]
{X Y X' Y' : TopCat}
{A : Set ↑X}
{B : Set ↑Y}
{A' : Set ↑X'}
{B' : Set ↑Y'}
(hA : IsOpen A)
(hB : IsOpen B)
(hA' : IsOpen A')
(hB' : IsOpen B')
(f : X ⟶ X')
(g : Y ⟶ Y')
(hf : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) A A')
(hg : Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom g)) B B')
(μ : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ L)
(p q n : ℕ)
(h : p + q = n)
(a : ↑((TopPair.ofSubset A').singularCohomology R k M p))
(b : ↑((TopPair.ofSubset B').singularCohomology S k N q))
:
((singularRelativeCross k X Y hA hB μ p q n h)
((CategoryTheory.ConcreteCategory.hom (TopPair.singularCohomologyMap (TopPair.ofSubsetMap f hf) p)) a))
((CategoryTheory.ConcreteCategory.hom (TopPair.singularCohomologyMap (TopPair.ofSubsetMap g hg) q)) b) = (CategoryTheory.ConcreteCategory.hom
(TopPair.singularCohomologyMap (TopPair.ofSubsetMap (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) ⋯) n))
(((singularRelativeCross k X' Y' hA' hB' μ p q n h) a) b)
Naturality of the relative cross product in maps f : X ⟶ X' carrying A into A' and
g : Y ⟶ Y' carrying B into B'.