English
If I is a unit in the lattice of submodules, then the underlying submodule I is finitely generated.
Русский
Если I является единицей в решётке подмодулей, то соответствующий подмодуль I конечно порождается.
LaTeX
$$$I \in (\text{Submodule } R A)^{\times} \quad\Rightarrow\quad (I : \text{Submodule } R A).FG$$$
Lean4
theorem fg_unit {R A : Type*} [CommSemiring R] [Semiring A] [Algebra R A] (I : (Submodule R A)ˣ) :
(I : Submodule R A).FG :=
by
obtain ⟨T, T', hT, hT', one_mem⟩ := mem_span_mul_finite_of_mem_mul (I.mul_inv ▸ one_le.mp le_rfl)
refine ⟨T, span_eq_of_le _ hT ?_⟩
rw [← one_mul I, ← mul_one (span R (T : Set A))]
conv_rhs => rw [← I.inv_mul, ← mul_assoc]
refine mul_le_mul_right' (le_trans ?_ <| mul_le_mul_left' (span_le.mpr hT') _) _
rwa [Units.val_one, span_mul_span, one_le]
