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

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)
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
induction' k with k ih
no goals
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
simp only [Nat.zero_eq, LieModule.lowerCentralSeries_zero, le_top]
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⁆
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)
simp only [LieModule.lowerCentralSeries_succ]
no goals
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⁆
exact le_trans (LieIdeal.map_bracket_le f) (LieSubmodule.mono_lie _ _ _ _ le_top ih)