English
A unit I of Submodule R A is projective as an R-module.
Русский
Единичный подмодуль I Submodule R A является проективным как R-модуль.
LaTeX
$$$ (I : \\mathrm{Units}(\\mathrm{Submodule} R A)) \\Rightarrow \\text{Projective } R I. $$$
Lean4
instance projective_unit (I : (Submodule R A)ˣ) : Projective R I :=
by
obtain ⟨T, T', hT, hT', one_mem⟩ := mem_span_mul_finite_of_mem_mul (I.inv_mul ▸ one_le.mp le_rfl)
classical
rw [← Set.image2_mul, ← Finset.coe_image₂, mem_span_finset] at one_mem
set S := T.image₂ (· * ·) T'
obtain ⟨r, hr⟩ := one_mem
choose a ha b hb eq using fun i : S ↦ Finset.mem_image₂.mp i.2
let f : I →ₗ[R] S → R :=
.pi fun i ↦
(LinearEquiv.ofInjective (Algebra.linearMap R A) (FaithfulSMul.algebraMap_injective R A)).symm.comp <|
restrict (mulRight R (r i • a i)) fun x hx ↦ by rw [← one_eq_range, ← I.mul_inv];
exact mul_mem_mul hx (I⁻¹.1.smul_mem _ <| hT <| ha i)
let g : (S → R) →ₗ[R] I := .lsum _ _ ℕ fun i ↦ .toSpanSingleton _ _ ⟨b i, hT' <| hb i⟩
refine .of_split f g (LinearMap.ext fun x ↦ Subtype.ext ?_)
simp only [f, g, lsum_apply, comp_apply, sum_apply, toSpanSingleton_apply, proj_apply, pi_apply]
simp_rw [restrict_apply, mulRight_apply, id_apply, coe_sum, coe_smul, Algebra.smul_def, ← Algebra.coe_linearMap,
LinearEquiv.coe_toLinearMap, LinearEquiv.ofInjective_symm_apply, mul_assoc, Algebra.coe_linearMap, ←
Algebra.smul_def, ← Finset.mul_sum, eq, (Finset.sum_coe_sort ..).trans hr.2, mul_one]
