Ado.ForMathlib.LieQuotient

@[reducible, inline]

abbrev LieIdeal.Quotient.mk {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {s : LieIdeal R L} :

L → L ⧸ s

Equations

LieIdeal.Quotient.mk = LieSubmodule.Quotient.mk

Instances For

source

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' := ⋯ }

Instances For

source

@[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) (x : L) :

(mk' s) x = mk x

source

@[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)

source

@[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

source

@[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

source

@[simp]

theorem LieIdeal.Quotient.map_mk'_eq_bot_le {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I J : LieIdeal R L) :

LieIdeal.map (mk' I) J = ⊥ ↔ J ≤ I

source

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

LieRing.IsNilpotent (L ⧸ s)

source

instance LieIdeal.Quotient.instIsSolvableQuotient_ado {R : Type u_4} {L : Type u_5} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsSolvable L] (s : LieIdeal R L) :

LieAlgebra.IsSolvable (L ⧸ s)

source

@[simp]

theorem LieIdeal.Quotient.coe_map_mk' {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I J : LieIdeal R L) :

↑(LieIdeal.map (mk' I) J) = ⇑(mk' I) '' ↑J

source

def LieIdeal.Quotient.lift {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (I : LieIdeal R L) (f : L →ₗ⁅R⁆ L₂) (h : I ≤ f.ker) :

L ⧸ I →ₗ⁅R⁆ L₂

Equations

LieIdeal.Quotient.lift I f h = { toLinearMap := (↑I).liftQ (↑f) h, map_lie' := ⋯ }

Instances For

source

@[simp]

theorem LieIdeal.Quotient.lift_apply {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (I : LieIdeal R L) (f : L →ₗ⁅R⁆ L₂) {h : I ≤ f.ker} (x : L) :

(lift I f h) (mk x) = f x

source

@[simp]

theorem LieIdeal.Quotient.lift_mk' {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (I : LieIdeal R L) (f : L →ₗ⁅R⁆ L₂) (h : I ≤ f.ker) :

(lift I f h).comp (mk' I) = f

source

def LieIdeal.Quotient.map {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (I : LieIdeal R L) (J : LieIdeal R L₂) (f : L →ₗ⁅R⁆ L₂) (h : I ≤ comap f J) :

L ⧸ I →ₗ⁅R⁆ L₂ ⧸ J

Equations

LieIdeal.Quotient.map I J f h = LieIdeal.Quotient.lift I ((LieIdeal.Quotient.mk' J).comp f) ⋯

Instances For

source

@[simp]

theorem LieIdeal.Quotient.map_apply {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (I : LieIdeal R L) (J : LieIdeal R L₂) (f : L →ₗ⁅R⁆ L₂) {h : I ≤ comap f J} (x : L) :

(map I J f h) (mk x) = mk (f x)

source

@[simp]

theorem LieIdeal.Quotient.map_mk' {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (I : LieIdeal R L) (J : LieIdeal R L₂) (f : L →ₗ⁅R⁆ L₂) {h : I ≤ comap f J} :

(map I J f h).comp (mk' I) = (mk' J).comp f

source

def LieIdeal.Quotient.quotientEquivQuotientAux {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I J : LieIdeal R L) (h : I ≤ J) :

(L ⧸ I) ⧸ LieIdeal.map (mk' I) J →ₗ⁅R⁆ L ⧸ J

Equations

LieIdeal.Quotient.quotientEquivQuotientAux I J h = LieIdeal.Quotient.lift (LieIdeal.map (LieIdeal.Quotient.mk' I) J) (LieIdeal.Quotient.map I J LieHom.id ⋯) ⋯

Instances For

source

@[simp]

theorem LieIdeal.Quotient.quotientEquivQuotientAux_mk_mk {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I J : LieIdeal R L) (h : I ≤ J) (x : L) :

(quotientEquivQuotientAux I J h) (mk (mk x)) = mk x

source

def LieIdeal.Quotient.quotientEquivQuotient {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I J : LieIdeal R L) (h : I ≤ J) :

((L ⧸ I) ⧸ LieIdeal.map (mk' I) J) ≃ₗ⁅R⁆ L ⧸ J

Equations

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

Instances For

source

@[simp]

theorem LieIdeal.Quotient.quotientEquivQuotient_apply_mk_mk {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I J : LieIdeal R L) (h : I ≤ J) (x : L) :

(quotientEquivQuotient I J h) (mk (mk x)) = mk x

source

@[simp]

theorem LieIdeal.Quotient.quotientEquivQuotient_symm_apply_mk {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I J : LieIdeal R L) (h : I ≤ J) (x : L) :

(quotientEquivQuotient I J h).symm (mk x) = mk (mk x)

source

def LieIdeal.Quotient.equiv {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (I : LieIdeal R L) (J : LieIdeal R L₂) (f : L ≃ₗ⁅R⁆ L₂) (h : LieIdeal.map f.toLieHom I = J) :

(L ⧸ I) ≃ₗ⁅R⁆ L₂ ⧸ J

Equations

LieIdeal.Quotient.equiv I J f h = { toLieHom := LieIdeal.Quotient.map I J f.toLieHom ⋯, invFun := ⇑(LieIdeal.Quotient.map J I f.symm.toLieHom ⋯), left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem LieIdeal.Quotient.equiv_apply {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (I : LieIdeal R L) (J : LieIdeal R L₂) (f : L ≃ₗ⁅R⁆ L₂) (h : LieIdeal.map f.toLieHom I = J) (x : L ⧸ I) :

(equiv I J f h) x = (map I J f.toLieHom ⋯) x

source

@[simp]

theorem LieIdeal.Quotient.equiv_symm {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] (I : LieIdeal R L) (J : LieIdeal R L₂) (f : L ≃ₗ⁅R⁆ L₂) (h : LieIdeal.map f.toLieHom I = J) :

(equiv I J f h).symm = equiv J I f.symm ⋯

source

@[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⁆

source

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' := ⋯ }

Instances For

source

@[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

source

@[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

source

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) ⋯

Instances For

source

@[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)

source

@[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

source

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.

Instances For

source

@[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

source

@[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 ⋯

source

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)

source

noncomputable def Module.Basis.sumLieQuot {R : Type u_1} {L : Type u_2} {V : Type u_3} [CommRing R] [LieRing L] [AddCommGroup V] [Module R V] [LieRingModule L V] {W : LieSubmodule R L V} {m : Type u_4} {n : Type u_5} (bW : Basis m R ↥W) (bQ : Basis n R (V ⧸ W)) :

Basis (m ⊕ n) R V

defeq問題回避の為の {name}sumQuotのコピー

Equations

bW.sumLieQuot bQ = bW.sumQuot bQ

Instances For

source

@[simp]

theorem Module.Basis.sumLieQuot_inl {R : Type u_1} {L : Type u_2} {V : Type u_3} [CommRing R] [LieRing L] [AddCommGroup V] [Module R V] [LieRingModule L V] {W : LieSubmodule R L V} {m : Type u_4} {n : Type u_5} (bW : Basis m R ↥W) (bQ : Basis n R (V ⧸ W)) (i : m) :

(bW.sumLieQuot bQ) (Sum.inl i) = ↑(bW i)

source

@[simp]

theorem Module.Basis.sumLieQuot_inr {R : Type u_1} {L : Type u_2} {V : Type u_3} [CommRing R] [LieRing L] [AddCommGroup V] [Module R V] [LieRingModule L V] {W : LieSubmodule R L V} {m : Type u_4} {n : Type u_5} (bW : Basis m R ↥W) (bQ : Basis n R (V ⧸ W)) (j : n) :

LieSubmodule.Quotient.mk ((bW.sumLieQuot bQ) (Sum.inr j)) = bQ j

source

@[simp]

theorem Module.Basis.sumLieQuot_repr_left {R : Type u_1} {L : Type u_2} {V : Type u_3} [CommRing R] [LieRing L] [AddCommGroup V] [Module R V] [LieRingModule L V] {W : LieSubmodule R L V} {m : Type u_4} {n : Type u_5} (bW : Basis m R ↥W) (bQ : Basis n R (V ⧸ W)) (i : m) :

(bW.sumLieQuot bQ).repr ↑(bW i) = Finsupp.single (Sum.inl i) 1

source

theorem Module.Basis.sumLieQuot_repr_inl {R : Type u_1} {L : Type u_2} {V : Type u_3} [CommRing R] [LieRing L] [AddCommGroup V] [Module R V] [LieRingModule L V] {W : LieSubmodule R L V} {m : Type u_4} {n : Type u_5} (bW : Basis m R ↥W) (bQ : Basis n R (V ⧸ W)) (w : ↥W) (i : m) :

((bW.sumLieQuot bQ).repr ↑w) (Sum.inl i) = (bW.repr w) i

source

@[simp]

theorem Module.Basis.sumLieQuot_repr_inl_of_mem {R : Type u_1} {L : Type u_2} {V : Type u_3} [CommRing R] [LieRing L] [AddCommGroup V] [Module R V] [LieRingModule L V] {W : LieSubmodule R L V} {m : Type u_4} {n : Type u_5} (bW : Basis m R ↥W) (bQ : Basis n R (V ⧸ W)) (v : V) (hv : v ∈ W) (i : m) :

((bW.sumLieQuot bQ).repr v) (Sum.inl i) = (bW.repr ⟨v, hv⟩) i

source

@[simp]

theorem Module.Basis.sumLieQuot_repr_inr {R : Type u_1} {L : Type u_2} {V : Type u_3} [CommRing R] [LieRing L] [AddCommGroup V] [Module R V] [LieRingModule L V] {W : LieSubmodule R L V} {m : Type u_4} {n : Type u_5} (bW : Basis m R ↥W) (bQ : Basis n R (V ⧸ W)) [LieAlgebra R L] [LieModule R L V] (v : V) (j : n) :

((bW.sumLieQuot bQ).repr v) (Sum.inr j) = (bQ.repr ((LieSubmodule.Quotient.mk' W) v)) j

source

theorem Module.Basis.sumLieQuot_repr_inr_of_mem {R : Type u_1} {L : Type u_2} {V : Type u_3} [CommRing R] [LieRing L] [AddCommGroup V] [Module R V] [LieRingModule L V] {W : LieSubmodule R L V} {m : Type u_4} {n : Type u_5} (bW : Basis m R ↥W) (bQ : Basis n R (V ⧸ W)) (v : V) (hv : v ∈ W) (j : n) :

((bW.sumLieQuot bQ).repr v) (Sum.inr j) = 0