English
If M fits in universe w, freeness is equivalent to the existence of a basis indexed by a type of universe w.
Русский
Если M помещается во вселенную w, то свобода M эквивалентна существованию базиса, индексированного типом вселенной w.
LaTeX
$$$$ \mathrm{Free}_R M \iff \exists I:\mathrm{Type}_w, \mathrm{Nonempty}(\mathrm{Basis}(I,R,M)) $$$$
Lean4
/-- If `M` fits in universe `w`, then freeness is equivalent to existence of a basis in that
universe.
Note that if `M` does not fit in `w`, the reverse direction of this implication is still true as
`Module.Free.of_basis`. -/
theorem free_def [Small.{w, v} M] : Free R M ↔ ∃ I : Type w, Nonempty (Basis I R M)
where
mp
h :=
⟨Shrink (Set.range h.exists_basis.some.2), ⟨(Basis.reindexRange h.exists_basis.some.2).reindex (equivShrink _)⟩⟩
mpr h := ⟨(nonempty_sigma.2 h).map fun ⟨_, b⟩ => ⟨Set.range b, b.reindexRange⟩⟩
