def LieIdeal.lieIdealOf {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (p q : LieIdeal R L) : LieIdeal R ↥q

Equations

• p.lieIdealOf q = LieIdeal.comap q.incl p

@[simp]

theorem LieIdeal.comap_incl {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (p q : LieIdeal R L) : comap q.incl p = p.lieIdealOf q

@[simp]

theorem LieIdeal.mem_lieIdealOf {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {p q : LieIdeal R L} {x : ↥q} : x ∈ p.lieIdealOf q ↔ ↑x ∈ p

def LieIdeal.lieIdealOfEquivOfLe {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {p q : LieIdeal R L} (h : p ≤ q) : ↥(p.lieIdealOf q) ≃ₗ⁅R⁆ ↥p

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LieIdeal.lieIdealOfEquivOfLe_invFun_coe_coe {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {p q : LieIdeal R L} (h : p ≤ q) (x : ↥p) : ↑↑((lieIdealOfEquivOfLe h).invFun x) = ↑x

@[simp]

theorem LieIdeal.lieIdealOfEquivOfLe_toFun_coe {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {p q : LieIdeal R L} (h : p ≤ q) (x : ↥(p.lieIdealOf q)) : ↑((lieIdealOfEquivOfLe h) x) = ↑↑x