Singular

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

TheoremBrouwer's fixed-point theorem#

every continuous self-map of the disk Dⁿ has a fixed point.

TauCeti.brouwerFixedPoint_topCatDisk.{w} (n : ℕ) (f : TopCat.disk n ⟶ TopCat.disk n) :
  ∃ x, Function.IsFixedPt (⇑(CategoryTheory.ConcreteCategory.hom f)) x

Lean

Formalized in Tau Ceti as TauCeti.brouwerFixedPoint_topCatDisk.

Other forms

Brouwer's fixed-point theorem for closed balls. Formalized in Tau Ceti as TauCeti.brouwerFixedPoint_closedBall.

TauCeti.brouwerFixedPoint_closedBall.{u_1} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [FiniteDimensional ℝ E] (x : E) {r : ℝ} (hr : 0 ≤ r)
  (f : C(↑(Metric.closedBall x r), ↑(Metric.closedBall x r))) : ∃ y, Function.IsFixedPt (⇑f) y

Brouwer's fixed-point theorem for compact convex sets. Formalized in Tau Ceti as TauCeti.brouwerFixedPoint_compactConvex.

TauCeti.brouwerFixedPoint_compactConvex.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] [FiniteDimensional ℝ E] {C : Set E} (hC : IsCompact C) (hconv : Convex ℝ C)
  (hne : C.Nonempty) (f : C(↑C, ↑C)) : ∃ x, Function.IsFixedPt (⇑f) x

Brouwer's fixed-point theorem for compact convex sets, for a function on the ambient space. Formalized in Tau Ceti as TauCeti.brouwerFixedPoint_compactConvex_continuousOn.

TauCeti.brouwerFixedPoint_compactConvex_continuousOn.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] {C : Set E} [FiniteDimensional ℝ ↥(Submodule.span ℝ C)] (hC : IsCompact C)
  (hconv : Convex ℝ C) (hne : C.Nonempty) {f : E → E} (hf : ContinuousOn f C)
  (hfC : Set.MapsTo f C C) : ∃ x ∈ C, Function.IsFixedPt f x

Brouwer's fixed-point theorem for compact convex sets in a finite-dimensional subspace. Formalized in Tau Ceti as TauCeti.brouwerFixedPoint_compactConvex_finiteSpan.

TauCeti.brouwerFixedPoint_compactConvex_finiteSpan.{u_1} {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace ℝ E] (V : Submodule ℝ E) [FiniteDimensional ℝ ↥V] {C : Set E} (hCV : C ⊆ ↑V)
  (hC : IsCompact C) (hconv : Convex ℝ C) (hne : C.Nonempty) (f : C(↑C, ↑C)) :
  ∃ x, Function.IsFixedPt (⇑f) x

Sources

• Tau Ceti documentation: TauCeti.brouwerFixedPoint_topCatDisk
• Source of TauCeti.brouwerFixedPoint_topCatDisk in TauCeti/AlgebraicTopology/Singular/BrouwerFixedPoint.lean

LeanTauCeti.brouwerFixedPoint_topCatDisk · TauCeti.brouwerFixedPoint_closedBall · TauCeti.brouwerFixedPoint_compactConvex · TauCeti.brouwerFixedPoint_compactConvex_continuousOn · TauCeti.brouwerFixedPoint_compactConvex_finiteSpan

Uses 1

Proof usesThe no-retraction theorem

TheoremThe cubical Eilenberg–Zilber theorem#

the cross product of normalized cubical chains N(X; k) ⊗ N(Y; k) ⟶ N(X × Y; k) is a quasi-isomorphism.

TauCeti.quasiIso_cubicalCrossProduct.{u} (k : Type u) [CommRing k] (X Y : TopCat) :
  QuasiIso (TauCeti.cubicalCrossProduct k X Y)

Lean

Formalized in Tau Ceti as TauCeti.quasiIso_cubicalCrossProduct.

Sources

• Tau Ceti documentation: TauCeti.quasiIso_cubicalCrossProduct
• Source of TauCeti.quasiIso_cubicalCrossProduct in TauCeti/AlgebraicTopology/Singular/Cubical/Kunneth.lean

LeanTauCeti.quasiIso_cubicalCrossProduct

Uses 1 · Used by 1

Proof usesThe Eilenberg–Zilber theorem for singular chains

Used byThe Künneth theorem for cubical homology

DefinitionThe Eilenberg–Zilber theorem for singular chains#

the Alexander–Whitney map C(X × Y; R ⊗ S) ⟶ C(X; R) ⊗ C(Y; S) is a chain homotopy equivalence, with homotopy inverse the shuffle map.

TopCat.eilenbergZilberHomotopyEquiv.{w, v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalCategory C]
  [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.Limits.HasCoproducts C]
  [∀ (T : C) (J : Type w),
      CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J)
        (CategoryTheory.MonoidalCategory.tensorLeft T)]
  [∀ (T : C) (J : Type w),
      CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J)
        (CategoryTheory.MonoidalCategory.tensorRight T)]
  (X Y : TopCat) (R S : C) :
  HomotopyEquiv
    ((TopCat.toSSet.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).chainComplex
      (CategoryTheory.MonoidalCategoryStruct.tensorObj R S))
    (CategoryTheory.MonoidalCategoryStruct.tensorObj ((TopCat.toSSet.obj X).chainComplex R)
      ((TopCat.toSSet.obj Y).chainComplex S))

Lean

Formalized in Tau Ceti as TopCat.eilenbergZilberHomotopyEquiv.

Sources

• Tau Ceti documentation: TopCat.eilenbergZilberHomotopyEquiv
• Source of TopCat.eilenbergZilberHomotopyEquiv in TauCeti/AlgebraicTopology/Singular/EilenbergZilber.lean

LeanTopCat.eilenbergZilberHomotopyEquiv

Used by 4

Used byThe Künneth short exact sequence over a hereditary commutative ring splits · The Künneth theorem for cohomology · The cubical Eilenberg–Zilber theorem · The Künneth theorem for cubical homology

TheoremThe Künneth theorem for cubical homology#

if the cycles of the normalized cubical chain complexes split off their terms and their homology splits off the cycles, the Künneth map ⨁_{p + q = n} Hₚ(X; k) ⊗ H_q(Y; k) ⟶ Hₙ(X × Y; k) is an isomorphism. This is the Künneth theorem for the chain complexes N(X; k) and N(Y; k), transported along the cubical Eilenberg–Zilber quasi-isomorphism.

TauCeti.isIso_cubicalHomologyKunneth.{u} (k : Type u) [CommRing k] (X Y : TopCat)
  [∀ (p : ℕ),
      CategoryTheory.IsSplitMono
        (HomologicalComplex.iCycles ((TauCeti.normalizedCubicalChainComplex k).obj X) p)]
  [∀ (p : ℕ),
      CategoryTheory.IsSplitEpi
        (HomologicalComplex.homologyπ ((TauCeti.normalizedCubicalChainComplex k).obj X) p)]
  [∀ (q : ℕ),
      CategoryTheory.IsSplitMono
        (HomologicalComplex.iCycles ((TauCeti.normalizedCubicalChainComplex k).obj Y) q)]
  [∀ (q : ℕ),
      CategoryTheory.IsSplitEpi
        (HomologicalComplex.homologyπ ((TauCeti.normalizedCubicalChainComplex k).obj Y) q)]
  (n : ℕ) : CategoryTheory.IsIso (TauCeti.cubicalHomologyKunneth k X Y n)

Lean

Formalized in Tau Ceti as TauCeti.isIso_cubicalHomologyKunneth.

Other forms

The Künneth theorem for cubical homology over a semisimple ring, for instance a field. Formalized in Tau Ceti as TauCeti.isIso_cubicalHomologyKunneth_of_isSemisimpleRing.

TauCeti.isIso_cubicalHomologyKunneth_of_isSemisimpleRing.{u} (k : Type u) [CommRing k]
  (X Y : TopCat) [IsSemisimpleRing k] (n : ℕ) :
  CategoryTheory.IsIso (TauCeti.cubicalHomologyKunneth k X Y n)

The Künneth theorem for cubical homology with projective homology. Formalized in Tau Ceti as TauCeti.isIso_cubicalHomologyKunneth_of_projective.

TauCeti.isIso_cubicalHomologyKunneth_of_projective.{u} (k : Type u) [CommRing k] (X Y : TopCat)
  [NoZeroDivisors k] [IsPrincipalIdealRing k]
  [∀ (p : ℕ),
      CategoryTheory.Projective
        (HomologicalComplex.homology ((TauCeti.normalizedCubicalChainComplex k).obj X) p)]
  [∀ (q : ℕ),
      CategoryTheory.Projective
        (HomologicalComplex.homology ((TauCeti.normalizedCubicalChainComplex k).obj Y) q)]
  (n : ℕ) : CategoryTheory.IsIso (TauCeti.cubicalHomologyKunneth k X Y n)

The Künneth theorem for split singular chains. Formalized in Tau Ceti as TopCat.isIso_singularHomologyKunneth.

TopCat.isIso_singularHomologyKunneth.{w} {k : Type w} [CommRing k] (X Y : TopCat)
  (M N : ModuleCat k)
  [∀ (p : ℕ),
      CategoryTheory.IsSplitMono
        (HomologicalComplex.iCycles ((TopCat.toSSet.obj X).chainComplex M) p)]
  [∀ (p : ℕ),
      CategoryTheory.IsSplitEpi
        (HomologicalComplex.homologyπ ((TopCat.toSSet.obj X).chainComplex M) p)]
  [∀ (q : ℕ),
      CategoryTheory.IsSplitMono
        (HomologicalComplex.iCycles ((TopCat.toSSet.obj Y).chainComplex N) q)]
  [∀ (q : ℕ),
      CategoryTheory.IsSplitEpi
        (HomologicalComplex.homologyπ ((TopCat.toSSet.obj Y).chainComplex N) q)]
  (n : ℕ) : CategoryTheory.IsIso (X.singularHomologyKunneth Y M N n)

The Künneth theorem with projective homology. Formalized in Tau Ceti as TopCat.isIso_singularHomologyKunneth_of_projective.

TopCat.isIso_singularHomologyKunneth_of_projective.{w} {k : Type w} [CommRing k] (X Y : TopCat)
  (M N : ModuleCat k)
  [∀ (p : ℕ),
      CategoryTheory.IsSplitMono
        (HomologicalComplex.iCycles ((TopCat.toSSet.obj X).chainComplex M) p)]
  [hX :
    ∀ (p : ℕ),
      CategoryTheory.Projective
        (((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) p).obj M).obj X)]
  [∀ (q : ℕ),
      CategoryTheory.IsSplitMono
        (HomologicalComplex.iCycles ((TopCat.toSSet.obj Y).chainComplex N) q)]
  [hY :
    ∀ (q : ℕ),
      CategoryTheory.Projective
        (((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) q).obj N).obj Y)]
  (n : ℕ) : CategoryTheory.IsIso (X.singularHomologyKunneth Y M N n)

The Künneth theorem with projective homology over any commutative ring. Formalized in Tau Ceti as TopCat.isIso_singularHomologyKunneth_of_projective_homology.

TopCat.isIso_singularHomologyKunneth_of_projective_homology.{w} {k : Type w} [CommRing k]
  (X Y : TopCat) (M N : ModuleCat k) [Module.Projective k ↑M] [Module.Projective k ↑N]
  [hX :
    ∀ (p : ℕ),
      CategoryTheory.Projective
        (((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) p).obj M).obj X)]
  [hY :
    ∀ (q : ℕ),
      CategoryTheory.Projective
        (((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) q).obj N).obj Y)]
  (n : ℕ) : CategoryTheory.IsIso (X.singularHomologyKunneth Y M N n)

Sources

• Tau Ceti documentation: TauCeti.isIso_cubicalHomologyKunneth
• Source of TauCeti.isIso_cubicalHomologyKunneth in TauCeti/AlgebraicTopology/Singular/Cubical/Kunneth.lean

LeanTauCeti.isIso_cubicalHomologyKunneth · TauCeti.isIso_cubicalHomologyKunneth_of_isSemisimpleRing · TauCeti.isIso_cubicalHomologyKunneth_of_projective · TopCat.isIso_singularHomologyKunneth · TopCat.isIso_singularHomologyKunneth_of_projective · TopCat.isIso_singularHomologyKunneth_of_projective_homology

Uses 3 · Used by 1

Proof usesThe cubical Eilenberg–Zilber theorem · The Eilenberg–Zilber theorem for singular chains · The Künneth theorem for split complexes

Used byThe Künneth theorem for cohomology

TheoremThe Mayer–Vietoris isomorphism of a sphere#

The reduced Mayer–Vietoris connecting morphism Hₖ₊₁(S) ⟶ H_redₖ(S ∖ {p, -p}) of the cover of the unit sphere S by the complements of p and -p is an isomorphism in every degree, since both complements are contractible.

TauCeti.isIso_reducedMayerVietorisδ_sphere.{w, v, u} {C : Type u} [CategoryTheory.Category.{v, u} C]
  [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {E : Type w}
  [NormedAddCommGroup E] [NormedSpace ℝ E] (p : ↑(Metric.sphere 0 1)) (k : ℕ) :
  CategoryTheory.IsIso (TopCat.reducedMayerVietorisδ R ⋯ ⋯ ⋯ k)

Lean

Formalized in Tau Ceti as TauCeti.isIso_reducedMayerVietorisδ_sphere.

Sources

• Tau Ceti documentation: TauCeti.isIso_reducedMayerVietorisδ_sphere
• Source of TauCeti.isIso_reducedMayerVietorisδ_sphere in TauCeti/AlgebraicTopology/Singular/Sphere.lean

LeanTauCeti.isIso_reducedMayerVietorisδ_sphere

Used by 19

Used byThe Hurewicz theorem · The relative Hurewicz isomorphism for highly connected spaces · The top homology of a compact manifold is the module of parallel families of local classes · Euler--Poincaré for cellular chains · The Morse polynomial identity for a CW pair · The strong Morse inequalities for a CW pair · The weak Morse inequality for a CW pair · The cellular chains of a contractible free cover are a projective resolution of the trivial representation of G over R · The no-retraction theorem · A crosscut of a simply connected domain has exactly two sides · The Jordan–Brouwer separation theorem · Thurston's Euler class inequality · Yazdi's theorem refutes the Euler class one conjecture · The Morse polynomial identity (TauCeti.IsMorse.exists_sum_range_monomial_eq_add_mul) · The strong Morse inequalities (TauCeti.IsMorse.sum_range_neg_one_pow_mul_finrank_singularHomology_le) · The weak Morse inequalities · Cerf's theorem as a count of path components · Under Gabai's theorem, a generator of H₂(S¹ × S²; ℤ) has minimal genus 0 · Yasui's theorem spelled out

TheoremThe no-retraction theorem#

the boundary sphere ∂Dⁿ of the disk is not a retract of the disk Dⁿ. That is, there are no maps i : ∂Dⁿ ⟶ Dⁿ and r : Dⁿ ⟶ ∂Dⁿ with i ≫ r = 𝟙; in particular the boundary inclusion TopCat.diskBoundaryInclusion n has no retraction. This includes n = 0, where the boundary is empty.

TauCeti.noRetraction_diskBoundary.{w} (n : ℕ) :
  IsEmpty (CategoryTheory.Retract (TopCat.diskBoundary n) (TopCat.disk n))

Lean

Formalized in Tau Ceti as TauCeti.noRetraction_diskBoundary.

Sources

• Tau Ceti documentation: TauCeti.noRetraction_diskBoundary
• Source of TauCeti.noRetraction_diskBoundary in TauCeti/AlgebraicTopology/Singular/BrouwerFixedPoint.lean

LeanTauCeti.noRetraction_diskBoundary

Uses 1 · Used by 1

Proof usesThe Mayer–Vietoris isomorphism of a sphere

Used byBrouwer's fixed-point theorem

TheoremThe relative small-chain theorem#

Restricting the singular pair of a topological pair to the simplices subordinate to an open cover of the ambient space does not change relative homology.

TopPair.isIso_homologyMap_restrictι_smallSingularSubcomplex.{w, v, u, u_1} {A : Type u}
  [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A]
  [CategoryTheory.Abelian A] (R : A) (P : TopPair) {ι : Type u_1} (U : ι → Set ↑TopPair.fst)
  (hU : ∀ (i : ι), IsOpen (U i)) (hcov : ⋃ i, U i = Set.univ) (n : ℕ) :
  CategoryTheory.IsIso
    (SSetPair.homologyMap ((TopPair.toSSetPair.obj P).restrictι (P.smallSingularSubcomplex U)) R n)

Lean

Formalized in Tau Ceti as TopPair.isIso_homologyMap_restrictι_smallSingularSubcomplex.

Sources

• Tau Ceti documentation: TopPair.isIso_homologyMap_restrictι_smallSingularSubcomplex
• Source of TopPair.isIso_homologyMap_restrictι_smallSingularSubcomplex in TauCeti/AlgebraicTopology/Singular/Subdivision/Small/Relative.lean

LeanTopPair.isIso_homologyMap_restrictι_smallSingularSubcomplex

Used by 16

Used byExcision of a set with closure in the interior of the subspace · The Hurewicz theorem · The relative Hurewicz isomorphism for highly connected spaces · The top homology of a compact manifold is the module of parallel families of local classes · Euler--Poincaré for cellular chains · The Morse polynomial identity for a CW pair · The strong Morse inequalities for a CW pair · The weak Morse inequality for a CW pair · The cellular chains of a contractible free cover are a projective resolution of the trivial representation of G over R · Thurston's Euler class inequality · Yazdi's theorem refutes the Euler class one conjecture · The Morse polynomial identity (TauCeti.IsMorse.exists_sum_range_monomial_eq_add_mul) · The strong Morse inequalities (TauCeti.IsMorse.sum_range_neg_one_pow_mul_finrank_singularHomology_le) · The weak Morse inequalities · Under Gabai's theorem, a generator of H₂(S¹ × S²; ℤ) has minimal genus 0 · Yasui's theorem spelled out

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.