[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
⊢ lcs k N ≤ N
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
⊢ lcs Nat.zero N ≤ N
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : lcs k N ≤ N
⊢ lcs (Nat.succ k) N ≤ N
[PROOFSTEP]
simp only [lcs_succ]
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : lcs k N ≤ N
⊢ ⁅⊤, lcs k N⁆ ≤ N
[PROOFSTEP]
exact (LieSubmodule.mono_lie_right _ _ ⊤ ih).trans (N.lie_le_right ⊤)
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
⊢ lowerCentralSeries R L { x // x ∈ ↑N } k = comap (incl N) (lcs k N)
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
⊢ lowerCentralSeries R L { x // x ∈ ↑N } Nat.zero = comap (incl N) (lcs Nat.zero N)
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : lowerCentralSeries R L { x // x ∈ ↑N } k = comap (incl N) (lcs k N)
⊢ lowerCentralSeries R L { x // x ∈ ↑N } (Nat.succ k) = comap (incl N) (lcs (Nat.succ k) N)
[PROOFSTEP]
simp only [lcs_succ, lowerCentralSeries_succ] at ih ⊢
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : lowerCentralSeries R L { x // x ∈ ↑N } k = comap (incl N) (lcs k N)
⊢ ⁅⊤, lowerCentralSeries R L { x // x ∈ ↑N } k⁆ = comap (incl N) ⁅⊤, lcs k N⁆
[PROOFSTEP]
have : N.lcs k ≤ N.incl.range := by
  rw [N.range_incl]
  apply lcs_le_self
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : lowerCentralSeries R L { x // x ∈ ↑N } k = comap (incl N) (lcs k N)
⊢ lcs k N ≤ LieModuleHom.range (incl N)
[PROOFSTEP]
rw [N.range_incl]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : lowerCentralSeries R L { x // x ∈ ↑N } k = comap (incl N) (lcs k N)
⊢ lcs k N ≤ N
[PROOFSTEP]
apply lcs_le_self
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : lowerCentralSeries R L { x // x ∈ ↑N } k = comap (incl N) (lcs k N)
this : lcs k N ≤ LieModuleHom.range (incl N)
⊢ ⁅⊤, lowerCentralSeries R L { x // x ∈ ↑N } k⁆ = comap (incl N) ⁅⊤, lcs k N⁆
[PROOFSTEP]
rw [ih, LieSubmodule.comap_bracket_eq _ _ N.incl N.ker_incl this]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
⊢ map (incl N) (lowerCentralSeries R L { x // x ∈ ↑N } k) = lcs k N
[PROOFSTEP]
rw [lowerCentralSeries_eq_lcs_comap, LieSubmodule.map_comap_incl, inf_eq_right]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
⊢ lcs k N ≤ N
[PROOFSTEP]
apply lcs_le_self
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
⊢ Antitone (lowerCentralSeries R L M)
[PROOFSTEP]
intro l k
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
l k : ℕ
⊢ l ≤ k → lowerCentralSeries R L M k ≤ lowerCentralSeries R L M l
[PROOFSTEP]
induction' k with k ih generalizing l
[GOAL]
case zero
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
l✝ l : ℕ
⊢ l ≤ Nat.zero → lowerCentralSeries R L M Nat.zero ≤ lowerCentralSeries R L M l
[PROOFSTEP]
intro h
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
l✝ k : ℕ
ih : ∀ ⦃l : ℕ⦄, l ≤ k → lowerCentralSeries R L M k ≤ lowerCentralSeries R L M l
l : ℕ
⊢ l ≤ Nat.succ k → lowerCentralSeries R L M (Nat.succ k) ≤ lowerCentralSeries R L M l
[PROOFSTEP]
intro h
[GOAL]
case zero
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
l✝ l : ℕ
h : l ≤ Nat.zero
⊢ lowerCentralSeries R L M Nat.zero ≤ lowerCentralSeries R L M l
[PROOFSTEP]
exact (le_zero_iff.mp h).symm ▸ le_rfl
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
l✝ k : ℕ
ih : ∀ ⦃l : ℕ⦄, l ≤ k → lowerCentralSeries R L M k ≤ lowerCentralSeries R L M l
l : ℕ
h : l ≤ Nat.succ k
⊢ lowerCentralSeries R L M (Nat.succ k) ≤ lowerCentralSeries R L M l
[PROOFSTEP]
rcases Nat.of_le_succ h with (hk | hk)
[GOAL]
case succ.inl
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
l✝ k : ℕ
ih : ∀ ⦃l : ℕ⦄, l ≤ k → lowerCentralSeries R L M k ≤ lowerCentralSeries R L M l
l : ℕ
h : l ≤ Nat.succ k
hk : l ≤ k
⊢ lowerCentralSeries R L M (Nat.succ k) ≤ lowerCentralSeries R L M l
[PROOFSTEP]
rw [lowerCentralSeries_succ]
[GOAL]
case succ.inl
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
l✝ k : ℕ
ih : ∀ ⦃l : ℕ⦄, l ≤ k → lowerCentralSeries R L M k ≤ lowerCentralSeries R L M l
l : ℕ
h : l ≤ Nat.succ k
hk : l ≤ k
⊢ ⁅⊤, lowerCentralSeries R L M k⁆ ≤ lowerCentralSeries R L M l
[PROOFSTEP]
exact (LieSubmodule.mono_lie_right _ _ ⊤ (ih hk)).trans (LieSubmodule.lie_le_right _ _)
[GOAL]
case succ.inr
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
l✝ k : ℕ
ih : ∀ ⦃l : ℕ⦄, l ≤ k → lowerCentralSeries R L M k ≤ lowerCentralSeries R L M l
l : ℕ
h : l ≤ Nat.succ k
hk : l = Nat.succ k
⊢ lowerCentralSeries R L M (Nat.succ k) ≤ lowerCentralSeries R L M l
[PROOFSTEP]
exact hk.symm ▸ le_rfl
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
⊢ IsTrivial L M ↔ lowerCentralSeries R L M 1 = ⊥
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
⊢ IsTrivial L M → lowerCentralSeries R L M 1 = ⊥
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
⊢ lowerCentralSeries R L M 1 = ⊥ → IsTrivial L M
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
h : IsTrivial L M
⊢ lowerCentralSeries R L M 1 = ⊥
[PROOFSTEP]
erw [eq_bot_iff, LieSubmodule.lieSpan_le]
[GOAL]
case mp
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
h : IsTrivial L M
⊢ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ ↑⊥
[PROOFSTEP]
rintro m ⟨x, n, hn⟩
[GOAL]
case mp.intro.intro
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
h : IsTrivial L M
m : M
x : { x // x ∈ ⊤ }
n : { x // x ∈ ⊤ }
hn : ⁅↑x, ↑n⁆ = m
⊢ m ∈ ↑⊥
[PROOFSTEP]
rw [← hn, h.trivial]
[GOAL]
case mp.intro.intro
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
h : IsTrivial L M
m : M
x : { x // x ∈ ⊤ }
n : { x // x ∈ ⊤ }
hn : ⁅↑x, ↑n⁆ = m
⊢ 0 ∈ ↑⊥
[PROOFSTEP]
simp
[GOAL]
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
h : lowerCentralSeries R L M 1 = ⊥
⊢ IsTrivial L M
[PROOFSTEP]
rw [LieSubmodule.eq_bot_iff] at h
[GOAL]
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
h : ∀ (m : M), m ∈ lowerCentralSeries R L M 1 → m = 0
⊢ IsTrivial L M
[PROOFSTEP]
apply IsTrivial.mk
[GOAL]
case mpr.trivial
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
h : ∀ (m : M), m ∈ lowerCentralSeries R L M 1 → m = 0
⊢ ∀ (x : L) (m : M), ⁅x, m⁆ = 0
[PROOFSTEP]
intro x m
[GOAL]
case mpr.trivial
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
h : ∀ (m : M), m ∈ lowerCentralSeries R L M 1 → m = 0
x : L
m : M
⊢ ⁅x, m⁆ = 0
[PROOFSTEP]
apply h
[GOAL]
case mpr.trivial.a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
h : ∀ (m : M), m ∈ lowerCentralSeries R L M 1 → m = 0
x : L
m : M
⊢ ⁅x, m⁆ ∈ lowerCentralSeries R L M 1
[PROOFSTEP]
apply LieSubmodule.subset_lieSpan
[GOAL]
case mpr.trivial.a.a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
h : ∀ (m : M), m ∈ lowerCentralSeries R L M 1 → m = 0
x : L
m : M
⊢ ⁅x, m⁆ ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
[PROOFSTEP]
simp only [LieSubmodule.top_coe, Subtype.exists, LieSubmodule.mem_top, exists_prop, true_and, Set.mem_setOf]
[GOAL]
case mpr.trivial.a.a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
h : ∀ (m : M), m ∈ lowerCentralSeries R L M 1 → m = 0
x : L
m : M
⊢ ∃ a a_1, ⁅a, a_1⁆ = ⁅x, m⁆
[PROOFSTEP]
exact ⟨x, m, rfl⟩
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
x : L
m : M
k : ℕ
⊢ (↑(↑(toEndomorphism R L M) x))^[k] m ∈ lowerCentralSeries R L M k
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
x : L
m : M
⊢ (↑(↑(toEndomorphism R L M) x))^[Nat.zero] m ∈ lowerCentralSeries R L M Nat.zero
[PROOFSTEP]
simp only [Nat.zero_eq, Function.iterate_zero, lowerCentralSeries_zero, LieSubmodule.mem_top]
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
x : L
m : M
k : ℕ
ih : (↑(↑(toEndomorphism R L M) x))^[k] m ∈ lowerCentralSeries R L M k
⊢ (↑(↑(toEndomorphism R L M) x))^[Nat.succ k] m ∈ lowerCentralSeries R L M (Nat.succ k)
[PROOFSTEP]
simp only [lowerCentralSeries_succ, Function.comp_apply, Function.iterate_succ', toEndomorphism_apply_apply]
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
x : L
m : M
k : ℕ
ih : (↑(↑(toEndomorphism R L M) x))^[k] m ∈ lowerCentralSeries R L M k
⊢ ⁅x, (↑(↑(toEndomorphism R L M) x))^[k] m⁆ ∈ ⁅⊤, lowerCentralSeries R L M k⁆
[PROOFSTEP]
exact LieSubmodule.lie_mem_lie _ _ (LieSubmodule.mem_top x) ih
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
x y : L
m : M
k : ℕ
⊢ (↑(LinearMap.comp (↑(toEndomorphism R L M) x) (↑(toEndomorphism R L M) y)))^[k] m ∈ lowerCentralSeries R L M (2 * k)
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
x y : L
m : M
⊢ (↑(LinearMap.comp (↑(toEndomorphism R L M) x) (↑(toEndomorphism R L M) y)))^[Nat.zero] m ∈
    lowerCentralSeries R L M (2 * Nat.zero)
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
x y : L
m : M
k : ℕ
ih :
  (↑(LinearMap.comp (↑(toEndomorphism R L M) x) (↑(toEndomorphism R L M) y)))^[k] m ∈ lowerCentralSeries R L M (2 * k)
⊢ (↑(LinearMap.comp (↑(toEndomorphism R L M) x) (↑(toEndomorphism R L M) y)))^[Nat.succ k] m ∈
    lowerCentralSeries R L M (2 * Nat.succ k)
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
x y : L
m : M
k : ℕ
ih :
  (↑(LinearMap.comp (↑(toEndomorphism R L M) x) (↑(toEndomorphism R L M) y)))^[k] m ∈ lowerCentralSeries R L M (2 * k)
⊢ (↑(LinearMap.comp (↑(toEndomorphism R L M) x) (↑(toEndomorphism R L M) y)))^[Nat.succ k] m ∈
    lowerCentralSeries R L M (2 * Nat.succ k)
[PROOFSTEP]
have hk : 2 * k.succ = (2 * k + 1) + 1 := rfl
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
x y : L
m : M
k : ℕ
ih :
  (↑(LinearMap.comp (↑(toEndomorphism R L M) x) (↑(toEndomorphism R L M) y)))^[k] m ∈ lowerCentralSeries R L M (2 * k)
hk : 2 * Nat.succ k = 2 * k + 1 + 1
⊢ (↑(LinearMap.comp (↑(toEndomorphism R L M) x) (↑(toEndomorphism R L M) y)))^[Nat.succ k] m ∈
    lowerCentralSeries R L M (2 * Nat.succ k)
[PROOFSTEP]
simp only [lowerCentralSeries_succ, Function.comp_apply, Function.iterate_succ', hk, toEndomorphism_apply_apply,
  LinearMap.coe_comp, toEndomorphism_apply_apply]
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
x y : L
m : M
k : ℕ
ih :
  (↑(LinearMap.comp (↑(toEndomorphism R L M) x) (↑(toEndomorphism R L M) y)))^[k] m ∈ lowerCentralSeries R L M (2 * k)
hk : 2 * Nat.succ k = 2 * k + 1 + 1
⊢ ⁅x, ⁅y, (↑(↑(toEndomorphism R L M) x) ∘ ↑(↑(toEndomorphism R L M) y))^[k] m⁆⁆ ∈
    ⁅⊤, ⁅⊤, lowerCentralSeries R L M (2 * k)⁆⁆
[PROOFSTEP]
refine' LieSubmodule.lie_mem_lie _ _ (LieSubmodule.mem_top x) _
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
x y : L
m : M
k : ℕ
ih :
  (↑(LinearMap.comp (↑(toEndomorphism R L M) x) (↑(toEndomorphism R L M) y)))^[k] m ∈ lowerCentralSeries R L M (2 * k)
hk : 2 * Nat.succ k = 2 * k + 1 + 1
⊢ ⁅y, (↑(↑(toEndomorphism R L M) x) ∘ ↑(↑(toEndomorphism R L M) y))^[k] m⁆ ∈ ⁅⊤, lowerCentralSeries R L M (2 * k)⁆
[PROOFSTEP]
exact LieSubmodule.lie_mem_lie _ _ (LieSubmodule.mem_top y) ih
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
M₂ : Type w₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
k : ℕ
f : M →ₗ⁅R,L⁆ M₂
⊢ LieSubmodule.map f (lowerCentralSeries R L M k) ≤ lowerCentralSeries R L M₂ k
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
L : Type v
M : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
M₂ : Type w₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
f : M →ₗ⁅R,L⁆ M₂
⊢ LieSubmodule.map f (lowerCentralSeries R L M Nat.zero) ≤ lowerCentralSeries R L M₂ Nat.zero
[PROOFSTEP]
simp only [Nat.zero_eq, lowerCentralSeries_zero, le_top]
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
M₂ : Type w₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
f : M →ₗ⁅R,L⁆ M₂
k : ℕ
ih : LieSubmodule.map f (lowerCentralSeries R L M k) ≤ lowerCentralSeries R L M₂ k
⊢ LieSubmodule.map f (lowerCentralSeries R L M (Nat.succ k)) ≤ lowerCentralSeries R L M₂ (Nat.succ k)
[PROOFSTEP]
simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.map_bracket_eq]
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
M₂ : Type w₁
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L M₂
inst✝ : LieModule R L M₂
f : M →ₗ⁅R,L⁆ M₂
k : ℕ
ih : LieSubmodule.map f (lowerCentralSeries R L M k) ≤ lowerCentralSeries R L M₂ k
⊢ ⁅⊤, LieSubmodule.map f (lowerCentralSeries R L M k)⁆ ≤ ⁅⊤, lowerCentralSeries R L M₂ k⁆
[PROOFSTEP]
exact LieSubmodule.mono_lie_right _ _ ⊤ ih
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
⊢ derivedSeries R L k ≤ lowerCentralSeries R L L k
[PROOFSTEP]
induction' k with k h
[GOAL]
case zero
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
⊢ derivedSeries R L Nat.zero ≤ lowerCentralSeries R L L Nat.zero
[PROOFSTEP]
rw [derivedSeries_def, derivedSeriesOfIdeal_zero, lowerCentralSeries_zero]
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
h : derivedSeries R L k ≤ lowerCentralSeries R L L k
⊢ derivedSeries R L (Nat.succ k) ≤ lowerCentralSeries R L L (Nat.succ k)
[PROOFSTEP]
have h' : derivedSeries R L k ≤ ⊤ := by simp only [le_top]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
h : derivedSeries R L k ≤ lowerCentralSeries R L L k
⊢ derivedSeries R L k ≤ ⊤
[PROOFSTEP]
simp only [le_top]
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
h : derivedSeries R L k ≤ lowerCentralSeries R L L k
h' : derivedSeries R L k ≤ ⊤
⊢ derivedSeries R L (Nat.succ k) ≤ lowerCentralSeries R L L (Nat.succ k)
[PROOFSTEP]
rw [derivedSeries_def, derivedSeriesOfIdeal_succ, lowerCentralSeries_succ]
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
h : derivedSeries R L k ≤ lowerCentralSeries R L L k
h' : derivedSeries R L k ≤ ⊤
⊢ ⁅derivedSeriesOfIdeal R L k ⊤, derivedSeriesOfIdeal R L k ⊤⁆ ≤ ⁅⊤, lowerCentralSeries R L L k⁆
[PROOFSTEP]
exact LieSubmodule.mono_lie _ _ _ _ h' h
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N✝ N : LieSubmodule R L M
⊢ IsNilpotent R L { x // x ∈ ↑N } ↔ ∃ k, LieSubmodule.lcs k N = ⊥
[PROOFSTEP]
rw [isNilpotent_iff]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N✝ N : LieSubmodule R L M
⊢ (∃ k, lowerCentralSeries R L { x // x ∈ ↑N } k = ⊥) ↔ ∃ k, LieSubmodule.lcs k N = ⊥
[PROOFSTEP]
refine' exists_congr fun k => _
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N✝ N : LieSubmodule R L M
k : ℕ
⊢ lowerCentralSeries R L { x // x ∈ ↑N } k = ⊥ ↔ LieSubmodule.lcs k N = ⊥
[PROOFSTEP]
rw [N.lowerCentralSeries_eq_lcs_comap k, LieSubmodule.comap_incl_eq_bot, inf_eq_right.mpr (N.lcs_le_self k)]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsTrivial L M
⊢ ∃ k, lowerCentralSeries R L M k = ⊥
[PROOFSTEP]
use 1
[GOAL]
case h
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsTrivial L M
⊢ lowerCentralSeries R L M 1 = ⊥
[PROOFSTEP]
change ⁅⊤, ⊤⁆ = ⊥
[GOAL]
case h
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsTrivial L M
⊢ ⁅⊤, ⊤⁆ = ⊥
[PROOFSTEP]
simp
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
hM : IsNilpotent R L M
⊢ ∃ k, ∀ (x : L), ↑(toEndomorphism R L M) x ^ k = 0
[PROOFSTEP]
obtain ⟨k, hM⟩ := hM
[GOAL]
case mk.intro
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
⊢ ∃ k, ∀ (x : L), ↑(toEndomorphism R L M) x ^ k = 0
[PROOFSTEP]
use k
[GOAL]
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
⊢ ∀ (x : L), ↑(toEndomorphism R L M) x ^ k = 0
[PROOFSTEP]
intro x
[GOAL]
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
x : L
⊢ ↑(toEndomorphism R L M) x ^ k = 0
[PROOFSTEP]
ext m
[GOAL]
case h.h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
x : L
m : M
⊢ ↑(↑(toEndomorphism R L M) x ^ k) m = ↑0 m
[PROOFSTEP]
rw [LinearMap.pow_apply, LinearMap.zero_apply, ← @LieSubmodule.mem_bot R L M, ← hM]
[GOAL]
case h.h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
x : L
m : M
⊢ (↑(↑(toEndomorphism R L M) x))^[k] m ∈ lowerCentralSeries R L M k
[PROOFSTEP]
exact iterate_toEndomorphism_mem_lowerCentralSeries R L M x m k
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
x : L
⊢ _root_.IsNilpotent (↑(toEndomorphism R L M) x)
[PROOFSTEP]
change ∃ k, toEndomorphism R L M x ^ k = 0
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
x : L
⊢ ∃ k, ↑(toEndomorphism R L M) x ^ k = 0
[PROOFSTEP]
have := exists_forall_pow_toEndomorphism_eq_zero R L M
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
x : L
this : ∃ k, ∀ (x : L), ↑(toEndomorphism R L M) x ^ k = 0
⊢ ∃ k, ↑(toEndomorphism R L M) x ^ k = 0
[PROOFSTEP]
tauto
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
x y : L
⊢ _root_.IsNilpotent (LinearMap.comp (↑(toEndomorphism R L M) x) (↑(toEndomorphism R L M) y))
[PROOFSTEP]
obtain ⟨k, hM⟩ := exists_lowerCentralSeries_eq_bot_of_isNilpotent R L M
[GOAL]
case intro
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
x y : L
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
⊢ _root_.IsNilpotent (LinearMap.comp (↑(toEndomorphism R L M) x) (↑(toEndomorphism R L M) y))
[PROOFSTEP]
replace hM : lowerCentralSeries R L M (2 * k) = ⊥ := by rw [eq_bot_iff, ← hM];
  exact antitone_lowerCentralSeries R L M (by linarith)
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
x y : L
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
⊢ lowerCentralSeries R L M (2 * k) = ⊥
[PROOFSTEP]
rw [eq_bot_iff, ← hM]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
x y : L
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
⊢ lowerCentralSeries R L M (2 * k) ≤ lowerCentralSeries R L M k
[PROOFSTEP]
exact antitone_lowerCentralSeries R L M (by linarith)
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
x y : L
k : ℕ
hM : lowerCentralSeries R L M k = ⊥
⊢ k ≤ 2 * k
[PROOFSTEP]
linarith
[GOAL]
case intro
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
x y : L
k : ℕ
hM : lowerCentralSeries R L M (2 * k) = ⊥
⊢ _root_.IsNilpotent (LinearMap.comp (↑(toEndomorphism R L M) x) (↑(toEndomorphism R L M) y))
[PROOFSTEP]
use k
[GOAL]
case h
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
x y : L
k : ℕ
hM : lowerCentralSeries R L M (2 * k) = ⊥
⊢ LinearMap.comp (↑(toEndomorphism R L M) x) (↑(toEndomorphism R L M) y) ^ k = 0
[PROOFSTEP]
ext m
[GOAL]
case h.h
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
x y : L
k : ℕ
hM : lowerCentralSeries R L M (2 * k) = ⊥
m : M
⊢ ↑(LinearMap.comp (↑(toEndomorphism R L M) x) (↑(toEndomorphism R L M) y) ^ k) m = ↑0 m
[PROOFSTEP]
rw [LinearMap.pow_apply, LinearMap.zero_apply, ← LieSubmodule.mem_bot (R := R) (L := L), ← hM]
[GOAL]
case h.h
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
x y : L
k : ℕ
hM : lowerCentralSeries R L M (2 * k) = ⊥
m : M
⊢ (↑(LinearMap.comp (↑(toEndomorphism R L M) x) (↑(toEndomorphism R L M) y)))^[k] m ∈ lowerCentralSeries R L M (2 * k)
[PROOFSTEP]
exact iterate_toEndomorphism_mem_lowerCentralSeries₂ R L M x y m k
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
⊢ ⨅ (x : L), Module.End.maximalGeneralizedEigenspace (↑(toEndomorphism R L M) x) 0 = ⊤
[PROOFSTEP]
ext m
[GOAL]
case h
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
m : M
⊢ m ∈ ⨅ (x : L), Module.End.maximalGeneralizedEigenspace (↑(toEndomorphism R L M) x) 0 ↔ m ∈ ⊤
[PROOFSTEP]
simp only [Module.End.mem_maximalGeneralizedEigenspace, Submodule.mem_top, sub_zero, iff_true_iff, zero_smul,
  Submodule.mem_iInf]
[GOAL]
case h
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
m : M
⊢ ∀ (i : L), ∃ k, ↑(↑(toEndomorphism R L M) i ^ k) m = 0
[PROOFSTEP]
intro x
[GOAL]
case h
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
m : M
x : L
⊢ ∃ k, ↑(↑(toEndomorphism R L M) x ^ k) m = 0
[PROOFSTEP]
obtain ⟨k, hk⟩ := exists_forall_pow_toEndomorphism_eq_zero R L M
[GOAL]
case h.intro
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
m : M
x : L
k : ℕ
hk : ∀ (x : L), ↑(toEndomorphism R L M) x ^ k = 0
⊢ ∃ k, ↑(↑(toEndomorphism R L M) x ^ k) m = 0
[PROOFSTEP]
use k
[GOAL]
case h
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
m : M
x : L
k : ℕ
hk : ∀ (x : L), ↑(toEndomorphism R L M) x ^ k = 0
⊢ ↑(↑(toEndomorphism R L M) x ^ k) m = 0
[PROOFSTEP]
rw [hk]
[GOAL]
case h
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
m : M
x : L
k : ℕ
hk : ∀ (x : L), ↑(toEndomorphism R L M) x ^ k = 0
⊢ ↑0 m = 0
[PROOFSTEP]
exact LinearMap.zero_apply m
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N✝ N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
h₂ : IsNilpotent R L (M ⧸ N)
⊢ IsNilpotent R L M
[PROOFSTEP]
obtain ⟨k, hk⟩ := h₂
[GOAL]
case mk.intro
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N✝ N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : lowerCentralSeries R L (M ⧸ N) k = ⊥
⊢ IsNilpotent R L M
[PROOFSTEP]
use k + 1
[GOAL]
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N✝ N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : lowerCentralSeries R L (M ⧸ N) k = ⊥
⊢ lowerCentralSeries R L M (k + 1) = ⊥
[PROOFSTEP]
simp only [lowerCentralSeries_succ]
[GOAL]
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N✝ N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : lowerCentralSeries R L (M ⧸ N) k = ⊥
⊢ ⁅⊤, lowerCentralSeries R L M k⁆ = ⊥
[PROOFSTEP]
suffices lowerCentralSeries R L M k ≤ N
  by
  replace this := LieSubmodule.mono_lie_right _ _ ⊤ (le_trans this h₁)
  rwa [ideal_oper_maxTrivSubmodule_eq_bot, le_bot_iff] at this
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N✝ N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : lowerCentralSeries R L (M ⧸ N) k = ⊥
this : lowerCentralSeries R L M k ≤ N
⊢ ⁅⊤, lowerCentralSeries R L M k⁆ = ⊥
[PROOFSTEP]
replace this := LieSubmodule.mono_lie_right _ _ ⊤ (le_trans this h₁)
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N✝ N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : lowerCentralSeries R L (M ⧸ N) k = ⊥
this : ⁅⊤, lowerCentralSeries R L M k⁆ ≤ ⁅⊤, maxTrivSubmodule R L M⁆
⊢ ⁅⊤, lowerCentralSeries R L M k⁆ = ⊥
[PROOFSTEP]
rwa [ideal_oper_maxTrivSubmodule_eq_bot, le_bot_iff] at this
[GOAL]
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N✝ N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : lowerCentralSeries R L (M ⧸ N) k = ⊥
⊢ lowerCentralSeries R L M k ≤ N
[PROOFSTEP]
rw [← LieSubmodule.Quotient.map_mk'_eq_bot_le, ← le_bot_iff, ← hk]
[GOAL]
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N✝ N : LieSubmodule R L M
h₁ : N ≤ maxTrivSubmodule R L M
k : ℕ
hk : lowerCentralSeries R L (M ⧸ N) k = ⊥
⊢ LieSubmodule.map (LieSubmodule.Quotient.mk' N) (lowerCentralSeries R L M k) ≤ lowerCentralSeries R L (M ⧸ N) k
[PROOFSTEP]
exact map_lowerCentralSeries_le k (LieSubmodule.Quotient.mk' N)
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
⊢ nilpotencyLength R L M = 0 ↔ Subsingleton M
[PROOFSTEP]
let s := {k | lowerCentralSeries R L M k = ⊥}
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
⊢ nilpotencyLength R L M = 0 ↔ Subsingleton M
[PROOFSTEP]
have hs : s.Nonempty := by
  obtain ⟨k, hk⟩ := (by infer_instance : IsNilpotent R L M)
  exact ⟨k, hk⟩
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
⊢ Set.Nonempty s
[PROOFSTEP]
obtain ⟨k, hk⟩ := (by infer_instance : IsNilpotent R L M)
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
⊢ IsNilpotent R L M
[PROOFSTEP]
infer_instance
[GOAL]
case mk.intro
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
k : ℕ
hk : lowerCentralSeries R L M k = ⊥
⊢ Set.Nonempty s
[PROOFSTEP]
exact ⟨k, hk⟩
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
hs : Set.Nonempty s
⊢ nilpotencyLength R L M = 0 ↔ Subsingleton M
[PROOFSTEP]
change sInf s = 0 ↔ _
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
hs : Set.Nonempty s
⊢ sInf s = 0 ↔ Subsingleton M
[PROOFSTEP]
rw [← LieSubmodule.subsingleton_iff R L M, ← subsingleton_iff_bot_eq_top, ← lowerCentralSeries_zero,
  @eq_comm (LieSubmodule R L M)]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
hs : Set.Nonempty s
⊢ sInf s = 0 ↔ lowerCentralSeries R L M 0 = ⊥
[PROOFSTEP]
refine' ⟨fun h => h ▸ Nat.sInf_mem hs, fun h => _⟩
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
hs : Set.Nonempty s
h : lowerCentralSeries R L M 0 = ⊥
⊢ sInf s = 0
[PROOFSTEP]
rw [Nat.sInf_eq_zero]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝ : IsNilpotent R L M
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
hs : Set.Nonempty s
h : lowerCentralSeries R L M 0 = ⊥
⊢ 0 ∈ s ∨ s = ∅
[PROOFSTEP]
exact Or.inl h
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
⊢ nilpotencyLength R L M = k + 1 ↔ lowerCentralSeries R L M (k + 1) = ⊥ ∧ lowerCentralSeries R L M k ≠ ⊥
[PROOFSTEP]
let s := {k | lowerCentralSeries R L M k = ⊥}
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
⊢ nilpotencyLength R L M = k + 1 ↔ lowerCentralSeries R L M (k + 1) = ⊥ ∧ lowerCentralSeries R L M k ≠ ⊥
[PROOFSTEP]
change sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
⊢ sInf s = k + 1 ↔ k + 1 ∈ s ∧ ¬k ∈ s
[PROOFSTEP]
have hs : ∀ k₁ k₂, k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s :=
  by
  rintro k₁ k₂ h₁₂ (h₁ : lowerCentralSeries R L M k₁ = ⊥)
  exact eq_bot_iff.mpr (h₁ ▸ antitone_lowerCentralSeries R L M h₁₂)
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
⊢ ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
[PROOFSTEP]
rintro k₁ k₂ h₁₂ (h₁ : lowerCentralSeries R L M k₁ = ⊥)
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
k₁ k₂ : ℕ
h₁₂ : k₁ ≤ k₂
h₁ : lowerCentralSeries R L M k₁ = ⊥
⊢ k₂ ∈ s
[PROOFSTEP]
exact eq_bot_iff.mpr (h₁ ▸ antitone_lowerCentralSeries R L M h₁₂)
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
s : Set ℕ := {k | lowerCentralSeries R L M k = ⊥}
hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s
⊢ sInf s = k + 1 ↔ k + 1 ∈ s ∧ ¬k ∈ s
[PROOFSTEP]
exact Nat.sInf_upward_closed_eq_succ_iff hs k
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
⊢ lowerCentralSeriesLast R L M ≤ maxTrivSubmodule R L M
[PROOFSTEP]
rw [lowerCentralSeriesLast]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
⊢ (match nilpotencyLength R L M with
    | 0 => ⊥
    | Nat.succ k => lowerCentralSeries R L M k) ≤
    maxTrivSubmodule R L M
[PROOFSTEP]
cases' h : nilpotencyLength R L M with k
[GOAL]
case zero
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
h : nilpotencyLength R L M = Nat.zero
⊢ (match Nat.zero with
    | 0 => ⊥
    | Nat.succ k => lowerCentralSeries R L M k) ≤
    maxTrivSubmodule R L M
[PROOFSTEP]
exact bot_le
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
h : nilpotencyLength R L M = Nat.succ k
⊢ (match Nat.succ k with
    | 0 => ⊥
    | Nat.succ k => lowerCentralSeries R L M k) ≤
    maxTrivSubmodule R L M
[PROOFSTEP]
rw [le_max_triv_iff_bracket_eq_bot]
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
h : nilpotencyLength R L M = Nat.succ k
⊢ ⁅⊤,
      match Nat.succ k with
      | 0 => ⊥
      | Nat.succ k => lowerCentralSeries R L M k⁆ =
    ⊥
[PROOFSTEP]
rw [nilpotencyLength_eq_succ_iff, lowerCentralSeries_succ] at h
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
h : ⁅⊤, lowerCentralSeries R L M k⁆ = ⊥ ∧ lowerCentralSeries R L M k ≠ ⊥
⊢ ⁅⊤,
      match Nat.succ k with
      | 0 => ⊥
      | Nat.succ k => lowerCentralSeries R L M k⁆ =
    ⊥
[PROOFSTEP]
exact h.1
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝¹ : Nontrivial M
inst✝ : IsNilpotent R L M
⊢ Nontrivial { x // x ∈ ↑(lowerCentralSeriesLast R L M) }
[PROOFSTEP]
rw [LieSubmodule.nontrivial_iff_ne_bot, lowerCentralSeriesLast]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝¹ : Nontrivial M
inst✝ : IsNilpotent R L M
⊢ (match nilpotencyLength R L M with
    | 0 => ⊥
    | Nat.succ k => lowerCentralSeries R L M k) ≠
    ⊥
[PROOFSTEP]
cases h : nilpotencyLength R L M
[GOAL]
case zero
R : Type u
L : Type v
M : Type w
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝¹ : Nontrivial M
inst✝ : IsNilpotent R L M
h : nilpotencyLength R L M = Nat.zero
⊢ (match Nat.zero with
    | 0 => ⊥
    | Nat.succ k => lowerCentralSeries R L M k) ≠
    ⊥
[PROOFSTEP]
rw [nilpotencyLength_eq_zero_iff, ← not_nontrivial_iff_subsingleton] at h
[GOAL]
case zero
R : Type u
L : Type v
M : Type w
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝¹ : Nontrivial M
inst✝ : IsNilpotent R L M
h : ¬Nontrivial M
⊢ (match Nat.zero with
    | 0 => ⊥
    | Nat.succ k => lowerCentralSeries R L M k) ≠
    ⊥
[PROOFSTEP]
contradiction
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝¹ : Nontrivial M
inst✝ : IsNilpotent R L M
n✝ : ℕ
h : nilpotencyLength R L M = Nat.succ n✝
⊢ (match Nat.succ n✝ with
    | 0 => ⊥
    | Nat.succ k => lowerCentralSeries R L M k) ≠
    ⊥
[PROOFSTEP]
rw [nilpotencyLength_eq_succ_iff] at h
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
k : ℕ
N : LieSubmodule R L M
inst✝¹ : Nontrivial M
inst✝ : IsNilpotent R L M
n✝ : ℕ
h : lowerCentralSeries R L M (n✝ + 1) = ⊥ ∧ lowerCentralSeries R L M n✝ ≠ ⊥
⊢ (match Nat.succ n✝ with
    | 0 => ⊥
    | Nat.succ k => lowerCentralSeries R L M k) ≠
    ⊥
[PROOFSTEP]
exact h.2
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
⊢ ↑(lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M k) = ↑(lowerCentralSeries R L M k)
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
⊢ ↑(lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M Nat.zero) =
    ↑(lowerCentralSeries R L M Nat.zero)
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M k) = ↑(lowerCentralSeries R L M k)
⊢ ↑(lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M (Nat.succ k)) =
    ↑(lowerCentralSeries R L M (Nat.succ k))
[PROOFSTEP]
simp only [lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', ←
  (lowerCentralSeries R (toEndomorphism R L M).range M k).mem_coeSubmodule, ih]
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M k) = ↑(lowerCentralSeries R L M k)
⊢ Submodule.span R {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ ↑(lowerCentralSeries R L M k) ∧ ⁅x, n⁆ = m} =
    Submodule.span R {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m}
[PROOFSTEP]
congr
[GOAL]
case succ.e_s
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M k) = ↑(lowerCentralSeries R L M k)
⊢ {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ ↑(lowerCentralSeries R L M k) ∧ ⁅x, n⁆ = m} =
    {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m}
[PROOFSTEP]
ext m
[GOAL]
case succ.e_s.h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M k) = ↑(lowerCentralSeries R L M k)
m : M
⊢ m ∈ {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ ↑(lowerCentralSeries R L M k) ∧ ⁅x, n⁆ = m} ↔
    m ∈ {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m}
[PROOFSTEP]
constructor
[GOAL]
case succ.e_s.h.mp
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M k) = ↑(lowerCentralSeries R L M k)
m : M
⊢ m ∈ {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ ↑(lowerCentralSeries R L M k) ∧ ⁅x, n⁆ = m} →
    m ∈ {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m}
[PROOFSTEP]
rintro ⟨⟨-, ⟨y, rfl⟩⟩, -, n, hn, rfl⟩
[GOAL]
case succ.e_s.h.mp.intro.mk.intro.intro.intro.intro
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M k) = ↑(lowerCentralSeries R L M k)
y : L
n : M
hn : n ∈ ↑(lowerCentralSeries R L M k)
⊢ ⁅{ val := ↑↑(toEndomorphism R L M) y,
        property := (_ : ∃ y_1, ↑↑(toEndomorphism R L M) y_1 = ↑↑(toEndomorphism R L M) y) },
      n⁆ ∈
    {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m}
[PROOFSTEP]
exact ⟨y, LieSubmodule.mem_top _, n, hn, rfl⟩
[GOAL]
case succ.e_s.h.mpr
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M k) = ↑(lowerCentralSeries R L M k)
m : M
⊢ m ∈ {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m} →
    m ∈ {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ ↑(lowerCentralSeries R L M k) ∧ ⁅x, n⁆ = m}
[PROOFSTEP]
rintro ⟨x, -, n, hn, rfl⟩
[GOAL]
case succ.e_s.h.mpr.intro.intro.intro.intro
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M k) = ↑(lowerCentralSeries R L M k)
x : L
n : M
hn : n ∈ lowerCentralSeries R L M k
⊢ ⁅x, n⁆ ∈ {m | ∃ x, x ∈ ⊤ ∧ ∃ n, n ∈ ↑(lowerCentralSeries R L M k) ∧ ⁅x, n⁆ = m}
[PROOFSTEP]
exact ⟨⟨toEndomorphism R L M x, LieHom.mem_range_self _ x⟩, LieSubmodule.mem_top _, n, hn, rfl⟩
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
⊢ IsNilpotent R { x // x ∈ LieHom.range (toEndomorphism R L M) } M ↔ IsNilpotent R L M
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
⊢ IsNilpotent R { x // x ∈ LieHom.range (toEndomorphism R L M) } M → IsNilpotent R L M
[PROOFSTEP]
rintro ⟨k, hk⟩
[GOAL]
case mpr
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
⊢ IsNilpotent R L M → IsNilpotent R { x // x ∈ LieHom.range (toEndomorphism R L M) } M
[PROOFSTEP]
rintro ⟨k, hk⟩
[GOAL]
case mp.mk.intro
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
hk : lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M k = ⊥
⊢ IsNilpotent R L M
[PROOFSTEP]
use k
[GOAL]
case mpr.mk.intro
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
hk : lowerCentralSeries R L M k = ⊥
⊢ IsNilpotent R { x // x ∈ LieHom.range (toEndomorphism R L M) } M
[PROOFSTEP]
use k
[GOAL]
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
hk : lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M k = ⊥
⊢ lowerCentralSeries R L M k = ⊥
[PROOFSTEP]
rw [← LieSubmodule.coe_toSubmodule_eq_iff] at hk ⊢
[GOAL]
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
hk : lowerCentralSeries R L M k = ⊥
⊢ lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M k = ⊥
[PROOFSTEP]
rw [← LieSubmodule.coe_toSubmodule_eq_iff] at hk ⊢
[GOAL]
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
hk : ↑(lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M k) = ↑⊥
⊢ ↑(lowerCentralSeries R L M k) = ↑⊥
[PROOFSTEP]
simpa using hk
[GOAL]
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
k : ℕ
hk : ↑(lowerCentralSeries R L M k) = ↑⊥
⊢ ↑(lowerCentralSeries R { x // x ∈ LieHom.range (toEndomorphism R L M) } M k) = ↑⊥
[PROOFSTEP]
simpa using hk
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N N₁ N₂ : LieSubmodule R L M
k : ℕ
h : N₁ ≤ N₂
⊢ ucs k N₁ ≤ ucs k N₂
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N N₁ N₂ : LieSubmodule R L M
h : N₁ ≤ N₂
⊢ ucs Nat.zero N₁ ≤ ucs Nat.zero N₂
[PROOFSTEP]
simpa
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N N₁ N₂ : LieSubmodule R L M
h : N₁ ≤ N₂
k : ℕ
ih : ucs k N₁ ≤ ucs k N₂
⊢ ucs (Nat.succ k) N₁ ≤ ucs (Nat.succ k) N₂
[PROOFSTEP]
simp only [ucs_succ]
  -- Porting note: `mono` makes no progress
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N N₁ N₂ : LieSubmodule R L M
h : N₁ ≤ N₂
k : ℕ
ih : ucs k N₁ ≤ ucs k N₂
⊢ normalizer (ucs k N₁) ≤ normalizer (ucs k N₂)
[PROOFSTEP]
apply monotone_normalizer ih
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N N₁ N₂ : LieSubmodule R L M
h : normalizer N₁ = N₁
k : ℕ
⊢ ucs k N₁ = N₁
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N N₁ N₂ : LieSubmodule R L M
h : normalizer N₁ = N₁
⊢ ucs Nat.zero N₁ = N₁
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N N₁ N₂ : LieSubmodule R L M
h : normalizer N₁ = N₁
k : ℕ
ih : ucs k N₁ = N₁
⊢ ucs (Nat.succ k) N₁ = N₁
[PROOFSTEP]
rwa [ucs_succ, ih]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N N₁ N₂ : LieSubmodule R L M
h : normalizer N₁ = N₁
k : ℕ
⊢ ucs k ⊥ ≤ N₁
[PROOFSTEP]
rw [← ucs_eq_self_of_normalizer_eq_self h k]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N N₁ N₂ : LieSubmodule R L M
h : normalizer N₁ = N₁
k : ℕ
⊢ ucs k ⊥ ≤ ucs k N₁
[PROOFSTEP]
mono
[GOAL]
case h
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N N₁ N₂ : LieSubmodule R L M
h : normalizer N₁ = N₁
k : ℕ
h_symm : N₁ = normalizer N₁
⊢ ⊥ ≤ N₁
[PROOFSTEP]
simp
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N N₁ N₂ : LieSubmodule R L M
l k : ℕ
⊢ lcs (l + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs k N₂
[PROOFSTEP]
induction' k with k ih generalizing l
[GOAL]
case zero
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N N₁ N₂ : LieSubmodule R L M
l✝ l : ℕ
⊢ lcs (l + Nat.zero) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs Nat.zero N₂
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N N₁ N₂ : LieSubmodule R L M
l✝ k : ℕ
ih : ∀ (l : ℕ), lcs (l + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs k N₂
l : ℕ
⊢ lcs (l + Nat.succ k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs (Nat.succ k) N₂
[PROOFSTEP]
rw [(by abel : l + (k + 1) = l + 1 + k), ih, ucs_succ, lcs_succ, top_lie_le_iff_le_normalizer]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N N₁ N₂ : LieSubmodule R L M
l✝ k : ℕ
ih : ∀ (l : ℕ), lcs (l + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs k N₂
l : ℕ
⊢ l + (k + 1) = l + 1 + k
[PROOFSTEP]
abel
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N N₁ N₂ : LieSubmodule R L M
l✝ k : ℕ
ih : ∀ (l : ℕ), lcs (l + k) N₁ ≤ N₂ ↔ lcs l N₁ ≤ ucs k N₂
l : ℕ
⊢ l + (k + 1) = l + 1 + k
[PROOFSTEP]
abel
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N N₁ N₂ : LieSubmodule R L M
k : ℕ
⊢ lcs k N₁ ≤ N₂ ↔ N₁ ≤ ucs k N₂
[PROOFSTEP]
convert lcs_add_le_iff (R := R) (L := L) (M := M) 0 k
[GOAL]
case h.e'_1.h.e'_3.h.e'_10
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N N₁ N₂ : LieSubmodule R L M
k : ℕ
⊢ k = 0 + k
[PROOFSTEP]
rw [zero_add]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N N₁ N₂ : LieSubmodule R L M
k : ℕ
⊢ ucs k N = ⊤ ↔ LieModule.lowerCentralSeries R L M k ≤ N
[PROOFSTEP]
rw [eq_top_iff, ← lcs_le_iff]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N N₁ N₂ : LieSubmodule R L M
k : ℕ
⊢ lcs k ⊤ ≤ N ↔ LieModule.lowerCentralSeries R L M k ≤ N
[PROOFSTEP]
rfl
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N N₁ N₂ : LieSubmodule R L M
⊢ LieModule.IsNilpotent R L M ↔ ∃ k, ucs k ⊥ = ⊤
[PROOFSTEP]
rw [LieModule.isNilpotent_iff]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N N₁ N₂ : LieSubmodule R L M
⊢ (∃ k, LieModule.lowerCentralSeries R L M k = ⊥) ↔ ∃ k, ucs k ⊥ = ⊤
[PROOFSTEP]
exact exists_congr fun k => by simp [ucs_eq_top_iff]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N N₁ N₂ : LieSubmodule R L M
k : ℕ
⊢ LieModule.lowerCentralSeries R L M k = ⊥ ↔ ucs k ⊥ = ⊤
[PROOFSTEP]
simp [ucs_eq_top_iff]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N N₁ N₂ : LieSubmodule R L M
k : ℕ
⊢ comap (incl N) (ucs k ⊥) = ucs k ⊥
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N N₁ N₂ : LieSubmodule R L M
⊢ comap (incl N) (ucs Nat.zero ⊥) = ucs Nat.zero ⊥
[PROOFSTEP]
exact N.ker_incl
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ : ℕ
N N₁ N₂ : LieSubmodule R L M
k : ℕ
ih : comap (incl N) (ucs k ⊥) = ucs k ⊥
⊢ comap (incl N) (ucs (Nat.succ k) ⊥) = ucs (Nat.succ k) ⊥
[PROOFSTEP]
simp [← ih]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
N N₁ N₂ : LieSubmodule R L M
⊢ LieModule.IsNilpotent R L { x // x ∈ ↑N } ↔ ∃ k, N ≤ ucs k ⊥
[PROOFSTEP]
simp_rw [LieModule.isNilpotent_iff_exists_ucs_eq_top, ← ucs_comap_incl, comap_incl_eq_top]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L₂ M₂
inst✝ : LieModule R L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hf : Surjective ↑f
hg : Surjective ↑g
hfg : ∀ (x : L) (m : M), ⁅↑f x, ↑g m⁆ = ↑g ⁅x, m⁆
k : ℕ
⊢ Submodule.map g ↑(lowerCentralSeries R L M k) = ↑(lowerCentralSeries R L₂ M₂ k)
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
L : Type v
M : Type w
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L₂ M₂
inst✝ : LieModule R L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hf : Surjective ↑f
hg : Surjective ↑g
hfg : ∀ (x : L) (m : M), ⁅↑f x, ↑g m⁆ = ↑g ⁅x, m⁆
⊢ Submodule.map g ↑(lowerCentralSeries R L M Nat.zero) = ↑(lowerCentralSeries R L₂ M₂ Nat.zero)
[PROOFSTEP]
simpa [LinearMap.range_eq_top]
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L₂ M₂
inst✝ : LieModule R L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hf : Surjective ↑f
hg : Surjective ↑g
hfg : ∀ (x : L) (m : M), ⁅↑f x, ↑g m⁆ = ↑g ⁅x, m⁆
k : ℕ
ih : Submodule.map g ↑(lowerCentralSeries R L M k) = ↑(lowerCentralSeries R L₂ M₂ k)
⊢ Submodule.map g ↑(lowerCentralSeries R L M (Nat.succ k)) = ↑(lowerCentralSeries R L₂ M₂ (Nat.succ k))
[PROOFSTEP]
suffices
  g '' {m | ∃ (x : L) (n : _), n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m} =
    {m | ∃ (x : L₂) (n : _), n ∈ lowerCentralSeries R L M k ∧ ⁅x, g n⁆ = m}
  by
  simp only [← LieSubmodule.mem_coeSubmodule] at this
  simp_rw [lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', Submodule.map_span,
    LieSubmodule.mem_top, true_and, ← LieSubmodule.mem_coeSubmodule, this, ← ih, Submodule.mem_map,
    exists_exists_and_eq_and]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L₂ M₂
inst✝ : LieModule R L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hf : Surjective ↑f
hg : Surjective ↑g
hfg : ∀ (x : L) (m : M), ⁅↑f x, ↑g m⁆ = ↑g ⁅x, m⁆
k : ℕ
ih : Submodule.map g ↑(lowerCentralSeries R L M k) = ↑(lowerCentralSeries R L₂ M₂ k)
this :
  ↑g '' {m | ∃ x n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m} =
    {m | ∃ x n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, ↑g n⁆ = m}
⊢ Submodule.map g ↑(lowerCentralSeries R L M (Nat.succ k)) = ↑(lowerCentralSeries R L₂ M₂ (Nat.succ k))
[PROOFSTEP]
simp only [← LieSubmodule.mem_coeSubmodule] at this
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L₂ M₂
inst✝ : LieModule R L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hf : Surjective ↑f
hg : Surjective ↑g
hfg : ∀ (x : L) (m : M), ⁅↑f x, ↑g m⁆ = ↑g ⁅x, m⁆
k : ℕ
ih : Submodule.map g ↑(lowerCentralSeries R L M k) = ↑(lowerCentralSeries R L₂ M₂ k)
this :
  (fun a => ↑g a) '' {m | ∃ x n, n ∈ ↑(lowerCentralSeries R L M k) ∧ ⁅x, n⁆ = m} =
    {m | ∃ x n, n ∈ ↑(lowerCentralSeries R L M k) ∧ ⁅x, ↑g n⁆ = m}
⊢ Submodule.map g ↑(lowerCentralSeries R L M (Nat.succ k)) = ↑(lowerCentralSeries R L₂ M₂ (Nat.succ k))
[PROOFSTEP]
simp_rw [lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', Submodule.map_span, LieSubmodule.mem_top,
  true_and, ← LieSubmodule.mem_coeSubmodule, this, ← ih, Submodule.mem_map, exists_exists_and_eq_and]
[GOAL]
case succ
R : Type u
L : Type v
M : Type w
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L₂ M₂
inst✝ : LieModule R L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hf : Surjective ↑f
hg : Surjective ↑g
hfg : ∀ (x : L) (m : M), ⁅↑f x, ↑g m⁆ = ↑g ⁅x, m⁆
k : ℕ
ih : Submodule.map g ↑(lowerCentralSeries R L M k) = ↑(lowerCentralSeries R L₂ M₂ k)
⊢ ↑g '' {m | ∃ x n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m} =
    {m | ∃ x n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, ↑g n⁆ = m}
[PROOFSTEP]
ext m₂
[GOAL]
case succ.h
R : Type u
L : Type v
M : Type w
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L₂ M₂
inst✝ : LieModule R L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hf : Surjective ↑f
hg : Surjective ↑g
hfg : ∀ (x : L) (m : M), ⁅↑f x, ↑g m⁆ = ↑g ⁅x, m⁆
k : ℕ
ih : Submodule.map g ↑(lowerCentralSeries R L M k) = ↑(lowerCentralSeries R L₂ M₂ k)
m₂ : M₂
⊢ m₂ ∈ ↑g '' {m | ∃ x n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m} ↔
    m₂ ∈ {m | ∃ x n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, ↑g n⁆ = m}
[PROOFSTEP]
constructor
[GOAL]
case succ.h.mp
R : Type u
L : Type v
M : Type w
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L₂ M₂
inst✝ : LieModule R L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hf : Surjective ↑f
hg : Surjective ↑g
hfg : ∀ (x : L) (m : M), ⁅↑f x, ↑g m⁆ = ↑g ⁅x, m⁆
k : ℕ
ih : Submodule.map g ↑(lowerCentralSeries R L M k) = ↑(lowerCentralSeries R L₂ M₂ k)
m₂ : M₂
⊢ m₂ ∈ ↑g '' {m | ∃ x n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m} →
    m₂ ∈ {m | ∃ x n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, ↑g n⁆ = m}
[PROOFSTEP]
rintro ⟨m, ⟨x, n, hn, rfl⟩, rfl⟩
[GOAL]
case succ.h.mp.intro.intro.intro.intro.intro
R : Type u
L : Type v
M : Type w
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L₂ M₂
inst✝ : LieModule R L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hf : Surjective ↑f
hg : Surjective ↑g
hfg : ∀ (x : L) (m : M), ⁅↑f x, ↑g m⁆ = ↑g ⁅x, m⁆
k : ℕ
ih : Submodule.map g ↑(lowerCentralSeries R L M k) = ↑(lowerCentralSeries R L₂ M₂ k)
x : L
n : M
hn : n ∈ lowerCentralSeries R L M k
⊢ ↑g ⁅x, n⁆ ∈ {m | ∃ x n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, ↑g n⁆ = m}
[PROOFSTEP]
exact ⟨f x, n, hn, hfg x n⟩
[GOAL]
case succ.h.mpr
R : Type u
L : Type v
M : Type w
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L₂ M₂
inst✝ : LieModule R L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hf : Surjective ↑f
hg : Surjective ↑g
hfg : ∀ (x : L) (m : M), ⁅↑f x, ↑g m⁆ = ↑g ⁅x, m⁆
k : ℕ
ih : Submodule.map g ↑(lowerCentralSeries R L M k) = ↑(lowerCentralSeries R L₂ M₂ k)
m₂ : M₂
⊢ m₂ ∈ {m | ∃ x n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, ↑g n⁆ = m} →
    m₂ ∈ ↑g '' {m | ∃ x n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m}
[PROOFSTEP]
rintro ⟨x, n, hn, rfl⟩
[GOAL]
case succ.h.mpr.intro.intro.intro
R : Type u
L : Type v
M : Type w
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L₂ M₂
inst✝ : LieModule R L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hf : Surjective ↑f
hg : Surjective ↑g
hfg : ∀ (x : L) (m : M), ⁅↑f x, ↑g m⁆ = ↑g ⁅x, m⁆
k : ℕ
ih : Submodule.map g ↑(lowerCentralSeries R L M k) = ↑(lowerCentralSeries R L₂ M₂ k)
x : L₂
n : M
hn : n ∈ lowerCentralSeries R L M k
⊢ ⁅x, ↑g n⁆ ∈ ↑g '' {m | ∃ x n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m}
[PROOFSTEP]
obtain ⟨y, rfl⟩ := hf x
[GOAL]
case succ.h.mpr.intro.intro.intro.intro
R : Type u
L : Type v
M : Type w
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L₂ M₂
inst✝ : LieModule R L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hf : Surjective ↑f
hg : Surjective ↑g
hfg : ∀ (x : L) (m : M), ⁅↑f x, ↑g m⁆ = ↑g ⁅x, m⁆
k : ℕ
ih : Submodule.map g ↑(lowerCentralSeries R L M k) = ↑(lowerCentralSeries R L₂ M₂ k)
n : M
hn : n ∈ lowerCentralSeries R L M k
y : L
⊢ ⁅↑f y, ↑g n⁆ ∈ ↑g '' {m | ∃ x n, n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m}
[PROOFSTEP]
exact ⟨⁅y, n⁆, ⟨y, n, hn, rfl⟩, (hfg y n).symm⟩
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝¹³ : CommRing R
inst✝¹² : LieRing L
inst✝¹¹ : LieAlgebra R L
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : LieRingModule L M
inst✝⁷ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L₂ M₂
inst✝¹ : LieModule R L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hf : Surjective ↑f
hg : Surjective ↑g
hfg : ∀ (x : L) (m : M), ⁅↑f x, ↑g m⁆ = ↑g ⁅x, m⁆
inst✝ : LieModule.IsNilpotent R L M
⊢ LieModule.IsNilpotent R L₂ M₂
[PROOFSTEP]
obtain ⟨k, hk⟩ := id (by infer_instance : IsNilpotent R L M)
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝¹³ : CommRing R
inst✝¹² : LieRing L
inst✝¹¹ : LieAlgebra R L
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : LieRingModule L M
inst✝⁷ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L₂ M₂
inst✝¹ : LieModule R L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hf : Surjective ↑f
hg : Surjective ↑g
hfg : ∀ (x : L) (m : M), ⁅↑f x, ↑g m⁆ = ↑g ⁅x, m⁆
inst✝ : LieModule.IsNilpotent R L M
⊢ LieModule.IsNilpotent R L M
[PROOFSTEP]
infer_instance
[GOAL]
case mk.intro
R : Type u
L : Type v
M : Type w
inst✝¹³ : CommRing R
inst✝¹² : LieRing L
inst✝¹¹ : LieAlgebra R L
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : LieRingModule L M
inst✝⁷ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L₂ M₂
inst✝¹ : LieModule R L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hf : Surjective ↑f
hg : Surjective ↑g
hfg : ∀ (x : L) (m : M), ⁅↑f x, ↑g m⁆ = ↑g ⁅x, m⁆
inst✝ : LieModule.IsNilpotent R L M
k : ℕ
hk : lowerCentralSeries R L M k = ⊥
⊢ LieModule.IsNilpotent R L₂ M₂
[PROOFSTEP]
use k
[GOAL]
case h
R : Type u
L : Type v
M : Type w
inst✝¹³ : CommRing R
inst✝¹² : LieRing L
inst✝¹¹ : LieAlgebra R L
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : LieRingModule L M
inst✝⁷ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L₂ M₂
inst✝¹ : LieModule R L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hf : Surjective ↑f
hg : Surjective ↑g
hfg : ∀ (x : L) (m : M), ⁅↑f x, ↑g m⁆ = ↑g ⁅x, m⁆
inst✝ : LieModule.IsNilpotent R L M
k : ℕ
hk : lowerCentralSeries R L M k = ⊥
⊢ lowerCentralSeries R L₂ M₂ k = ⊥
[PROOFSTEP]
rw [← LieSubmodule.coe_toSubmodule_eq_iff] at hk ⊢
[GOAL]
case h
R : Type u
L : Type v
M : Type w
inst✝¹³ : CommRing R
inst✝¹² : LieRing L
inst✝¹¹ : LieAlgebra R L
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : LieRingModule L M
inst✝⁷ : LieModule R L M
k✝ : ℕ
N : LieSubmodule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁶ : LieRing L₂
inst✝⁵ : LieAlgebra R L₂
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R M₂
inst✝² : LieRingModule L₂ M₂
inst✝¹ : LieModule R L₂ M₂
f : L →ₗ⁅R⁆ L₂
g : M →ₗ[R] M₂
hf : Surjective ↑f
hg : Surjective ↑g
hfg : ∀ (x : L) (m : M), ⁅↑f x, ↑g m⁆ = ↑g ⁅x, m⁆
inst✝ : LieModule.IsNilpotent R L M
k : ℕ
hk : ↑(lowerCentralSeries R L M k) = ↑⊥
⊢ ↑(lowerCentralSeries R L₂ M₂ k) = ↑⊥
[PROOFSTEP]
simp [← hf.lieModule_lcs_map_eq hg hfg k, hk]
[GOAL]
R : Type u
L : Type v
M : Type w
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L₂ M₂
inst✝ : LieModule R L₂ M₂
f✝ : L →ₗ⁅R⁆ L₂
g✝ : M →ₗ[R] M₂
hf : Surjective ↑f✝
hg : Surjective ↑g✝
hfg✝ : ∀ (x : L) (m : M), ⁅↑f✝ x, ↑g✝ m⁆ = ↑g✝ ⁅x, m⁆
f : L ≃ₗ⁅R⁆ L₂
g : M ≃ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅↑f x, ↑g m⁆ = ↑g ⁅x, m⁆
⊢ LieModule.IsNilpotent R L M ↔ LieModule.IsNilpotent R L₂ M₂
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
L : Type v
M : Type w
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L₂ M₂
inst✝ : LieModule R L₂ M₂
f✝ : L →ₗ⁅R⁆ L₂
g✝ : M →ₗ[R] M₂
hf : Surjective ↑f✝
hg : Surjective ↑g✝
hfg✝ : ∀ (x : L) (m : M), ⁅↑f✝ x, ↑g✝ m⁆ = ↑g✝ ⁅x, m⁆
f : L ≃ₗ⁅R⁆ L₂
g : M ≃ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅↑f x, ↑g m⁆ = ↑g ⁅x, m⁆
⊢ LieModule.IsNilpotent R L M → LieModule.IsNilpotent R L₂ M₂
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u
L : Type v
M : Type w
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L₂ M₂
inst✝ : LieModule R L₂ M₂
f✝ : L →ₗ⁅R⁆ L₂
g✝ : M →ₗ[R] M₂
hf : Surjective ↑f✝
hg : Surjective ↑g✝
hfg✝ : ∀ (x : L) (m : M), ⁅↑f✝ x, ↑g✝ m⁆ = ↑g✝ ⁅x, m⁆
f : L ≃ₗ⁅R⁆ L₂
g : M ≃ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅↑f x, ↑g m⁆ = ↑g ⁅x, m⁆
⊢ LieModule.IsNilpotent R L₂ M₂ → LieModule.IsNilpotent R L M
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u
L : Type v
M : Type w
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L₂ M₂
inst✝ : LieModule R L₂ M₂
f✝ : L →ₗ⁅R⁆ L₂
g✝ : M →ₗ[R] M₂
hf : Surjective ↑f✝
hg : Surjective ↑g✝
hfg✝ : ∀ (x : L) (m : M), ⁅↑f✝ x, ↑g✝ m⁆ = ↑g✝ ⁅x, m⁆
f : L ≃ₗ⁅R⁆ L₂
g : M ≃ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅↑f x, ↑g m⁆ = ↑g ⁅x, m⁆
h : LieModule.IsNilpotent R L M
⊢ LieModule.IsNilpotent R L₂ M₂
[PROOFSTEP]
have hg : Surjective (g : M →ₗ[R] M₂) := g.surjective
[GOAL]
case mp
R : Type u
L : Type v
M : Type w
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L₂ M₂
inst✝ : LieModule R L₂ M₂
f✝ : L →ₗ⁅R⁆ L₂
g✝ : M →ₗ[R] M₂
hf : Surjective ↑f✝
hg✝ : Surjective ↑g✝
hfg✝ : ∀ (x : L) (m : M), ⁅↑f✝ x, ↑g✝ m⁆ = ↑g✝ ⁅x, m⁆
f : L ≃ₗ⁅R⁆ L₂
g : M ≃ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅↑f x, ↑g m⁆ = ↑g ⁅x, m⁆
h : LieModule.IsNilpotent R L M
hg : Surjective ↑↑g
⊢ LieModule.IsNilpotent R L₂ M₂
[PROOFSTEP]
exact f.surjective.lieModuleIsNilpotent hg hfg
[GOAL]
case mpr
R : Type u
L : Type v
M : Type w
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L₂ M₂
inst✝ : LieModule R L₂ M₂
f✝ : L →ₗ⁅R⁆ L₂
g✝ : M →ₗ[R] M₂
hf : Surjective ↑f✝
hg : Surjective ↑g✝
hfg✝ : ∀ (x : L) (m : M), ⁅↑f✝ x, ↑g✝ m⁆ = ↑g✝ ⁅x, m⁆
f : L ≃ₗ⁅R⁆ L₂
g : M ≃ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅↑f x, ↑g m⁆ = ↑g ⁅x, m⁆
h : LieModule.IsNilpotent R L₂ M₂
⊢ LieModule.IsNilpotent R L M
[PROOFSTEP]
have hg : Surjective (g.symm : M₂ →ₗ[R] M) := g.symm.surjective
[GOAL]
case mpr
R : Type u
L : Type v
M : Type w
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L₂ M₂
inst✝ : LieModule R L₂ M₂
f✝ : L →ₗ⁅R⁆ L₂
g✝ : M →ₗ[R] M₂
hf : Surjective ↑f✝
hg✝ : Surjective ↑g✝
hfg✝ : ∀ (x : L) (m : M), ⁅↑f✝ x, ↑g✝ m⁆ = ↑g✝ ⁅x, m⁆
f : L ≃ₗ⁅R⁆ L₂
g : M ≃ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅↑f x, ↑g m⁆ = ↑g ⁅x, m⁆
h : LieModule.IsNilpotent R L₂ M₂
hg : Surjective ↑↑(LinearEquiv.symm g)
⊢ LieModule.IsNilpotent R L M
[PROOFSTEP]
refine' f.symm.surjective.lieModuleIsNilpotent hg fun x m => _
[GOAL]
case mpr
R : Type u
L : Type v
M : Type w
inst✝¹² : CommRing R
inst✝¹¹ : LieRing L
inst✝¹⁰ : LieAlgebra R L
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : LieRingModule L M
inst✝⁶ : LieModule R L M
k : ℕ
N : LieSubmodule R L M
L₂ : Type u_1
M₂ : Type u_2
inst✝⁵ : LieRing L₂
inst✝⁴ : LieAlgebra R L₂
inst✝³ : AddCommGroup M₂
inst✝² : Module R M₂
inst✝¹ : LieRingModule L₂ M₂
inst✝ : LieModule R L₂ M₂
f✝ : L →ₗ⁅R⁆ L₂
g✝ : M →ₗ[R] M₂
hf : Surjective ↑f✝
hg✝ : Surjective ↑g✝
hfg✝ : ∀ (x : L) (m : M), ⁅↑f✝ x, ↑g✝ m⁆ = ↑g✝ ⁅x, m⁆
f : L ≃ₗ⁅R⁆ L₂
g : M ≃ₗ[R] M₂
hfg : ∀ (x : L) (m : M), ⁅↑f x, ↑g m⁆ = ↑g ⁅x, m⁆
h : LieModule.IsNilpotent R L₂ M₂
hg : Surjective ↑↑(LinearEquiv.symm g)
x : L₂
m : M₂
⊢ ⁅↑(LieEquiv.symm f).toLieHom x, ↑↑(LinearEquiv.symm g) m⁆ = ↑↑(LinearEquiv.symm g) ⁅x, m⁆
[PROOFSTEP]
rw [LinearEquiv.coe_coe, LieEquiv.coe_to_lieHom, ← g.symm_apply_apply ⁅f.symm x, g.symm m⁆, ← hfg, f.apply_symm_apply,
  g.apply_symm_apply]
[GOAL]
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
hL : LieModule.IsNilpotent R L L
⊢ IsSolvable R L
[PROOFSTEP]
obtain ⟨k, h⟩ : ∃ k, LieModule.lowerCentralSeries R L L k = ⊥ := hL.nilpotent
[GOAL]
case intro
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
hL : LieModule.IsNilpotent R L L
k : ℕ
h : LieModule.lowerCentralSeries R L L k = ⊥
⊢ IsSolvable R L
[PROOFSTEP]
use k
[GOAL]
case h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
hL : LieModule.IsNilpotent R L L
k : ℕ
h : LieModule.lowerCentralSeries R L L k = ⊥
⊢ derivedSeries R L k = ⊥
[PROOFSTEP]
rw [← le_bot_iff] at h ⊢
[GOAL]
case h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
hL : LieModule.IsNilpotent R L L
k : ℕ
h : LieModule.lowerCentralSeries R L L k ≤ ⊥
⊢ derivedSeries R L k ≤ ⊥
[PROOFSTEP]
exact le_trans (LieModule.derivedSeries_le_lowerCentralSeries R L k) h
[GOAL]
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
k : ℕ
⊢ ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
⊢ ↑(lowerCentralSeries R L (L ⧸ I) Nat.zero) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) Nat.zero)
[PROOFSTEP]
simp only [Nat.zero_eq, LieModule.lowerCentralSeries_zero, LieSubmodule.top_coeSubmodule,
  LieIdeal.top_coe_lieSubalgebra, LieSubalgebra.top_coe_submodule]
[GOAL]
case succ
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
⊢ ↑(lowerCentralSeries R L (L ⧸ I) (Nat.succ k)) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) (Nat.succ k))
[PROOFSTEP]
simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span]
[GOAL]
case succ
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
⊢ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m} = Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
[PROOFSTEP]
congr
[GOAL]
case succ.e_s
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
⊢ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} = {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
[PROOFSTEP]
ext x
[GOAL]
case succ.e_s.h
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
x : L ⧸ I
⊢ x ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ↔ x ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
[PROOFSTEP]
constructor
[GOAL]
case succ.e_s.h.mp
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
x : L ⧸ I
⊢ x ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} → x ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
[PROOFSTEP]
rintro ⟨⟨y, -⟩, ⟨z, hz⟩, rfl : ⁅y, z⁆ = x⟩
[GOAL]
case succ.e_s.h.mp.intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
y : L
z : L ⧸ I
hz : z ∈ lowerCentralSeries R L (L ⧸ I) k
⊢ ⁅y, z⁆ ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
[PROOFSTEP]
erw [← LieSubmodule.mem_coeSubmodule, ih, LieSubmodule.mem_coeSubmodule] at hz
[GOAL]
case succ.e_s.h.mp.intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
y : L
z : L ⧸ I
hz : z ∈ lowerCentralSeries R (L ⧸ I) (L ⧸ I) k
⊢ ⁅y, z⁆ ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
[PROOFSTEP]
exact ⟨⟨LieSubmodule.Quotient.mk y, LieSubmodule.mem_top _⟩, ⟨z, hz⟩, rfl⟩
[GOAL]
case succ.e_s.h.mpr
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
x : L ⧸ I
⊢ x ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} → x ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
[PROOFSTEP]
rintro ⟨⟨⟨y⟩, -⟩, ⟨z, hz⟩, rfl : ⁅y, z⁆ = x⟩
[GOAL]
case succ.e_s.h.mpr.intro.mk.mk.intro.mk
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
val✝ : L ⧸ I
y : L
z : L ⧸ I
hz : z ∈ lowerCentralSeries R (L ⧸ I) (L ⧸ I) k
⊢ ⁅y, z⁆ ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
[PROOFSTEP]
erw [← LieSubmodule.mem_coeSubmodule, ← ih, LieSubmodule.mem_coeSubmodule] at hz
[GOAL]
case succ.e_s.h.mpr.intro.mk.mk.intro.mk
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R L (L ⧸ I) k) = ↑(lowerCentralSeries R (L ⧸ I) (L ⧸ I) k)
val✝ : L ⧸ I
y : L
z : L ⧸ I
hz : z ∈ lowerCentralSeries R L (L ⧸ I) k
⊢ ⁅y, z⁆ ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
[PROOFSTEP]
exact ⟨⟨y, LieSubmodule.mem_top _⟩, ⟨z, hz⟩, rfl⟩
[GOAL]
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
k : ℕ
⊢ ↑(lowerCentralSeries R { x // x ∈ ↑I } { x // x ∈ ↑I } k) ≤ ↑(lowerCentralSeries R L { x // x ∈ ↑I } k)
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
⊢ ↑(lowerCentralSeries R { x // x ∈ ↑I } { x // x ∈ ↑I } Nat.zero) ≤ ↑(lowerCentralSeries R L { x // x ∈ ↑I } Nat.zero)
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ ↑I } { x // x ∈ ↑I } k) ≤ ↑(lowerCentralSeries R L { x // x ∈ ↑I } k)
⊢ ↑(lowerCentralSeries R { x // x ∈ ↑I } { x // x ∈ ↑I } (Nat.succ k)) ≤
    ↑(lowerCentralSeries R L { x // x ∈ ↑I } (Nat.succ k))
[PROOFSTEP]
simp only [LieModule.lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span]
[GOAL]
case succ
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ ↑I } { x // x ∈ ↑I } k) ≤ ↑(lowerCentralSeries R L { x // x ∈ ↑I } k)
⊢ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ≤ Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
[PROOFSTEP]
apply Submodule.span_mono
[GOAL]
case succ.h
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ ↑I } { x // x ∈ ↑I } k) ≤ ↑(lowerCentralSeries R L { x // x ∈ ↑I } k)
⊢ {m | ∃ x n, ⁅↑x, ↑n⁆ = m} ⊆ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
[PROOFSTEP]
rintro x ⟨⟨y, -⟩, ⟨z, hz⟩, rfl : ⁅y, z⁆ = x⟩
[GOAL]
case succ.h.intro.mk.intro.mk
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
k : ℕ
ih : ↑(lowerCentralSeries R { x // x ∈ ↑I } { x // x ∈ ↑I } k) ≤ ↑(lowerCentralSeries R L { x // x ∈ ↑I } k)
y z : { x // x ∈ ↑I }
hz : z ∈ lowerCentralSeries R { x // x ∈ ↑I } { x // x ∈ ↑I } k
⊢ ⁅y, z⁆ ∈ {m | ∃ x n, ⁅↑x, ↑n⁆ = m}
[PROOFSTEP]
exact ⟨⟨y.val, LieSubmodule.mem_top _⟩, ⟨z, ih hz⟩, rfl⟩
[GOAL]
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
h₁ : I ≤ center R L
h₂ : IsNilpotent R (L ⧸ I)
⊢ IsNilpotent R L
[PROOFSTEP]
suffices LieModule.IsNilpotent R L (L ⧸ I) by exact LieModule.nilpotentOfNilpotentQuotient R L L h₁ this
[GOAL]
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
h₁ : I ≤ center R L
h₂ : IsNilpotent R (L ⧸ I)
this : LieModule.IsNilpotent R L (L ⧸ I)
⊢ IsNilpotent R L
[PROOFSTEP]
exact LieModule.nilpotentOfNilpotentQuotient R L L h₁ this
[GOAL]
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
h₁ : I ≤ center R L
h₂ : IsNilpotent R (L ⧸ I)
⊢ LieModule.IsNilpotent R L (L ⧸ I)
[PROOFSTEP]
obtain ⟨k, hk⟩ := h₂
[GOAL]
case mk.intro
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
h₁ : I ≤ center R L
k : ℕ
hk : lowerCentralSeries R (L ⧸ I) (L ⧸ I) k = ⊥
⊢ LieModule.IsNilpotent R L (L ⧸ I)
[PROOFSTEP]
use k
[GOAL]
case h
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
I : LieIdeal R L
h₁ : I ≤ center R L
k : ℕ
hk : lowerCentralSeries R (L ⧸ I) (L ⧸ I) k = ⊥
⊢ lowerCentralSeries R L (L ⧸ I) k = ⊥
[PROOFSTEP]
simp [← LieSubmodule.coe_toSubmodule_eq_iff, coe_lowerCentralSeries_ideal_quot_eq, hk]
[GOAL]
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
k : ℕ
f : L →ₗ⁅R⁆ L'
⊢ map f (lowerCentralSeries R L L k) ≤ lowerCentralSeries R L' L' k
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
⊢ map f (lowerCentralSeries R L L Nat.zero) ≤ lowerCentralSeries R L' L' Nat.zero
[PROOFSTEP]
simp only [Nat.zero_eq, LieModule.lowerCentralSeries_zero, le_top]
[GOAL]
case succ
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
k : ℕ
ih : map f (lowerCentralSeries R L L k) ≤ lowerCentralSeries R L' L' k
⊢ map f (lowerCentralSeries R L L (Nat.succ k)) ≤ lowerCentralSeries R L' L' (Nat.succ k)
[PROOFSTEP]
simp only [LieModule.lowerCentralSeries_succ]
[GOAL]
case succ
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
k : ℕ
ih : map f (lowerCentralSeries R L L k) ≤ lowerCentralSeries R L' L' k
⊢ map f ⁅⊤, lowerCentralSeries R L L k⁆ ≤ ⁅⊤, lowerCentralSeries R L' L' k⁆
[PROOFSTEP]
exact le_trans (LieIdeal.map_bracket_le f) (LieSubmodule.mono_lie _ _ _ _ le_top ih)
[GOAL]
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
k : ℕ
f : L →ₗ⁅R⁆ L'
h : Function.Surjective ↑f
⊢ map f (lowerCentralSeries R L L k) = lowerCentralSeries R L' L' k
[PROOFSTEP]
have h' : (⊤ : LieIdeal R L).map f = ⊤ := by
  rw [← f.idealRange_eq_map]
  exact f.idealRange_eq_top_of_surjective h
[GOAL]
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
k : ℕ
f : L →ₗ⁅R⁆ L'
h : Function.Surjective ↑f
⊢ map f ⊤ = ⊤
[PROOFSTEP]
rw [← f.idealRange_eq_map]
[GOAL]
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
k : ℕ
f : L →ₗ⁅R⁆ L'
h : Function.Surjective ↑f
⊢ LieHom.idealRange f = ⊤
[PROOFSTEP]
exact f.idealRange_eq_top_of_surjective h
[GOAL]
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
k : ℕ
f : L →ₗ⁅R⁆ L'
h : Function.Surjective ↑f
h' : map f ⊤ = ⊤
⊢ map f (lowerCentralSeries R L L k) = lowerCentralSeries R L' L' k
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
h : Function.Surjective ↑f
h' : map f ⊤ = ⊤
⊢ map f (lowerCentralSeries R L L Nat.zero) = lowerCentralSeries R L' L' Nat.zero
[PROOFSTEP]
simp only [LieModule.lowerCentralSeries_zero]
[GOAL]
case zero
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
h : Function.Surjective ↑f
h' : map f ⊤ = ⊤
⊢ map f ⊤ = ⊤
[PROOFSTEP]
exact h'
[GOAL]
case succ
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
h : Function.Surjective ↑f
h' : map f ⊤ = ⊤
k : ℕ
ih : map f (lowerCentralSeries R L L k) = lowerCentralSeries R L' L' k
⊢ map f (lowerCentralSeries R L L (Nat.succ k)) = lowerCentralSeries R L' L' (Nat.succ k)
[PROOFSTEP]
simp only [LieModule.lowerCentralSeries_succ, LieIdeal.map_bracket_eq f h, ih, h']
[GOAL]
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : LieAlgebra.IsNilpotent R L'
f : L →ₗ⁅R⁆ L'
h₂ : Injective ↑f
⊢ ∃ k, lowerCentralSeries R L L k = ⊥
[PROOFSTEP]
obtain ⟨k, hk⟩ := id h₁
[GOAL]
case mk.intro
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : LieAlgebra.IsNilpotent R L'
f : L →ₗ⁅R⁆ L'
h₂ : Injective ↑f
k : ℕ
hk : lowerCentralSeries R L' L' k = ⊥
⊢ ∃ k, lowerCentralSeries R L L k = ⊥
[PROOFSTEP]
use k
[GOAL]
case h
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : LieAlgebra.IsNilpotent R L'
f : L →ₗ⁅R⁆ L'
h₂ : Injective ↑f
k : ℕ
hk : lowerCentralSeries R L' L' k = ⊥
⊢ lowerCentralSeries R L L k = ⊥
[PROOFSTEP]
apply LieIdeal.bot_of_map_eq_bot h₂
[GOAL]
case h
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : LieAlgebra.IsNilpotent R L'
f : L →ₗ⁅R⁆ L'
h₂ : Injective ↑f
k : ℕ
hk : lowerCentralSeries R L' L' k = ⊥
⊢ LieIdeal.map f (lowerCentralSeries R L L k) = ⊥
[PROOFSTEP]
rw [eq_bot_iff, ← hk]
[GOAL]
case h
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : LieAlgebra.IsNilpotent R L'
f : L →ₗ⁅R⁆ L'
h₂ : Injective ↑f
k : ℕ
hk : lowerCentralSeries R L' L' k = ⊥
⊢ LieIdeal.map f (lowerCentralSeries R L L k) ≤ lowerCentralSeries R L' L' k
[PROOFSTEP]
apply LieIdeal.map_lowerCentralSeries_le
[GOAL]
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : LieAlgebra.IsNilpotent R L
f : L →ₗ⁅R⁆ L'
h₂ : Surjective ↑f
⊢ ∃ k, lowerCentralSeries R L' L' k = ⊥
[PROOFSTEP]
obtain ⟨k, hk⟩ := id h₁
[GOAL]
case mk.intro
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : LieAlgebra.IsNilpotent R L
f : L →ₗ⁅R⁆ L'
h₂ : Surjective ↑f
k : ℕ
hk : lowerCentralSeries R L L k = ⊥
⊢ ∃ k, lowerCentralSeries R L' L' k = ⊥
[PROOFSTEP]
use k
[GOAL]
case h
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : LieAlgebra.IsNilpotent R L
f : L →ₗ⁅R⁆ L'
h₂ : Surjective ↑f
k : ℕ
hk : lowerCentralSeries R L L k = ⊥
⊢ lowerCentralSeries R L' L' k = ⊥
[PROOFSTEP]
rw [← LieIdeal.lowerCentralSeries_map_eq k h₂, hk]
[GOAL]
case h
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h₁ : LieAlgebra.IsNilpotent R L
f : L →ₗ⁅R⁆ L'
h₂ : Surjective ↑f
k : ℕ
hk : lowerCentralSeries R L L k = ⊥
⊢ LieIdeal.map f ⊥ = ⊥
[PROOFSTEP]
simp only [LieIdeal.map_eq_bot_iff, bot_le]
[GOAL]
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L ≃ₗ⁅R⁆ L'
⊢ LieAlgebra.IsNilpotent R L ↔ LieAlgebra.IsNilpotent R L'
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L ≃ₗ⁅R⁆ L'
⊢ LieAlgebra.IsNilpotent R L → LieAlgebra.IsNilpotent R L'
[PROOFSTEP]
intro h
[GOAL]
case mpr
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L ≃ₗ⁅R⁆ L'
⊢ LieAlgebra.IsNilpotent R L' → LieAlgebra.IsNilpotent R L
[PROOFSTEP]
intro h
[GOAL]
case mp
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L ≃ₗ⁅R⁆ L'
h : LieAlgebra.IsNilpotent R L
⊢ LieAlgebra.IsNilpotent R L'
[PROOFSTEP]
exact e.symm.injective.lieAlgebra_isNilpotent
[GOAL]
case mpr
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
e : L ≃ₗ⁅R⁆ L'
h : LieAlgebra.IsNilpotent R L'
⊢ LieAlgebra.IsNilpotent R L
[PROOFSTEP]
exact e.injective.lieAlgebra_isNilpotent
[GOAL]
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
⊢ IsNilpotent R { x // x ∈ LieHom.range (ad R L) } ↔ IsNilpotent R L
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h : IsNilpotent R { x // x ∈ LieHom.range (ad R L) }
⊢ IsNilpotent R L
[PROOFSTEP]
have : (ad R L).ker = center R L := by simp
[GOAL]
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h : IsNilpotent R { x // x ∈ LieHom.range (ad R L) }
⊢ LieHom.ker (ad R L) = center R L
[PROOFSTEP]
simp
[GOAL]
case refine'_1
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h : IsNilpotent R { x // x ∈ LieHom.range (ad R L) }
this : LieHom.ker (ad R L) = center R L
⊢ IsNilpotent R L
[PROOFSTEP]
exact
  LieAlgebra.nilpotent_of_nilpotent_quotient (le_of_eq this)
    ((ad R L).quotKerEquivRange.nilpotent_iff_equiv_nilpotent.mpr h)
[GOAL]
case refine'_2
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
⊢ IsNilpotent R L → IsNilpotent R { x // x ∈ LieHom.range (ad R L) }
[PROOFSTEP]
intro h
[GOAL]
case refine'_2
R : Type u
L : Type v
L' : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : LieAlgebra R L
inst✝¹ : LieRing L'
inst✝ : LieAlgebra R L'
h : IsNilpotent R L
⊢ IsNilpotent R { x // x ∈ LieHom.range (ad R L) }
[PROOFSTEP]
exact (ad R L).isNilpotent_range
[GOAL]
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
⊢ ↑(lcs I M k) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M k)
[PROOFSTEP]
induction' k with k ih
[GOAL]
case zero
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k : ℕ
⊢ ↑(lcs I M Nat.zero) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M Nat.zero)
[PROOFSTEP]
simp
[GOAL]
case succ
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ k : ℕ
ih : ↑(lcs I M k) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M k)
⊢ ↑(lcs I M (Nat.succ k)) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M (Nat.succ k))
[PROOFSTEP]
simp_rw [lowerCentralSeries_succ, lcs_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', ← (I.lcs M k).mem_coeSubmodule,
  ih, LieSubmodule.mem_coeSubmodule, LieSubmodule.mem_top, true_and, (I : LieSubalgebra R L).coe_bracket_of_module]
[GOAL]
case succ
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ k : ℕ
ih : ↑(lcs I M k) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M k)
⊢ Submodule.span R {m | ∃ x, x ∈ I ∧ ∃ n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅x, n⁆ = m} =
    Submodule.span R {m | ∃ x n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅↑x, n⁆ = m}
[PROOFSTEP]
congr
[GOAL]
case succ.e_s
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ k : ℕ
ih : ↑(lcs I M k) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M k)
⊢ {m | ∃ x, x ∈ I ∧ ∃ n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅x, n⁆ = m} =
    {m | ∃ x n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅↑x, n⁆ = m}
[PROOFSTEP]
ext m
[GOAL]
case succ.e_s.h
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ k : ℕ
ih : ↑(lcs I M k) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M k)
m : M
⊢ m ∈ {m | ∃ x, x ∈ I ∧ ∃ n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅x, n⁆ = m} ↔
    m ∈ {m | ∃ x n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅↑x, n⁆ = m}
[PROOFSTEP]
constructor
[GOAL]
case succ.e_s.h.mp
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ k : ℕ
ih : ↑(lcs I M k) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M k)
m : M
⊢ m ∈ {m | ∃ x, x ∈ I ∧ ∃ n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅x, n⁆ = m} →
    m ∈ {m | ∃ x n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅↑x, n⁆ = m}
[PROOFSTEP]
rintro ⟨x, hx, m, hm, rfl⟩
[GOAL]
case succ.e_s.h.mp.intro.intro.intro.intro
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ k : ℕ
ih : ↑(lcs I M k) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M k)
x : L
hx : x ∈ I
m : M
hm : m ∈ lowerCentralSeries R { x // x ∈ ↑I } M k
⊢ ⁅x, m⁆ ∈ {m | ∃ x n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅↑x, n⁆ = m}
[PROOFSTEP]
exact ⟨⟨x, hx⟩, m, hm, rfl⟩
[GOAL]
case succ.e_s.h.mpr
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ k : ℕ
ih : ↑(lcs I M k) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M k)
m : M
⊢ m ∈ {m | ∃ x n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅↑x, n⁆ = m} →
    m ∈ {m | ∃ x, x ∈ I ∧ ∃ n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅x, n⁆ = m}
[PROOFSTEP]
rintro ⟨⟨x, hx⟩, m, hm, rfl⟩
[GOAL]
case succ.e_s.h.mpr.intro.mk.intro.intro
R : Type u_1
L : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
I : LieIdeal R L
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
k✝ k : ℕ
ih : ↑(lcs I M k) = ↑(lowerCentralSeries R { x // x ∈ ↑I } M k)
x : L
hx : x ∈ ↑I
m : M
hm : m ∈ lowerCentralSeries R { x // x ∈ ↑I } M k
⊢ ⁅↑{ val := x, property := hx }, m⁆ ∈ {m | ∃ x, x ∈ I ∧ ∃ n, n ∈ lowerCentralSeries R { x // x ∈ ↑I } M k ∧ ⁅x, n⁆ = m}
[PROOFSTEP]
exact ⟨x, hx, m, hm, rfl⟩
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : IsNilpotent a
⊢ IsNilpotent (↑(LieAlgebra.ad R A) a)
[PROOFSTEP]
rw [LieAlgebra.ad_eq_lmul_left_sub_lmul_right]
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : IsNilpotent a
⊢ IsNilpotent ((LinearMap.mulLeft R - LinearMap.mulRight R) a)
[PROOFSTEP]
have hl : IsNilpotent (LinearMap.mulLeft R a) := by rwa [LinearMap.isNilpotent_mulLeft_iff]
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : IsNilpotent a
⊢ IsNilpotent (LinearMap.mulLeft R a)
[PROOFSTEP]
rwa [LinearMap.isNilpotent_mulLeft_iff]
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : IsNilpotent a
hl : IsNilpotent (LinearMap.mulLeft R a)
⊢ IsNilpotent ((LinearMap.mulLeft R - LinearMap.mulRight R) a)
[PROOFSTEP]
have hr : IsNilpotent (LinearMap.mulRight R a) := by rwa [LinearMap.isNilpotent_mulRight_iff]
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : IsNilpotent a
hl : IsNilpotent (LinearMap.mulLeft R a)
⊢ IsNilpotent (LinearMap.mulRight R a)
[PROOFSTEP]
rwa [LinearMap.isNilpotent_mulRight_iff]
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : IsNilpotent a
hl : IsNilpotent (LinearMap.mulLeft R a)
hr : IsNilpotent (LinearMap.mulRight R a)
⊢ IsNilpotent ((LinearMap.mulLeft R - LinearMap.mulRight R) a)
[PROOFSTEP]
have := @LinearMap.commute_mulLeft_right R A _ _ _ _ _ a a
[GOAL]
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : IsNilpotent a
hl : IsNilpotent (LinearMap.mulLeft R a)
hr : IsNilpotent (LinearMap.mulRight R a)
this : Commute (LinearMap.mulLeft R a) (LinearMap.mulRight R a)
⊢ IsNilpotent ((LinearMap.mulLeft R - LinearMap.mulRight R) a)
[PROOFSTEP]
exact this.isNilpotent_sub hl hr
[GOAL]
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Algebra R A
L : Type v
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
x : { x // x ∈ K }
h : IsNilpotent (↑(LieAlgebra.ad R L) ↑x)
⊢ IsNilpotent (↑(LieAlgebra.ad R { x // x ∈ K }) x)
[PROOFSTEP]
obtain ⟨n, hn⟩ := h
[GOAL]
case intro
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Algebra R A
L : Type v
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
x : { x // x ∈ K }
n : ℕ
hn : ↑(LieAlgebra.ad R L) ↑x ^ n = 0
⊢ IsNilpotent (↑(LieAlgebra.ad R { x // x ∈ K }) x)
[PROOFSTEP]
use n
[GOAL]
case h
R : Type u
A : Type v
inst✝⁴ : CommRing R
inst✝³ : Ring A
inst✝² : Algebra R A
L : Type v
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
K : LieSubalgebra R L
x : { x // x ∈ K }
n : ℕ
hn : ↑(LieAlgebra.ad R L) ↑x ^ n = 0
⊢ ↑(LieAlgebra.ad R { x // x ∈ K }) x ^ n = 0
[PROOFSTEP]
exact LinearMap.submodule_pow_eq_zero_of_pow_eq_zero (K.ad_comp_incl_eq x) hn