English
Equality between the baseChange construction and the carrier baseChange is preserved componentwise.
Русский
Сохранение равенства между конструкциями baseChange и переносимым носителем по компонентам.
LaTeX
$$$\text{LieSubmodule.baseChange } A N \; = \; \text{Submodule.baseChange } A N.toSubmodule$$$
Lean4
/-- If `A` is an `R`-algebra, any Lie submodule of a Lie module `M` with coefficients in `R` may be
pushed forward to a Lie submodule of `A ⊗ M` with coefficients in `A`.
This "base change" operation is also known as "extension of scalars". -/
def baseChange : LieSubmodule A (A ⊗[R] L) (A ⊗[R] M) :=
{ (N : Submodule R M).baseChange A with
lie_mem := by
intro x m hm
rw [Submodule.mem_carrier, SetLike.mem_coe] at hm ⊢
rw [Submodule.baseChange_eq_span] at hm
obtain ⟨c, rfl⟩ := (Finsupp.mem_span_iff_linearCombination _ _ _).mp hm
refine x.induction_on (by simp) (fun a y ↦ ?_) (fun y z hy hz ↦ ?_)
· change toEnd A (A ⊗[R] L) (A ⊗[R] M) _ _ ∈ _
simp_rw [Finsupp.linearCombination_apply, Finsupp.sum, map_sum, map_smul, toEnd_apply_apply]
refine Submodule.sum_mem _ fun ⟨_, n, hn, h⟩ _ ↦ Submodule.smul_mem _ _ ?_
rw [Subtype.coe_mk, ← h]
exact Submodule.tmul_mem_baseChange_of_mem _ (N.lie_mem hn)
· rw [add_lie]
exact ((N : Submodule R M).baseChange A).add_mem hy hz }
