def LieIdeal.Quotient.mk' {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (s : LieIdeal R L) : L →ₗ⁅R⁆ L ⧸ s

Equations

• LieIdeal.Quotient.mk' s = { toFun := LieSubmodule.Quotient.mk, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

@[simp]

theorem LieIdeal.Quotient.mk'_apply {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (s : LieIdeal R L) (a✝ : L) : (mk' s) a✝ = LieSubmodule.Quotient.mk a✝

@[simp]

theorem LieIdeal.Quotient.surjective_mk' {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (s : LieIdeal R L) : Function.Surjective ⇑(mk' s)

@[simp]

theorem LieIdeal.Quotient.mk'_ker {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (s : LieIdeal R L) : (mk' s).ker = s

instance LieIdeal.Quotient.instIsNilpotentQuotient_ado {R : Type u_3} {L : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing.IsNilpotent L] (s : LieIdeal R L) : LieRing.IsNilpotent (L ⧸ s)

@[simp]

theorem LieSubmodule.Quotient.lie_bracket_mk {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieAlgebra R L] [LieModule R L M] (N : LieSubmodule R L M) (x : L) (m : M) : ⁅x, mk m⁆ = mk ⁅x, m⁆

def LieSubmodule.Quotient.lift {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] [LieRingModule L M] [LieRingModule L M₂] [LieAlgebra R L] [LieModule R L M] (N : LieSubmodule R L M) (f : M →ₗ⁅R,L⁆ M₂) (h : N ≤ f.ker) : M ⧸ N →ₗ⁅R,L⁆ M₂

Equations

• LieSubmodule.Quotient.lift N f h = { toLinearMap := (↑N).liftQ (↑f) h, map_lie' := ⋯ }

@[simp]

theorem LieSubmodule.Quotient.lift_apply {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] [LieRingModule L M] [LieRingModule L M₂] [LieAlgebra R L] [LieModule R L M] (N : LieSubmodule R L M) (f : M →ₗ⁅R,L⁆ M₂) {h : N ≤ f.ker} (x : M) : (lift N f h) (mk x) = f x

@[simp]

theorem LieSubmodule.Quotient.lift_mk' {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] [LieRingModule L M] [LieRingModule L M₂] [LieAlgebra R L] [LieModule R L M] (N : LieSubmodule R L M) (f : M →ₗ⁅R,L⁆ M₂) (h : N ≤ f.ker) : (lift N f h).comp (mk' N) = f

def LieSubmodule.Quotient.map {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] [LieRingModule L M] [LieRingModule L M₂] [LieAlgebra R L] [LieModule R L M] [LieModule R L M₂] (N : LieSubmodule R L M) (N₂ : LieSubmodule R L M₂) (f : M →ₗ⁅R,L⁆ M₂) (h : N ≤ comap f N₂) : M ⧸ N →ₗ⁅R,L⁆ M₂ ⧸ N₂

Equations

• LieSubmodule.Quotient.map N N₂ f h = LieSubmodule.Quotient.lift N ((LieSubmodule.Quotient.mk' N₂).comp f) ⋯

@[simp]

theorem LieSubmodule.Quotient.map_apply {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] [LieRingModule L M] [LieRingModule L M₂] [LieAlgebra R L] [LieModule R L M] [LieModule R L M₂] (N : LieSubmodule R L M) (N₂ : LieSubmodule R L M₂) (f : M →ₗ⁅R,L⁆ M₂) {h : N ≤ comap f N₂} (x : M) : (map N N₂ f h) (mk x) = mk (f x)

@[simp]

theorem LieSubmodule.Quotient.map_mk' {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] [LieRingModule L M] [LieRingModule L M₂] [LieAlgebra R L] [LieModule R L M] [LieModule R L M₂] (N : LieSubmodule R L M) (N₂ : LieSubmodule R L M₂) (f : M →ₗ⁅R,L⁆ M₂) (h : N ≤ comap f N₂) : (map N N₂ f h).comp (mk' N) = (mk' N₂).comp f

def LieSubmodule.Quotient.equiv {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] [LieRingModule L M] [LieRingModule L M₂] [LieAlgebra R L] [LieModule R L M] [LieModule R L M₂] (N : LieSubmodule R L M) (N₂ : LieSubmodule R L M₂) (f : M ≃ₗ⁅R,L⁆ M₂) (h : LieSubmodule.map f.toLieModuleHom N = N₂) : M ⧸ N ≃ₗ⁅R,L⁆ M₂ ⧸ N₂

Equations

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

@[simp]

theorem LieSubmodule.Quotient.equiv_apply {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] [LieRingModule L M] [LieRingModule L M₂] [LieAlgebra R L] [LieModule R L M] [LieModule R L M₂] (N : LieSubmodule R L M) (N₂ : LieSubmodule R L M₂) (f : M ≃ₗ⁅R,L⁆ M₂) (h : LieSubmodule.map f.toLieModuleHom N = N₂) (x : M ⧸ N) : (equiv N N₂ f h) x = (map N N₂ f.toLieModuleHom ⋯) x

@[simp]

theorem LieSubmodule.Quotient.equiv_symm {R : Type u_1} {L : Type u_2} {M : Type u_3} {M₂ : Type u_4} [CommRing R] [LieRing L] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] [LieRingModule L M] [LieRingModule L M₂] [LieAlgebra R L] [LieModule R L M] [LieModule R L M₂] (N : LieSubmodule R L M) (N₂ : LieSubmodule R L M₂) (f : M ≃ₗ⁅R,L⁆ M₂) (h : LieSubmodule.map f.toLieModuleHom N = N₂) : (equiv N N₂ f h).symm = equiv N₂ N f.symm ⋯

instance LieSubmodule.Quotient.instIsNilpotentQuotient_ado {R : Type u_5} {L : Type u_6} {M : Type u_7} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [LieModule.IsNilpotent L M] (s : LieSubmodule R L M) : LieModule.IsNilpotent L (M ⧸ s)