English
Given g: M → M'' and a family h asserting that every x ∈ S maps to a unit in End(M''), there exists a linear map LocalizedModule S M → M'' extending g, with a concrete formula on representatives and gluing data.
Русский
Пусть dаны g: M → M'' и семейство h, задающее, что каждый x ∈ S соответствует единице в End(M''), тогда существует линейное отображение LocalizedModule S M → M'', продолжающее g, с явной формулой на представителей и согласование на склейках.
LaTeX
$$$\\exists \\mathrm{lift}'\\;: \\mathrm{LocalizedModule}(S,M) \\to M'' \\;\\text{(продолжающее } g\\text{ with compatibility on representatives).}$$$
Lean4
/-- If `g` is a linear map `M → M''` such that all scalar multiplication by `s : S` is invertible, then
there is a linear map `LocalizedModule S M → M''`.
-/
noncomputable def lift' (g : M →ₗ[R] M'') (h : ∀ x : S, IsUnit (algebraMap R (Module.End R M'') x)) :
LocalizedModule S M → M'' := fun m =>
m.liftOn (fun p => (h p.2).unit⁻¹.val <| g p.1) fun ⟨m, s⟩ ⟨m', s'⟩ ⟨c, eq1⟩ =>
by
dsimp only
simp only [Submonoid.smul_def] at eq1
rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← map_smul, eq_comm,
Module.End.algebraMap_isUnit_inv_apply_eq_iff]
have : c • s • g m' = c • s' • g m := by simp only [Submonoid.smul_def, ← g.map_smul, eq1]
have : Function.Injective (h c).unit.inv := ((Module.End.isUnit_iff _).1 (by simp)).1
apply_fun (h c).unit.inv
rw [Units.inv_eq_val_inv, Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← (h c).unit⁻¹.val.map_smul]
symm
rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, ← g.map_smul, ← g.map_smul, ← g.map_smul, ← g.map_smul, eq1]
