Cohomology

Results named in Tau Ceti's TauCeti.AlgebraicTopology.Cohomology modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremThe Künneth theorem for cohomology#

over a commutative semisimple ring k, for instance a field, if the homology Hₚ(X; k) is finitely generated in degrees p ≤ n, the cohomology Künneth map ⨁_{p + q = n} Hᵖ(X; k) ⊗ H^q(Y; k) ⟶ Hⁿ(X × Y; k) is bijective.

TopCat.singularCohomologyKunneth_bijective.{w} {k : Type w} [CommRing k] (X Y : TopCat)
  [IsSemisimpleRing k] (n : ℕ)
  (hX :
    ∀ p ≤ n,
      Module.Finite k
        ↑(((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) p).obj
                (CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat k))).obj
            X)) :
  Function.Bijective
    ⇑(CategoryTheory.ConcreteCategory.hom
        (X.singularCohomologyKunneth Y
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat k))
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat k)) k
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor
              (CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat k))).hom
          n))

Lean

Formalized in Tau Ceti as TopCat.singularCohomologyKunneth_bijective.

Sources

• Tau Ceti documentation: TopCat.singularCohomologyKunneth_bijective
• Source of TopCat.singularCohomologyKunneth_bijective in TauCeti/AlgebraicTopology/Cohomology/Kunneth.lean

LeanTopCat.singularCohomologyKunneth_bijective

Uses 3

Proof usesThe Eilenberg–Zilber theorem for singular chains · The Künneth theorem for cubical homology · The universal coefficient theorem over a field

TheoremThe relative small-chain theorem for cochains#

Restricting relative singular cochains of a topological pair to the simplices subordinate to an open cover of the ambient space is a quasi-isomorphism.

TopPair.quasiIso_cochainComplexMap_restrictι_smallSingularSubcomplex.{w, v, u, u_1, u_2}
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C]
  [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C}
  {ι : Type u_2} (P : TopPair) (U : ι → Set ↑TopPair.fst) (hU : ∀ (i : ι), IsOpen (U i))
  (hcov : ⋃ i, U i = Set.univ) :
  QuasiIso
    (SSetPair.cochainComplexMap
      ((TopPair.toSSetPair.obj P).restrictι (P.smallSingularSubcomplex U)))

Lean

Formalized in Tau Ceti as TopPair.quasiIso_cochainComplexMap_restrictι_smallSingularSubcomplex.

Sources

• Tau Ceti documentation: TopPair.quasiIso_cochainComplexMap_restrictι_smallSingularSubcomplex
• Source of TopPair.quasiIso_cochainComplexMap_restrictι_smallSingularSubcomplex in TauCeti/AlgebraicTopology/Cohomology/Excision.lean

LeanTopPair.quasiIso_cochainComplexMap_restrictι_smallSingularSubcomplex

DefinitionThe relative universal coefficient theorem over a field#

the relative singular cohomology of a pair with coefficients in a field k is the dual of its relative singular homology, Hⁿ(X, A; k) ≃ₗ[k] Module.Dual k (Hₙ(X, A; k)). It sends a class to the linear form underlying its relative Kronecker pairing (TopPair.singularCohomologyDualEquiv_apply).

TopPair.singularCohomologyDualEquiv.{w} {k : Type w} [Field k] (P : TopPair) (n : ℕ) :
  ↑(P.singularCohomology (↧k) k (↧k) n) ≃ₗ[k] Module.Dual k ↑(P.singularHomology (↧k) n)

Lean

Formalized in Tau Ceti as TopPair.singularCohomologyDualEquiv.

Other forms

The relative universal coefficient theorem with projective homology, over any commutative ring k. Formalized in Tau Ceti as TopPair.singularKronecker_bijective_of_projective_homology.

TopPair.singularKronecker_bijective_of_projective_homology.{w, u_1} {k : Type u_1} [CommRing k]
  (P : TopPair) (R M : ModuleCat k) [Module.Projective k ↑R]
  [hP : ∀ (n : ℕ), CategoryTheory.Projective (P.singularHomology R n)]
  [CategoryTheory.Linear k (ModuleCat k)] (n : ℕ) : Function.Bijective ⇑(P.singularKronecker k n)

Sources

• Tau Ceti documentation: TopPair.singularCohomologyDualEquiv
• Source of TopPair.singularCohomologyDualEquiv in TauCeti/AlgebraicTopology/Cohomology/UniversalCoefficient/Field.lean

LeanTopPair.singularCohomologyDualEquiv · TopPair.singularKronecker_bijective_of_projective_homology

Uses 1

Proof usesThe relative universal coefficient theorem below the first non-projective homology, over any commutative ring k

DefinitionThe universal coefficient theorem over a field#

singular cohomology with coefficients in a field k is the dual of singular homology, Hⁿ(X; k) ≃ₗ[k] Module.Dual k (Hₙ(X; k)). It sends a class to the linear form underlying its Kronecker pairing (TopCat.singularCohomologyDualEquiv_apply).

TopCat.singularCohomologyDualEquiv.{w} {k : Type w} [Field k] (X : TopCat) (n : ℕ) :
  ↑(TopCat.singularCohomology (↧k) k (↧k) X n) ≃ₗ[k]
    Module.Dual k ↑(((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) n).obj ↧k).obj X)

Lean

Formalized in Tau Ceti as TopCat.singularCohomologyDualEquiv.

Other forms

The universal coefficient theorem for injective coefficients. Formalized in Tau Ceti as TopCat.singularKroneckerEquiv.

TopCat.singularKroneckerEquiv.{w, v, u, u_1} {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] {R M : C} (X : TopCat)
  (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] [CategoryTheory.Injective M] (n : ℕ) :
  ↑(TopCat.singularCohomology R k M X n) ≃ₗ[k]
    ((AlgebraicTopology.singularHomologyFunctor C n).obj R).obj X ⟶ M

The universal coefficient theorem in degree zero. Formalized in Tau Ceti as TopCat.singularKronecker_bijective_zero.

TopCat.singularKronecker_bijective_zero.{w, v, u, u_1} {C : Type u}
  [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C]
  [CategoryTheory.Limits.HasCoproducts C] {R M : C} (X : TopCat) (k : Type u_1) [Ring k]
  [CategoryTheory.Linear k C] : Function.Bijective ⇑(X.singularKronecker k 0)

The universal coefficient theorem with projective homology, over any commutative ring k. Formalized in Tau Ceti as TopCat.singularKronecker_bijective_of_projective_homology.

TopCat.singularKronecker_bijective_of_projective_homology.{w} {k : Type w} [CommRing k] (X : TopCat)
  (R M : ModuleCat k) [Module.Projective k ↑R]
  [hX :
    ∀ (n : ℕ),
      CategoryTheory.Projective
        (((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) n).obj R).obj X)]
  (n : ℕ) : Function.Bijective ⇑(X.singularKronecker k n)

Sources

• Tau Ceti documentation: TopCat.singularCohomologyDualEquiv
• Source of TopCat.singularCohomologyDualEquiv in TauCeti/AlgebraicTopology/Cohomology/UniversalCoefficient/Field.lean

LeanTopCat.singularCohomologyDualEquiv · TopCat.singularKroneckerEquiv · TopCat.singularKronecker_bijective_zero · TopCat.singularKronecker_bijective_of_projective_homology

Uses 1 · Used by 2

Statement usesThe universal coefficient theorem with projective homology

Used byEuler--Poincaré for cellular chains · The Künneth theorem for cohomology

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.