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
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
have h' : (⊤ : LieIdeal R L).map f = ⊤ := by
  rw [← f.idealRange_eq_map]
  exact f.idealRange_eq_top_of_surjective h
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

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)
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
induction' k with k ih
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 = ⊤
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 ⊤ = ⊤
rw [← f.idealRange_eq_map]
no goals
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 = ⊤
exact f.idealRange_eq_top_of_surjective h
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
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
simp only [LieModule.lowerCentralSeries_zero]
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'
h : Function.Surjective ↑f
h' : map f ⊤ = ⊤
⊢ map f (lowerCentralSeries R L L Nat.zero) = lowerCentralSeries R L' L' Nat.zero
exact h'
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'
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)
simp only [LieModule.lowerCentralSeries_succ, LieIdeal.map_bracket_eq f h, ih, h']