def LieHom.lieIdealComap {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (q : LieIdeal R L₂) : ↥(LieIdeal.comap f q) →ₗ⁅R⁆ ↥q

Equations

• f.lieIdealComap q = { toLinearMap := (↑f).submoduleComap (LieIdeal.toLieSubalgebra R L₂ q).toSubmodule, map_lie' := ⋯ }

@[simp]

theorem LieHom.lieIdealComap_apply_coe {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (q : LieIdeal R L₂) (x : ↥(LieIdeal.comap f q)) : ↑((f.lieIdealComap q) x) = f ↑x

@[simp]

theorem LieHom.lieIdealComap_surjective_of_surjective {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (q : LieIdeal R L₂) (hf : Function.Surjective ⇑f) : Function.Surjective ⇑(f.lieIdealComap q)

@[simp]

theorem LieHom.lieIdealComap_ker {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (q : LieIdeal R L₂) : (f.lieIdealComap q).ker = f.ker.lieIdealOf (LieIdeal.comap f q)