Cellular

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

TheoremEuler--Poincaré for cellular chains#

For a relative CW complex with finitely many cells through degree n and a finite-dimensional coefficient module M, if there are no (n + 1)-cells, then the alternating sum of the dimensions of the cellular homology groups in degrees at most n is dim M times the alternating count of the cells of dimension at most n.

TauCeti.sum_range_finrank_cellularHomology.{w} {X : Type w} [TopologicalSpace X] {D : Set X}
  (C : Set X) [Topology.RelCWComplex C D] [T2Space X] {k : Type w} [DivisionRing k]
  (M : ModuleCat k) [Module.Finite k ↑M] {n : ℕ}
  (hfinite : ∀ i ≤ n, Finite (Topology.RelCWComplex.cell C i))
  (hn : IsEmpty (Topology.RelCWComplex.cell C (n + 1))) :
  ∑ i ∈ Finset.range (n + 1),
      (-1) ^ i *
        ↑(Module.finrank k ↑(HomologicalComplex.homology (TauCeti.cellularChainComplex C M) i)) =
    ↑(Module.finrank k ↑M) *
      ∑ i ∈ Finset.range (n + 1), (-1) ^ i * ↑(Nat.card (Topology.RelCWComplex.cell C i))

Lean

Formalized in Tau Ceti as TauCeti.sum_range_finrank_cellularHomology.

Other forms

Euler--Poincaré for a space of finite CW type. Formalized in Tau Ceti as TauCeti.eulerChar_eq_finsum_finrank_singularHomology.

TauCeti.eulerChar_eq_finsum_finrank_singularHomology.{w} (X : Type w) [TopologicalSpace X]
  [TauCeti.FiniteCWType X] (k : Type w) [DivisionRing k] :
  TauCeti.eulerChar X =
    ∑ᶠ (i : ℕ),
      (-1) ^ i *
        ↑(Module.finrank k
            ↑(((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) i).obj ↧k).obj ↧X))

Euler--Poincaré for a finite relative CW complex. Formalized in Tau Ceti as TauCeti.homologyEulerChar_cellularChainComplex.

TauCeti.homologyEulerChar_cellularChainComplex.{w} {X : Type w} [TopologicalSpace X] {D : Set X}
  (C : Set X) [Topology.RelCWComplex C D] [T2Space X] {k : Type w} [DivisionRing k]
  (M : ModuleCat k) [Module.Finite k ↑M] [Topology.RelCWComplex.Finite C] :
  HomologicalComplex.homologyEulerChar (TauCeti.cellularChainComplex C M) =
    ↑(Module.finrank k ↑M) * TauCeti.cwEulerChar C

Euler--Poincaré for ordinary singular homology. Formalized in Tau Ceti as TauCeti.finsum_finrank_singularHomology_of_finite_cwComplex.

TauCeti.finsum_finrank_singularHomology_of_finite_cwComplex.{w} {X : Type w} [TopologicalSpace X]
  [T2Space X] (C : Set X) [Topology.CWComplex C] {k : Type w} [DivisionRing k] (M : ModuleCat k)
  [Module.Finite k ↑M] [Topology.RelCWComplex.Finite C] :
  ∑ᶠ (i : ℕ),
      (-1) ^ i *
        ↑(Module.finrank k
            ↑(((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) i).obj M).obj ↧↑C)) =
    ↑(Module.finrank k ↑M) * TauCeti.cwEulerChar C

Euler--Poincaré for relative singular homology. Formalized in Tau Ceti as TauCeti.finsum_finrank_singularHomology_complexBasePair.

TauCeti.finsum_finrank_singularHomology_complexBasePair.{w} {X : Type w} [TopologicalSpace X]
  [T2Space X] {D : Set X} (C : Set X) [Topology.RelCWComplex C D] {k : Type w} [DivisionRing k]
  (M : ModuleCat k) [Module.Finite k ↑M] [Topology.RelCWComplex.Finite C] :
  ∑ᶠ (i : ℕ), (-1) ^ i * ↑(Module.finrank k ↑((TauCeti.complexBasePair C).singularHomology M i)) =
    ↑(Module.finrank k ↑M) * TauCeti.cwEulerChar C

Euler--Poincaré in cohomology for a space of finite CW type. Formalized in Tau Ceti as TauCeti.eulerChar_eq_finsum_finrank_singularCohomology.

TauCeti.eulerChar_eq_finsum_finrank_singularCohomology.{w} (X : Type w) [TopologicalSpace X]
  [TauCeti.FiniteCWType X] (k : Type w) [Field k] :
  TauCeti.eulerChar X =
    ∑ᶠ (i : ℕ), (-1) ^ i * ↑(Module.finrank k ↑(TopCat.singularCohomology (↧k) k (↧k) (↧X) i))

Sources

• Tau Ceti documentation: TauCeti.sum_range_finrank_cellularHomology
• Source of TauCeti.sum_range_finrank_cellularHomology in TauCeti/AlgebraicTopology/Cellular/EulerCharacteristic/Basic.lean

LeanTauCeti.sum_range_finrank_cellularHomology · TauCeti.eulerChar_eq_finsum_finrank_singularHomology · TauCeti.homologyEulerChar_cellularChainComplex · TauCeti.finsum_finrank_singularHomology_of_finite_cwComplex · TauCeti.finsum_finrank_singularHomology_complexBasePair · TauCeti.eulerChar_eq_finsum_finrank_singularCohomology

Uses 4 · Used by 3

Proof usesEuler–Poincaré for cubes · The Mayer–Vietoris isomorphism of a sphere · The relative small-chain theorem · The universal coefficient theorem over a field

Used byThe 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

TheoremThe Morse polynomial identity for a CW pair#

If there are finitely many relative cells through degree n and none in degree n + 1, then in ℕ[X] ∑ᵢ₌₀ⁿ cᵢ dim M · Xⁱ = ∑ᵢ₌₀ⁿ bᵢ Xⁱ + (1 + X) Q, where cᵢ is the number of relative i-cells, bᵢ the dimension of the relative singular homology, and the coefficient of Xⁱ in Q is the rank of the cellular differential in degree i + 1 for i < n, and zero otherwise.

TauCeti.sum_range_monomial_natCard_cell_mul_finrank_eq.{w} {X : Type w} [TopologicalSpace X]
  [T2Space X] {k : Type w} [DivisionRing k] {D : Set X} (C : Set X) [Topology.RelCWComplex C D]
  (M : ModuleCat k) [Module.Finite k ↑M] {n : ℕ}
  (hfinite : ∀ i ≤ n, Finite (Topology.RelCWComplex.cell C i))
  (hn : IsEmpty (Topology.RelCWComplex.cell C (n + 1))) :
  ∑ i ∈ Finset.range (n + 1),
      (Polynomial.monomial i) (Nat.card (Topology.RelCWComplex.cell C i) * Module.finrank k ↑M) =
    ∑ i ∈ Finset.range (n + 1),
        (Polynomial.monomial i)
          (Module.finrank k ↑((TauCeti.complexBasePair C).singularHomology M i)) +
      (1 + Polynomial.X) *
        ∑ i ∈ Finset.range n,
          (Polynomial.monomial i)
            (Module.finrank k
              ↥(ModuleCat.Hom.hom ((TauCeti.cellularChainComplex C M).d (i + 1) i)).range)

Lean

Formalized in Tau Ceti as TauCeti.sum_range_monomial_natCard_cell_mul_finrank_eq.

Other forms

The Morse polynomial identity for a CW complex. Formalized in Tau Ceti as TauCeti.sum_range_monomial_natCard_cell_mul_finrank_eq_of_cwComplex.

TauCeti.sum_range_monomial_natCard_cell_mul_finrank_eq_of_cwComplex.{w} {X : Type w}
  [TopologicalSpace X] [T2Space X] {k : Type w} [DivisionRing k] (C : Set X) [Topology.CWComplex C]
  (M : ModuleCat k) [Module.Finite k ↑M] {n : ℕ}
  (hfinite : ∀ i ≤ n, Finite (Topology.RelCWComplex.cell C i))
  (hn : IsEmpty (Topology.RelCWComplex.cell C (n + 1))) :
  ∑ i ∈ Finset.range (n + 1),
      (Polynomial.monomial i) (Nat.card (Topology.RelCWComplex.cell C i) * Module.finrank k ↑M) =
    ∑ i ∈ Finset.range (n + 1),
        (Polynomial.monomial i)
          (Module.finrank k
            ↑(((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) i).obj M).obj ↧↑C)) +
      (1 + Polynomial.X) *
        ∑ i ∈ Finset.range n,
          (Polynomial.monomial i)
            (Module.finrank k
              ↥(ModuleCat.Hom.hom ((TauCeti.cellularChainComplex C M).d (i + 1) i)).range)

Sources

• Tau Ceti documentation: TauCeti.sum_range_monomial_natCard_cell_mul_finrank_eq
• Source of TauCeti.sum_range_monomial_natCard_cell_mul_finrank_eq in TauCeti/AlgebraicTopology/Cellular/EulerCharacteristic/MorseInequalities.lean

LeanTauCeti.sum_range_monomial_natCard_cell_mul_finrank_eq · TauCeti.sum_range_monomial_natCard_cell_mul_finrank_eq_of_cwComplex

Uses 3

Proof usesThe Mayer–Vietoris isomorphism of a sphere · The Morse polynomial identity (ChainComplex.sum_range_monomial_finrank_X_eq) · The relative small-chain theorem

TheoremThe strong Morse inequalities for a CW pair#

If there are finitely many relative cells through degree n, then bₙ - bₙ₋₁ + ⋯ ± b₀ ≤ (cₙ - cₙ₋₁ + ⋯ ± c₀) · dim M, where bᵢ is the dimension of the relative singular homology and cᵢ the number of relative i-cells.

TauCeti.sum_range_neg_one_pow_mul_finrank_singularHomology_complexBasePair_le.{w} {X : Type w}
  [TopologicalSpace X] [T2Space X] {k : Type w} [DivisionRing k] {D : Set X} (C : Set X)
  [Topology.RelCWComplex C D] (M : ModuleCat k) [Module.Finite k ↑M] {n : ℕ}
  (hfinite : ∀ i ≤ n, Finite (Topology.RelCWComplex.cell C i)) :
  ∑ i ∈ Finset.range (n + 1),
      (-1) ^ (n - i) * ↑(Module.finrank k ↑((TauCeti.complexBasePair C).singularHomology M i)) ≤
    ↑(Module.finrank k ↑M) *
      ∑ i ∈ Finset.range (n + 1), (-1) ^ (n - i) * ↑(Nat.card (Topology.RelCWComplex.cell C i))

Lean

Formalized in Tau Ceti as TauCeti.sum_range_neg_one_pow_mul_finrank_singularHomology_complexBasePair_le.

Other forms

The strong Morse inequalities for a CW complex. Formalized in Tau Ceti as TauCeti.sum_range_neg_one_pow_mul_finrank_singularHomology_le_of_cwComplex.

TauCeti.sum_range_neg_one_pow_mul_finrank_singularHomology_le_of_cwComplex.{w} {X : Type w}
  [TopologicalSpace X] [T2Space X] {k : Type w} [DivisionRing k] (C : Set X) [Topology.CWComplex C]
  (M : ModuleCat k) [Module.Finite k ↑M] {n : ℕ}
  (hfinite : ∀ i ≤ n, Finite (Topology.RelCWComplex.cell C i)) :
  ∑ i ∈ Finset.range (n + 1),
      (-1) ^ (n - i) *
        ↑(Module.finrank k
            ↑(((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) i).obj M).obj ↧↑C)) ≤
    ↑(Module.finrank k ↑M) *
      ∑ i ∈ Finset.range (n + 1), (-1) ^ (n - i) * ↑(Nat.card (Topology.RelCWComplex.cell C i))

Sources

• Tau Ceti documentation: TauCeti.sum_range_neg_one_pow_mul_finrank_singularHomology_complexBasePair_le
• Source of TauCeti.sum_range_neg_one_pow_mul_finrank_singularHomology_complexBasePair_le in TauCeti/AlgebraicTopology/Cellular/EulerCharacteristic/MorseInequalities.lean

LeanTauCeti.sum_range_neg_one_pow_mul_finrank_singularHomology_complexBasePair_le · TauCeti.sum_range_neg_one_pow_mul_finrank_singularHomology_le_of_cwComplex

Uses 3 · Used by 3

Proof usesThe Mayer–Vietoris isomorphism of a sphere · The relative small-chain theorem · The strong Morse inequalities (ChainComplex.sum_range_neg_one_pow_mul_finrank_homology_le)

Used byThe 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

TheoremThe weak Morse inequality for a CW pair#

In a degree with finitely many relative cells, the relative singular homology has dimension at most the number of cells times dim M.

TauCeti.finrank_singularHomology_complexBasePair_le.{w} {X : Type w} [TopologicalSpace X]
  [T2Space X] {k : Type w} [DivisionRing k] {D : Set X} (C : Set X) [Topology.RelCWComplex C D]
  (M : ModuleCat k) [Module.Finite k ↑M] (n : ℕ) [Finite (Topology.RelCWComplex.cell C n)] :
  Module.finrank k ↑((TauCeti.complexBasePair C).singularHomology M n) ≤
    Nat.card (Topology.RelCWComplex.cell C n) * Module.finrank k ↑M

Lean

Formalized in Tau Ceti as TauCeti.finrank_singularHomology_complexBasePair_le.

Other forms

The weak Morse inequality for a CW complex. Formalized in Tau Ceti as TauCeti.finrank_singularHomology_le_of_cwComplex.

TauCeti.finrank_singularHomology_le_of_cwComplex.{w} {X : Type w} [TopologicalSpace X] [T2Space X]
  {k : Type w} [DivisionRing k] (C : Set X) [Topology.CWComplex C] (M : ModuleCat k)
  [Module.Finite k ↑M] (n : ℕ) [Finite (Topology.RelCWComplex.cell C n)] :
  Module.finrank k ↑(((AlgebraicTopology.singularHomologyFunctor (ModuleCat k) n).obj M).obj ↧↑C) ≤
    Nat.card (Topology.RelCWComplex.cell C n) * Module.finrank k ↑M

Sources

• Tau Ceti documentation: TauCeti.finrank_singularHomology_complexBasePair_le
• Source of TauCeti.finrank_singularHomology_complexBasePair_le in TauCeti/AlgebraicTopology/Cellular/EulerCharacteristic/MorseInequalities.lean

LeanTauCeti.finrank_singularHomology_complexBasePair_le · TauCeti.finrank_singularHomology_le_of_cwComplex

Uses 3 · Used by 3

Proof usesThe Mayer–Vietoris isomorphism of a sphere · The relative small-chain theorem · The weak Morse inequality

Used byThe 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

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.