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'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
⊢ ⁅LieHom.idealRange f ⊓ J₁, LieHom.idealRange f ⊓ J₂⁆ ≤ 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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
⊢ map f ⁅comap f J₁, comap f J₂⁆ = ⁅LieHom.idealRange f ⊓ J₁, LieHom.idealRange f ⊓ J₂⁆
rw [← map_sup_ker_eq_map, ← comap_bracket_eq h, map_comap_eq h, inf_eq_right]
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'
f : L →ₗ⁅R⁆ L'
I : LieIdeal R L
J J₁ J₂ : LieIdeal R L'
h : LieHom.IsIdealMorphism f
⊢ ⁅LieHom.idealRange f ⊓ J₁, LieHom.idealRange f ⊓ J₂⁆ ≤ LieHom.idealRange f
exact le_trans (LieSubmodule.lie_le_left _ _) inf_le_left