English
A variant of the split criterion allowing selection of the universe for the free module; the equivalence expresses projectivity via existence of a split after embedding into a suitably chosen free module.
Русский
Вариант критерия разложения, допускающий выбор вселенной для свободного модуля; эквивалентность выражает проективность через существование разложения после внедрения в подобранный свободный модуль.
LaTeX
$$$$ \\text{Projective}(R,P) \\iff \\exists M, \\exists i: P \\to M, \\exists s: M \\to P \\text{ with } s \\circ i = \\mathrm{id}_P. $$$$
Lean4
/-- A variant of `Projective.iff_split` allowing for a more flexible selection of the universe
for the free module `M`. -/
theorem iff_split' [Small.{w} R] [Small.{w} P] :
Module.Projective R P ↔
∃ (M : Type w) (_ : AddCommMonoid M) (_ : Module R M) (_ : Module.Free R M) (i : P →ₗ[R] M) (s : M →ₗ[R] P),
s.comp i = LinearMap.id :=
by
let e : (Shrink.{w, v} P →₀ Shrink.{w, u} R) ≃ₗ[R] P →₀ R :=
Finsupp.mapDomain.linearEquiv _ R (equivShrink P).symm ≪≫ₗ Finsupp.mapRange.linearEquiv (Shrink.linearEquiv R R)
refine
⟨fun ⟨i, hi⟩ ↦
⟨(Shrink.{w} P) →₀ (Shrink.{w} R), _, _, Free.of_basis ⟨e⟩, e.symm.toLinearMap ∘ₗ i,
(linearCombination R id) ∘ₗ e.toLinearMap, ?_⟩,
fun ⟨_, _, _, _, i, s, H⟩ ↦ Projective.of_split i s H⟩
apply LinearMap.ext
simp only [coe_comp, LinearEquiv.coe_coe, Function.comp_apply, e.apply_symm_apply]
exact hi
