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
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)
intro l k
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

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
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
induction' k with k ih generalizing l <;> intro h
no goals
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
exact (le_zero_iff.mp h).symm ▸ le_rfl
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

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
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
rcases Nat.of_le_succ h with (hk | hk)
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
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
rw [lowerCentralSeries_succ]
no goals
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
exact (LieSubmodule.mono_lie_right _ _ ⊤ (ih hk)).trans (LieSubmodule.lie_le_right _ _)
no goals
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
exact hk.symm ▸ le_rfl