English
Given f,g, Exact f g is equivalent to the existence of a left inverse l and a splitting with an isomorphism N ≅ M × P; equivalently, existence of e with f,g expressed via inl and snd.
Русский
Для отображений f,g: точность эквивалентна существованию левого обратного и разложению через изоморфизм; эквивалентно существованию e: N ≅ M × P, такое что f,g выражены через inl и snd.
LaTeX
$$$$ \\operatorname{Exact}(f,g) \\iff \\Bigl(\\exists l\\; g\\circ l = \\mathrm{id} \\land \\exists l\\; l\\circ f = \\mathrm{id} \\Bigr) \\iff \\exists e: N \\cong M\\times P \\; \\bigl(f = e^{-1} \\circ \\mathrm{inl},\\; g = \\mathrm{snd} \\circ e\\bigr). $$$$
Lean4
/-- Given an exact sequence `0 → M → N → P`, giving a section `P → N` is equivalent to giving a
splitting `N ≃ M × P`. -/
noncomputable def splitSurjectiveEquiv (h : Function.Exact f g) (hf : Function.Injective f) :
{ l // g ∘ₗ l = .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 (f ∘ₗ fst R M P + l.1 ∘ₗ snd R M P) ?_).symm, ?_⟩
invFun := fun e ↦ ⟨e.1.symm ∘ₗ inr R M P, ?_⟩
left_inv := ?_
right_inv := ?_ }
· have h₁ : ∀ x, g (l.1 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 [add_apply, coe_comp, comp_apply, fst_apply, snd_apply] at e
suffices x.2 = y.2 from Prod.ext (hf (by rwa [this, add_left_inj] at e)) this
simpa [h₁, h₂] using DFunLike.congr_arg g e
· intro x
obtain ⟨y, hy⟩ := (h (x - l.1 (g x))).mp (by simp [h₁, g.map_sub])
exact ⟨⟨y, g x⟩, by simp [hy]⟩
· have h₁ : ∀ x, g (l.1 x) = x := LinearMap.congr_fun l.2
have h₂ : ∀ x, g (f x) = 0 := congr_fun h.comp_eq_zero
constructor
· ext; simp
· rw [LinearEquiv.eq_comp_toLinearMap_symm]
ext <;> simp [h₁, h₂]
· rw [← LinearMap.comp_assoc, (LinearEquiv.eq_comp_toLinearMap_symm _ _).mp e.2.2]; rfl
· intro; ext; simp
· rintro ⟨e, rfl, rfl⟩
ext1
apply LinearEquiv.symm_bijective.injective
ext
apply e.injective
ext <;> simp
