of_basis — Mathlib

English

Free modules are projective: if P has a basis, then P is projective.

Русский

Свободные модули проектные: если у P есть базис, то P проективен.

LaTeX

$$$$ \\text{If } P \\text{ is free, then } \\text{Projective}(R,P). $$$$

Lean4

/-- Free modules are projective. -/
theorem of_basis {ι : Type*} (b : Basis ι R P) : Projective R P := by
  -- need P →ₗ (P →₀ R) for definition of projective.
    -- get it from `ι → (P →₀ R)` coming from `b`.

  use b.constr ℕ fun i => Finsupp.single (b i) (1 : R)
  intro m
  simp only [b.constr_apply, mul_one, id, Finsupp.smul_single', Finsupp.linearCombination_single, map_finsuppSum]
  exact b.linearCombination_repr m

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