Theorems · Theorem · category theory

Module.sum_neg_one_pow_finrank_eq_zero_of_exact

∀ {k : Type u_1} [inst : DivisionRing k] {n : ℕ} (V : Fin (n + 2) → Type u_2)
  [inst_1 : (i : Fin (n + 2)) → AddCommGroup (V i)] [inst_2 : (i : Fin (n + 2)) → Module k (V i)]
  [∀ (i : Fin (n + 2)), FiniteDimensional k (V i)] (f : (i : Fin (n + 1)) → V i.castSucc →ₗ[k] V i.succ),
  Function.Injective ⇑(f 0) →
    (∀ (i : Fin n), Function.Exact ⇑(f i.castSucc) ⇑(f i.succ)) →
      Function.Surjective ⇑(f (Fin.last n)) → ∑ i, (-1) ^ ↑i * ↑(Module.finrank k (V i)) = 0

The Euler characteristic of a finite exact sequence is zero.

Defined in

Mathlib.Algebra.Exact.Sequence

Cited by

0 results in Mathlib

Foundations

Depth 118 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DivisionRingAddCommGroupModuleFiniteDimensional