split_tfae' — Mathlib

English

Three equivalent conditions for split exact sequences: existence of l with g∘l=id, existence of l with l∘f=id, and an isomorphism N ≅ M×P with f and g given by canonical injections/projections.

Русский

Три эквивалентные условия для распада точной последовательности: существование левого обратного l, существование правого обратного, и изоморфизм N ≅ M×P с выражениями f и g через инл/снд.

LaTeX

$$$$ \\text{TFAE}(\\{\\exists l: N\\to M\\; (g\\circ l = id)\\},\\{\\exists l: M\\to N\\; (l\\circ f = id)\\},\\{\\exists e: N\\cong M\\times P\\; (f = e^{-1}\\circ inl,\\; g = snd\\circ e)\\}) $$$$

Lean4

theorem split_tfae' (h : Function.Exact f g) :
    List.TFAE
      [Function.Injective f ∧ ∃ l, g ∘ₗ l = LinearMap.id, Function.Surjective g ∧ ∃ 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
    | ⟨hf, l, hl⟩ => ⟨_, (h.splitSurjectiveEquiv hf ⟨l, hl⟩).2⟩
  tfae_have 2 → 3
    | ⟨hg, l, hl⟩ => ⟨_, (h.splitInjectiveEquiv hg ⟨l, hl⟩).2⟩
  tfae_have 3 → 1
    | ⟨e, e₁, e₂⟩ => by
      have : Function.Injective f := e₁ ▸ e.symm.injective.comp LinearMap.inl_injective
      exact ⟨this, ⟨_, ((h.splitSurjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩
  tfae_have 3 → 2
    | ⟨e, e₁, e₂⟩ => by
      have : Function.Surjective g := e₂ ▸ Prod.snd_surjective.comp e.surjective
      exact ⟨this, ⟨_, ((h.splitInjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩
  tfae_finish

Похожие утверждения