English
Let 0 → N → M → P → 0 be a short exact sequence of modules over R. Then the length of M equals the sum of the lengths of N and P: length_R(M) = length_R(N) + length_R(P).
Русский
Пусть 0 → N → M → P → 0 — краткая точная последовательность модулей над кольцом R. Тогда длина M равна сумме длин N и P:
length_R(M) = length_R(N) + length_R(P).
LaTeX
$$$\operatorname{length}_R(M) = \operatorname{length}_R(N) + \operatorname{length}_R(P)$$$
Lean4
/-- Length is additive in exact sequences. -/
theorem length_eq_add_of_exact : Module.length R M = Module.length R N + Module.length R P :=
by
by_cases hP : IsFiniteLength R P
· by_cases hN : IsFiniteLength R N
· obtain ⟨s, hs₁, hs₂⟩ := isFiniteLength_iff_exists_compositionSeries.mp hP
obtain ⟨t, ht₁, ht₂⟩ := isFiniteLength_iff_exists_compositionSeries.mp hN
let s' : CompositionSeries (Submodule R M) := s.map ⟨Submodule.comap g, Submodule.comap_covBy_of_surjective hg⟩
let t' : CompositionSeries (Submodule R M) := t.map ⟨Submodule.map f, Submodule.map_covBy_of_injective hf⟩
have hfg : Submodule.map f ⊤ = Submodule.comap g ⊥ := by
rw [Submodule.map_top, Submodule.comap_bot, LinearMap.exact_iff.mp H]
let r := t'.smash s' (by simpa [s', t', hs₁, ht₂] using hfg)
rw [← Module.length_compositionSeries s hs₁ hs₂, ← Module.length_compositionSeries t ht₁ ht₂, ←
Module.length_compositionSeries r (by simpa [r, t', ht₁, -Submodule.map_bot] using Submodule.map_bot f)
(by simpa [r, s', hs₂, -Submodule.comap_top] using Submodule.comap_top g)]
simp_rw [r, RelSeries.smash_length, Nat.cast_add, s', t', RelSeries.map_length]
· have := mt (IsFiniteLength.of_injective · hf) hN
rw [← Module.length_ne_top_iff, ne_eq, not_not] at hN this
rw [hN, this, top_add]
· have := mt (IsFiniteLength.of_surjective · hg) hP
rw [← Module.length_ne_top_iff, ne_eq, not_not] at hP this
rw [hP, this, add_top]
