English
Equivalent characterizations of split exact sequences: existence of l with g∘l=id, existence of l with l∘f=id, and existence of an isomorphism N ≅ M×P with f,g recovered from it.
Русский
Эквивалентные характеристики распадающейся точной последовательности: существование l с g∘l = id, существование l с l∘f = id и существование изоморфизма N ≅ M×P, из которого восстанавливаются f и g.
LaTeX
$$$$ \\exists l\\, (g\\circ l = \\mathrm{id}) \\land \\exists l\\, (l\\circ f = \\mathrm{id}) \\iff \\exists e: N \\cong M\\times P\\; (f = e^{-1}\\circ \\mathrm{inl},\\; g = \\mathrm{snd}\\circ e). $$$$
Lean4
/-- Given an exact sequence `M → N → P → 0`, giving a retraction `N → M` is equivalent to giving a
splitting `N ≃ M × P`. -/
noncomputable def splitInjectiveEquiv {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)
(hg : Function.Surjective g) :
{ l // l ∘ₗ f = .id } ≃ { e : N ≃ₗ[R] M × P // f = e.symm ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ e } :=
by
refine
{ toFun := fun l ↦ ⟨(LinearEquiv.ofBijective (l.1.prod g) ?_), ?_⟩
invFun := fun e ↦ ⟨fst R M P ∘ₗ e.1, ?_⟩
left_inv := ?_
right_inv := ?_ }
· have h₁ : ∀ x, l.1 (f x) = x := LinearMap.congr_fun l.2
have h₂ : ∀ x, g (f x) = 0 := congr_fun h.comp_eq_zero
constructor
· intro x y e
simp only [prod_apply, Pi.prod, Prod.mk.injEq] at e
obtain ⟨z, hz⟩ := (h (x - y)).mp (by simpa [sub_eq_zero] using e.2)
suffices z = 0 by rw [← sub_eq_zero, ← hz, this, map_zero]
rw [← h₁ z, hz, map_sub, e.1, sub_self]
· rintro ⟨x, y⟩
obtain ⟨y, rfl⟩ := hg y
refine ⟨f x + y - f (l.1 y), by ext <;> simp [h₁, h₂]⟩
· have h₁ : ∀ x, l.1 (f x) = x := LinearMap.congr_fun l.2
have h₂ : ∀ x, g (f x) = 0 := congr_fun h.comp_eq_zero
constructor
· rw [LinearEquiv.eq_toLinearMap_symm_comp]
ext <;> simp [h₁, h₂]
· ext; simp
· rw [LinearMap.comp_assoc, (LinearEquiv.eq_toLinearMap_symm_comp _ _).mp e.2.1]; rfl
· intro; ext; simp
· rintro ⟨e, rfl, rfl⟩
ext x <;> simp
