English
Let R be a commutative semiring and M an R-module. Then M is free if and only if there exists a linear equivalence between M and R.
Русский
Пусть R — коммутативное полупкольцо, и M — R-модуль. Тогда M свободен тогда и только тогда, когда существует линейное эквивалентное отображение между M и R.
LaTeX
$$$\operatorname{Free}_R(M) \iff \exists e: M \cong_R R$$$
Lean4
/-- An invertible module is free iff it is isomorphic to the ring, i.e. its class is trivial in
the Picard group. -/
theorem free_iff_linearEquiv : Free R M ↔ Nonempty (M ≃ₗ[R] R) :=
by
refine ⟨fun _ ↦ ?_, fun ⟨e⟩ ↦ .of_equiv e.symm⟩
nontriviality R
have e := (Free.chooseBasis R M).repr
have :=
card_eq_of_linearEquiv R <|
(finsuppTensorFinsupp' .. ≪≫ₗ linearEquivFunOnFinite R R _).symm ≪≫ₗ
TensorProduct.congr (linearEquivFunOnFinite R R _ ≪≫ₗ llift R R R _ ≪≫ₗ e.dualMap) e.symm ≪≫ₗ
linearEquiv R M ≪≫ₗ
(.symm <| .funUnique Unit R R)
have : Unique (Free.ChooseBasisIndex R M) := (Fintype.card_eq_one_iff_nonempty_unique.mp (by simpa using this)).some
exact
⟨e ≪≫ₗ LinearEquiv.finsuppUnique R R _⟩
/- TODO: The ≤ direction holds for arbitrary invertible modules over any commutative **ring** by
considering the localization at a prime (which is free of rank 1) using the strong rank condition.
The ≥ direction fails in general but holds for domains and Noetherian rings without embedded
components, see https://math.stackexchange.com/q/5089900. -/
