Euler characteristic of homological complexes

The Euler characteristic is defined using the ComplexShape.EulerCharSigns typeclass, which provides the alternating signs for each index. This allows the definition to work uniformly for chain complexes, cochain complexes, and complexes with other index types.

The definitions work on graded objects, with the homological complex versions defined as abbreviations that apply the graded object versions to C.X and C.homology.

Junk values

These definitions may have junk values from finsum (0 for infinite support) and Module.finrank (0 for modules not free of finite rank).

Main definitions

• ComplexShape.EulerCharSigns: Typeclass providing alternating signs for Euler characteristic
• GradedObject.eulerChar: The Euler characteristic of a graded object using finsum
• GradedObject.finrankSupport: Indices where Module.finrank is nonzero
• HomologicalComplex.eulerChar: The Euler characteristic using finsum
• HomologicalComplex.homologyEulerChar: The homological Euler characteristic using finsum

Main results

• GradedObject.eulerChar_eq_sum_finSet_of_finrankSupport_subset: The finsum equals the finite sum when the graded object has finite support contained in the given set
• HomologicalComplex.eulerChar_eq_sum_finSet_of_finrankSupport_subset: The finsum equals the finite sum when the complex has finite support contained in the given set
• HomologicalComplex.homologyEulerChar_eq_sum_finSet_of_finrankSupport_subset: The finsum homological Euler characteristic equals the finite sum when homology has finite support

class ComplexShape.EulerCharSigns {ι : Type u_1} (c : ComplexShape ι) : Type u_1

Signs for terms of Euler characteristic on complexes.

• χ : ι → ℤˣ

  The sign for each index

• χ_next {i j : ι} (h : c.Rel i j) : χ c j = -χ c i

  Signs alternate along relations in the complex shape

@[reducible, inline]

abbrev ComplexShape.χ {ι : Type u_1} (c : ComplexShape ι) [c.EulerCharSigns] : ι → ℤˣ

The sign at index i for Euler characteristic computations.

Equations

• c.χ = ComplexShape.EulerCharSigns.χ c

theorem ComplexShape.χ_next {ι : Type u_1} (c : ComplexShape ι) [c.EulerCharSigns] {i j : ι} (h : c.Rel i j) : c.χ j = -c.χ i

Signs alternate in the forward direction of the complex shape.

theorem ComplexShape.χ_prev {ι : Type u_1} (c : ComplexShape ι) [c.EulerCharSigns] {i j : ι} (h : c.Rel i j) : c.χ i = -c.χ j

Signs alternate in the backward direction of the complex shape.

instance ComplexShape.eulerCharSignsUpInt : (up ℤ).EulerCharSigns

Equations

• ComplexShape.eulerCharSignsUpInt = { χ := Int.negOnePow, χ_next := @ComplexShape.eulerCharSignsUpInt._proof_1 }

@[simp]

theorem ComplexShape.eulerCharSignsUpInt_χ (n : ℤ) : EulerCharSigns.χ (up ℤ) n = n.negOnePow

instance ComplexShape.eulerCharSignsDownInt : (down ℤ).EulerCharSigns

Equations

• ComplexShape.eulerCharSignsDownInt = { χ := Int.negOnePow, χ_next := @ComplexShape.eulerCharSignsDownInt._proof_1 }

@[simp]

theorem ComplexShape.eulerCharSignsDownInt_χ (n : ℤ) : EulerCharSigns.χ (down ℤ) n = n.negOnePow

instance ComplexShape.eulerCharSignsUpNat : (up ℕ).EulerCharSigns

Equations

• ComplexShape.eulerCharSignsUpNat = { χ := fun (n : ℕ) => (-1) ^ n, χ_next := @ComplexShape.eulerCharSignsUpNat._proof_1 }

@[simp]

theorem ComplexShape.eulerCharSignsUpNat_χ (n : ℕ) : EulerCharSigns.χ (up ℕ) n = (-1) ^ n

instance ComplexShape.eulerCharSignsDownNat : (down ℕ).EulerCharSigns

Equations

• ComplexShape.eulerCharSignsDownNat = { χ := fun (n : ℕ) => (-1) ^ n, χ_next := @ComplexShape.eulerCharSignsDownNat._proof_1 }

@[simp]

theorem ComplexShape.eulerCharSignsDownNat_χ (n : ℕ) : EulerCharSigns.χ (down ℕ) n = (-1) ^ n

def GradedObject.finrankSupport {R : Type u_1} [Ring R] {ι : Type u_2} (X : CategoryTheory.GradedObject ι (ModuleCat R)) : Set ι

The support of a graded object with respect to finite rank: the set of indices where the rank is nonzero.

Equations

• GradedObject.finrankSupport X = Function.support fun (i : ι) => Module.finrank R ↑(X i)

theorem GradedObject.finrankSupport_subset_iff {R : Type u_1} [Ring R] {ι : Type u_2} (X : CategoryTheory.GradedObject ι (ModuleCat R)) (s : Set ι) : finrankSupport X ⊆ s ↔ ∀ i ∉ s, Module.finrank R ↑(X i) = 0

The finite rank support is contained in a set if and only if the rank vanishes outside that set.

noncomputable def GradedObject.eulerChar {R : Type u_1} [Ring R] {ι : Type u_2} (c : ComplexShape ι) [c.EulerCharSigns] (X : CategoryTheory.GradedObject ι (ModuleCat R)) : ℤ

The Euler characteristic of a graded object as a sum over all indices. The sign at each index is determined by the ComplexShape.EulerCharSigns instance. Defaults to 0 if the support of the ranks of the objects of X is infinite.

Equations

• GradedObject.eulerChar c X = ∑ᶠ (i : ι), ↑(c.χ i) * ↑(Module.finrank R ↑(X i))

theorem GradedObject.eulerChar_eq_sum_finSet_of_finrankSupport_subset {R : Type u_1} [Ring R] {ι : Type u_2} (c : ComplexShape ι) [c.EulerCharSigns] (X : CategoryTheory.GradedObject ι (ModuleCat R)) (indices : Finset ι) (h_support : finrankSupport X ⊆ ↑indices) : eulerChar c X = ∑ i ∈ indices, ↑(c.χ i) * ↑(Module.finrank R ↑(X i))

If a graded object has finite rank support contained in a finite set, the finsum Euler characteristic equals the finite sum over that set.

@[reducible, inline]

noncomputable abbrev HomologicalComplex.eulerChar {R : Type u_1} [Ring R] {ι : Type u_2} {c : ComplexShape ι} [c.EulerCharSigns] (C : HomologicalComplex (ModuleCat R) c) : ℤ

The Euler characteristic of a homological complex as a sum over all indices using finsum. The sign at each index is determined by the ComplexShape.EulerCharSigns instance. Defaults to 0 if the support of the ranks is infinite.

Equations

• C.eulerChar = GradedObject.eulerChar c C.X

@[reducible, inline]

noncomputable abbrev HomologicalComplex.homologyEulerChar {R : Type u_1} [Ring R] {ι : Type u_2} {c : ComplexShape ι} [c.EulerCharSigns] (C : HomologicalComplex (ModuleCat R) c) [∀ (i : ι), C.HasHomology i] : ℤ

The homological Euler characteristic as a sum over all indices using finsum. This is the Euler characteristic computed from the homology groups rather than the original complex. Defaults to 0 if the support of the ranks is infinite.

Equations

• C.homologyEulerChar = GradedObject.eulerChar c fun (i : ι) => C.homology i

theorem HomologicalComplex.eulerChar_eq_sum_finSet_of_finrankSupport_subset {R : Type u_1} [Ring R] {ι : Type u_2} {c : ComplexShape ι} [c.EulerCharSigns] (C : HomologicalComplex (ModuleCat R) c) (indices : Finset ι) (h_support : GradedObject.finrankSupport C.X ⊆ ↑indices) : C.eulerChar = ∑ i ∈ indices, ↑(c.χ i) * ↑(Module.finrank R ↑(C.X i))

If a complex has finite rank support contained in a finite set, the finsum Euler characteristic equals the finite sum over that set.

theorem HomologicalComplex.homologyEulerChar_eq_sum_finSet_of_finrankSupport_subset {R : Type u_1} [Ring R] {ι : Type u_2} {c : ComplexShape ι} [c.EulerCharSigns] (C : HomologicalComplex (ModuleCat R) c) [∀ (i : ι), C.HasHomology i] (indices : Finset ι) (h_support : (GradedObject.finrankSupport fun (i : ι) => C.homology i) ⊆ ↑indices) : C.homologyEulerChar = ∑ i ∈ indices, ↑(c.χ i) * ↑(Module.finrank R ↑(C.homology i))

If homology has finite rank support contained in a finite set, the finsum homological Euler characteristic equals the finite sum over that set.