English
The injection inr: N → M×N and the projection fst: M×N → M form an exact pair: im(inr) = ker(fst).
Русский
Встраивание inr: N → M×N и проекция fst: M×N → M образуют точную пару: im(inr) = ker(fst).
LaTeX
$$$$ \\operatorname{Im}(\\operatorname{inr}) = \\ker(\\operatorname{fst}). $$$$
Lean4
/-- Equivalent characterizations of split exact sequences. Also known as the **Splitting lemma**. -/
theorem split_tfae {R M N P} [Semiring R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N]
[Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (h : Function.Exact f g) (hf : Function.Injective f)
(hg : Function.Surjective g) :
List.TFAE
[∃ l, g ∘ₗ l = LinearMap.id, ∃ l, l ∘ₗ f = LinearMap.id,
∃ e : N ≃ₗ[R] M × P, f = e.symm ∘ₗ LinearMap.inl R M P ∧ g = LinearMap.snd R M P ∘ₗ e] :=
by
tfae_have 1 ↔ 3 := by simpa using (h.splitSurjectiveEquiv hf).nonempty_congr
tfae_have 2 ↔ 3 := by simpa using (h.splitInjectiveEquiv hg).nonempty_congr
tfae_finish
