English
The map lift' is additive with respect to the LocalizedModule addition; i.e., lifts respect addition of localized elements.
Русский
lift' сохраняет сложение: переход через lift' совместим с операцией сложения в локализованном модуле.
LaTeX
$$$\\mathrm{lift}'(g,h)(x+y) = \\mathrm{lift}'(g,h)(x) + \\mathrm{lift}'(g,h)(y).$$$
Lean4
theorem lift'_add (g : M →ₗ[R] M'') (h : ∀ x : S, IsUnit ((algebraMap R (Module.End R M'')) x)) (x y) :
LocalizedModule.lift' S g h (x + y) = LocalizedModule.lift' S g h x + LocalizedModule.lift' S g h y :=
LocalizedModule.induction_on₂
(by
intro a a' b b'
rw [mk_add_mk, LocalizedModule.lift'_mk, LocalizedModule.lift'_mk, LocalizedModule.lift'_mk]
rw [map_add, Module.End.algebraMap_isUnit_inv_apply_eq_iff, smul_add, ← map_smul, ← map_smul, ← map_smul]
congr 1 <;> symm
· rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff]
simp only [Submonoid.coe_mul, LinearMap.map_smul_of_tower]
rw [mul_smul, Submonoid.smul_def]
· dsimp
rw [Module.End.algebraMap_isUnit_inv_apply_eq_iff, mul_comm, mul_smul, ← map_smul]
rfl)
x y
