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

@[simp]

theorem UniversalEnvelopingAlgebra.toEnd_eq {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) : (LieModule.toEnd R L (UniversalEnvelopingAlgebra R L)) x = LinearMap.mulLeft R ((ι R) x)

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_5} (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_5} (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

theorem UniversalEnvelopingAlgebra.mkAlgHom_tprod_lie_of_associative {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {n : ℕ} (f : Fin n → L) (x : L) : ⁅(mkAlgHom R L) ((TensorAlgebra.tprod R L n) f), (ι R) x⁆ = ∑ i : Fin n, (mkAlgHom R L) ((TensorAlgebra.tprod R L n) (Function.update f i ⁅f i, x⁆))

def UniversalEnvelopingAlgebra.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₂] (f : L →ₗ⁅R⁆ L₂) : UniversalEnvelopingAlgebra R L →ₐ[R] UniversalEnvelopingAlgebra R L₂

Equations

• UniversalEnvelopingAlgebra.map R f = (UniversalEnvelopingAlgebra.lift R) ((UniversalEnvelopingAlgebra.ι R).comp f)

@[simp]

theorem UniversalEnvelopingAlgebra.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₂] (f : L →ₗ⁅R⁆ L₂) (x : L) : (map R f) ((ι R) x) = (ι R) (f x)

@[simp]

theorem UniversalEnvelopingAlgebra.map_mkAlgHom {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₂) (x : L) : (map R f) ((mkAlgHom R L) ((TensorAlgebra.ι R) x)) = (mkAlgHom R L₂) ((TensorAlgebra.ι R) (f x))

theorem UniversalEnvelopingAlgebra.comp_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₂] (f : L →ₗ⁅R⁆ L₂) : (map R f).toLieHom.comp (ι R) = (ι R).comp f

@[simp]

theorem UniversalEnvelopingAlgebra.lift_comp_map {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} {A : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] [Ring A] [Algebra R A] (f : L₂ →ₗ⁅R⁆ A) (g : L →ₗ⁅R⁆ L₂) : ((lift R) f).comp (map R g) = (lift R) (f.comp g)

@[simp]

theorem UniversalEnvelopingAlgebra.lift_map {R : Type u_1} {L : Type u_2} {L₂ : Type u_3} {A : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L₂] [LieAlgebra R L₂] [Ring A] [Algebra R A] (f : L₂ →ₗ⁅R⁆ A) (g : L →ₗ⁅R⁆ L₂) (x : UniversalEnvelopingAlgebra R L) : ((lift R) f) ((map R g) x) = ((lift R) (f.comp g)) x