iff_split — Mathlib

English

Another formulation of projectivity in terms of an explicit presentation with a map i and s such that s ∘ i = id; provides a constructive criterion.

Русский

Еще одна формулировка проективности через явное отображение i и s с условием s ∘ i = id; дает конструктивный критерий.

LaTeX

$$$$ \\text{Projective}(R,P) \\iff \\exists i,s, s\\circ i = \\mathrm{id}_P. $$$$

Lean4

/-- A module is projective iff it is the direct summand of a free module. -/
theorem iff_split :
    Module.Projective R P ↔
      ∃ (M : Type max u v) (_ : AddCommMonoid M) (_ : Module R M) (_ : Module.Free R M) (i : P →ₗ[R] M) (s : M →ₗ[R] P),
        s.comp i = LinearMap.id :=
  Projective.iff_split'.{max u v}

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