Exactness of sequences #
In this file we provide some API for handling exact sequences.
Main definitions / results: #
Module.sum_neg_one_pow_finrank_eq_zero_of_exact: the Euler characteristic of a finite exact sequence is zero.
TODO #
Write a simproc to generate unrolled, universe-polymorphic versions of
Module.sum_neg_one_pow_finrank_eq_zero_of_exact on the fly and so obviate the need for
Module.sum_neg_one_pow_finrank_eq_zero_of_exact_six.
theorem
Module.sum_neg_one_pow_finrank_eq_zero_of_exact
{k : Type u_1}
[DivisionRing k]
{n : ℕ}
(V : Fin (n + 2) → Type u_2)
[(i : Fin (n + 2)) → AddCommGroup (V i)]
[(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)
(inj : Function.Injective ⇑(f 0))
(h_exact : ∀ (i : Fin n), Function.Exact ⇑(f i.castSucc) ⇑(f i.succ))
(surj : Function.Surjective ⇑(f (Fin.last n)))
:
The Euler characteristic of a finite exact sequence is zero.
theorem
Module.sum_neg_one_pow_finrank_eq_zero_of_exact_six
{k : Type u_1}
[DivisionRing k]
{V₀ : Type u₀}
[AddCommGroup V₀]
[Module k V₀]
[FiniteDimensional k V₀]
{V₁ : Type u₁}
[AddCommGroup V₁]
[Module k V₁]
[FiniteDimensional k V₁]
{V₂ : Type u₂}
[AddCommGroup V₂]
[Module k V₂]
[FiniteDimensional k V₂]
{V₃ : Type u₃}
[AddCommGroup V₃]
[Module k V₃]
[FiniteDimensional k V₃]
{V₄ : Type u₄}
[AddCommGroup V₄]
[Module k V₄]
[FiniteDimensional k V₄]
{V₅ : Type u₅}
[AddCommGroup V₅]
[Module k V₅]
[FiniteDimensional k V₅]
(f₀ : V₀ →ₗ[k] V₁)
(f₁ : V₁ →ₗ[k] V₂)
(f₂ : V₂ →ₗ[k] V₃)
(f₃ : V₃ →ₗ[k] V₄)
(f₄ : V₄ →ₗ[k] V₅)
(inj : Function.Injective ⇑f₀)
(exact₁ : Function.Exact ⇑f₀ ⇑f₁)
(exact₂ : Function.Exact ⇑f₁ ⇑f₂)
(exact₃ : Function.Exact ⇑f₂ ⇑f₃)
(exact₄ : Function.Exact ⇑f₃ ⇑f₄)
(surj : Function.Surjective ⇑f₄)
:
This is an unrolled, universe-polymorphic version of
Module.sum_neg_one_pow_finrank_eq_zero_of_exact. This special case exists because of the role that
this lemma plays in the proof of LinearMap.index_comp.
In theory one could write a simproc which conjured up this lemma for a sequence of any length and
then one would not need to have this special-case lemma at all.