English
Base change commutes with Lie bracket: the base change of the bracket [I,N] equals the bracket of the base changes I and N.
Русский
Базовое изменение commute с относительно скобки: базовое изменение ⁅I,N⁆ равно ⁅I.baseChange A, N.baseChange A⁆.
LaTeX
$$$ \\operatorname{baseChange}_A([I,N]) = [I^{\\mathrm{baseChange}_A}, N^{\\mathrm{baseChange}_A}] $$$
Lean4
theorem lie_baseChange {I : LieIdeal R L} {N : LieSubmodule R L M} :
⁅I, N⁆.baseChange A = ⁅I.baseChange A, N.baseChange A⁆ :=
by
set s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ ⁅x, n⁆ = m}
have : (TensorProduct.mk R A M 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s := by ext; simp [s]
rw [← toSubmodule_inj, coe_baseChange, lieIdeal_oper_eq_linear_span', Submodule.baseChange_span, this,
lieIdeal_oper_eq_linear_span']
refine le_antisymm (Submodule.span_mono ?_) (Submodule.span_le.mpr ?_)
· rintro - ⟨x, hx, m, hm, rfl⟩
exact ⟨1 ⊗ₜ x, tmul_mem_baseChange_of_mem 1 hx, 1 ⊗ₜ m, tmul_mem_baseChange_of_mem 1 hm, by simp⟩
· rintro - ⟨x, hx, m, hm, rfl⟩
rw [mem_baseChange_iff] at hx hm
refine
Submodule.span_induction₂ (p := fun x m _ _ ↦ ⁅x, m⁆ ∈ Submodule.span A s) ?_ (by simp) (by simp) ?_ ?_ ?_ ?_ hx
hm
· rintro - - ⟨x, hx, rfl⟩ ⟨y, hy, rfl⟩; exact Submodule.subset_span ⟨x, hx, y, hy, by simp⟩
all_goals { intros; simp [add_mem, Submodule.smul_mem, *]
}
