English
The unit of Submodule R A yields an invertible R-module structure on its carrier.
Русский
Единичный элемент Submodule R A порождает инвертируемость как R-модуля на его носитель.
LaTeX
$$$ \\forall (I : \\mathrm{Units}( \\mathrm{Submodule} R A )), \\; \\mathrm{Module.Invertible} R (\\mathrm{Subtype} (\\lambda x, x \\in I.1)). $$$
Lean4
/-- The group homomorphism from the invertible submodules
in a localization of `R` to the Picard group of `R`. -/
@[simps]
noncomputable def unitsToPic : (Submodule R A)ˣ →* Pic R :=
haveI := Units.submodule_invertible S (A := A)
{ toFun I := Pic.mk R I
map_one' :=
mk_eq_one_iff.mpr ⟨.ofEq _ _ one_eq_range ≪≫ₗ .symm (.ofInjective _ (FaithfulSMul.algebraMap_injective R A))⟩
map_mul' I J := by rw [← mk_tensor, mk_eq_mk_iff]; exact ⟨(tensorEquivMul S I J).symm⟩ }
