isSolvable_tensorProduct_iff — Mathlib

English

Under faithful flatness of A, the solvability of A ⊗_R L is equivalent to the solvability of L.

Русский

При условии полной плоскости A как модуль над R существование равенства: solvable(A ⊗_R L) ⇔ solvable(L).

LaTeX

$$$\text{IsSolvable} (A \otimes_R L) \;\iff\; \text{IsSolvable } L$$$

Lean4

theorem isSolvable_tensorProduct_iff : IsSolvable (A ⊗[R] L) ↔ IsSolvable L :=
  by
  refine ⟨?_, fun _ ↦ inferInstance⟩
  rw [isSolvable_iff A, isSolvable_iff R]
  rintro ⟨k, h⟩
  use k
  rw [eq_bot_iff] at h ⊢
  intro x hx
  rw [derivedSeries_baseChange] at h
  specialize h <| Submodule.tmul_mem_baseChange_of_mem 1 hx
  rw [LieSubmodule.mem_bot] at h ⊢
  rwa [Module.FaithfullyFlat.one_tmul_eq_zero_iff] at h

Похожие утверждения