English
For a principal ideal I and a nonzero element, the inclusion map composed with the principal-isPrincipal is equal to multiplication by the generator of I.
Русский
Для главного идеала I и элемента x выполняется равенство: вкючение через подпорядок I после изоморфизма базиса равно умножению на генератор I.
LaTeX
$$$\text{Submodule.subtype } I \circ_\ell (\mathrm{Ideal.isoBaseOfIsPrincipal } h) = \mathrm{LinearMap.mul}(R,R, \mathrm{IsPrincipal.generator } I)$$$
Lean4
/-- A nonzero principal ideal in an integral domain `R` is isomorphic to `R` as a module.
The isomorphism we choose here sends `1` to the generator chosen by `Ideal.generator`. -/
noncomputable def isoBaseOfIsPrincipal {I : Ideal R} [hprinc : I.IsPrincipal] (hI : I ≠ ⊥) : R ≃ₗ[R] I :=
letI x := IsPrincipal.generator I
have hx : x ≠ 0 := by rwa [Ne, ← IsPrincipal.eq_bot_iff_generator_eq_zero]
(LinearEquiv.toSpanNonzeroSingleton R R x hx).trans
(LinearEquiv.ofEq (Submodule.span R { x }) I (IsPrincipal.span_singleton_generator I))
