@[instance_reducible]

instance UniversalEnvelopingAlgebra.instLieRingModule_ado {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] : LieRingModule L (UniversalEnvelopingAlgebra R L)

Equations

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

@[simp]

theorem UniversalEnvelopingAlgebra.bracket_eq {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) (a : UniversalEnvelopingAlgebra R L) : ⁅x, a⁆ = (ι R) x * a

instance UniversalEnvelopingAlgebra.instLieModule_ado {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] : LieModule R L (UniversalEnvelopingAlgebra R L)

theorem UniversalEnvelopingAlgebra.ringCon_lie_compat {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (x y : L) : (ringCon R L) ((TensorAlgebra.ι R) ⁅x, y⁆ + (TensorAlgebra.ι R) y * (TensorAlgebra.ι R) x) ((TensorAlgebra.ι R) x * (TensorAlgebra.ι R) y)

theorem UniversalEnvelopingAlgebra.ringCon_induction {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {motive : (x y : TensorAlgebra R L) → (ringCon R L) x y → Prop} (refl : ∀ (a : TensorAlgebra R L), motive a a ⋯) (symm : ∀ (a b : TensorAlgebra R L) (h : (ringCon R L) a b), motive a b h → motive b a ⋯) (trans : ∀ (a b c : TensorAlgebra R L) (h₁ : (ringCon R L) a b) (h₂ : (ringCon R L) b c), motive a b h₁ → motive b c h₂ → motive a c ⋯) (add : ∀ (a b c d : TensorAlgebra R L) (h₁ : (ringCon R L) a b) (h₂ : (ringCon R L) c d), motive a b h₁ → motive c d h₂ → motive (a + c) (b + d) ⋯) (mul : ∀ (a b c d : TensorAlgebra R L) (h₁ : (ringCon R L) a b) (h₂ : (ringCon R L) c d), motive a b h₁ → motive c d h₂ → motive (a * c) (b * d) ⋯) (lie_compat : ∀ (a b : L), motive ((TensorAlgebra.ι R) ⁅a, b⁆ + (TensorAlgebra.ι R) b * (TensorAlgebra.ι R) a) ((TensorAlgebra.ι R) a * (TensorAlgebra.ι R) b) ⋯) {a b : TensorAlgebra R L} (h : (ringCon R L) a b) : motive a b h

def UniversalEnvelopingAlgebra.tensorLift {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {α : Type u_3} (f : TensorAlgebra R L → α) (hf : ∀ (a b : TensorAlgebra R L), (ringCon R L) a b → f a = f b) : UniversalEnvelopingAlgebra R L → α

Equations

• UniversalEnvelopingAlgebra.tensorLift f hf = Quotient.lift f hf

@[simp]

theorem UniversalEnvelopingAlgebra.tensorLift_mkAlgHom {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {α : Type u_3} (f : TensorAlgebra R L → α) (hf : ∀ (a b : TensorAlgebra R L), (ringCon R L) a b → f a = f b) (a : TensorAlgebra R L) : tensorLift f hf ((mkAlgHom R L) a) = f a

theorem UniversalEnvelopingAlgebra.mkAlgHom_eq_mkAlgHom {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {a b : TensorAlgebra R L} : (mkAlgHom R L) a = (mkAlgHom R L) b ↔ (ringCon R L) a b

theorem UniversalEnvelopingAlgebra.mkAlgHom_surjective (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] : Function.Surjective ⇑(mkAlgHom R L)

theorem UniversalEnvelopingAlgebra.ind {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {motive : UniversalEnvelopingAlgebra R L → Prop} (mkAlgHom : ∀ (a : TensorAlgebra R L), motive ((mkAlgHom R L) a)) (a : UniversalEnvelopingAlgebra R L) : motive a