Lie-Rinehart subalgebras

This file defines Lie-Rinehart subalgebras of a Lie-Rinehart algebra and provides basic related definitions and results.

Main definitions/ statements:

• LieRinehartSubalgebra as an A-submodule of L stable under the Lie bracket. (This is also applicable to Lie-Rinehart rings and more generally any A-module with a Lie ring structure).

• A Lie-Rinehart subalgebra of a Lie-Rinehart ring is a Lie-Rinehart ring

• A Lie-Rinehart subalgebra of a Lie-Rinehart algebra is a Lie-Rinehart algebra over the same ring.

structure LieRinehartSubalgebra (A : Type u_1) (L : Type u_2) [CommRing A] [LieRing L] [Module A L] extends Submodule A L : Type u_2

A Lie-Rinehart subalgebra of a Lie-Rinehart algebra (R A L) is an A-submodule of L, which is stable under the Lie bracket. (This can be defined independently of R and most Lie-Rinehart algebra axioms).

• carrier : Set L
• add_mem' {a b : L} : a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• smul_mem' (c : A) {x : L} : x ∈ self.carrier → c • x ∈ self.carrier
• lie_mem' {a b : L} : a ∈ self.carrier → b ∈ self.carrier → ⁅a, b⁆ ∈ self.carrier

@[implicit_reducible]

instance instZeroLieRinehartSubalgebra (A : Type u_1) (L : Type u_2) [CommRing A] [LieRing L] [Module A L] : Zero (LieRinehartSubalgebra A L)

Equations

• instZeroLieRinehartSubalgebra A L = { zero := { toSubmodule := 0, lie_mem' := ⋯ } }

@[implicit_reducible]

instance instInhabitedLieRinehartSubalgebra (A : Type u_1) (L : Type u_2) [CommRing A] [LieRing L] [Module A L] : Inhabited (LieRinehartSubalgebra A L)

Equations

• instInhabitedLieRinehartSubalgebra A L = { default := 0 }

@[implicit_reducible]

instance LieRinehartSubalgebra.instSetLike (A : Type u_1) (L : Type u_2) [CommRing A] [LieRing L] [Module A L] : SetLike (LieRinehartSubalgebra A L) L

Equations

• LieRinehartSubalgebra.instSetLike A L = { coe := fun (L' : LieRinehartSubalgebra A L) => L'.carrier, coe_injective := ⋯ }

@[implicit_reducible]

instance LieRinehartSubalgebra.instPartialOrder (A : Type u_1) (L : Type u_2) [CommRing A] [LieRing L] [Module A L] : PartialOrder (LieRinehartSubalgebra A L)

Equations

• LieRinehartSubalgebra.instPartialOrder A L = PartialOrder.ofSetLike (LieRinehartSubalgebra A L) L

instance LieRinehartSubalgebra.instAddSubgroupClass (A : Type u_1) (L : Type u_2) [CommRing A] [LieRing L] [Module A L] : AddSubgroupClass (LieRinehartSubalgebra A L) L

instance LieRinehartSubalgebra.instSMulMemClass (A : Type u_1) (L : Type u_2) [CommRing A] [LieRing L] [Module A L] : SMulMemClass (LieRinehartSubalgebra A L) A L

@[implicit_reducible]

instance LieRinehartSubalgebra.lieRing (A : Type u_1) (L : Type u_2) [CommRing A] [LieRing L] [Module A L] (L' : LieRinehartSubalgebra A L) : LieRing ↥L'

A Lie-Rinehart subalgebra forms a Lie ring.

Equations

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

theorem LieRinehartSubalgebra.zero_mem {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (L' : LieRinehartSubalgebra A L) : 0 ∈ L'

theorem LieRinehartSubalgebra.add_mem {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (L' : LieRinehartSubalgebra A L) {x y : L} : x ∈ L' → y ∈ L' → x + y ∈ L'

theorem LieRinehartSubalgebra.sub_mem {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (L' : LieRinehartSubalgebra A L) {x y : L} : x ∈ L' → y ∈ L' → x - y ∈ L'

theorem LieRinehartSubalgebra.smul_mem {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (L' : LieRinehartSubalgebra A L) (t : A) {x : L} (h : x ∈ L') : t • x ∈ L'

theorem LieRinehartSubalgebra.lie_mem {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (L' : LieRinehartSubalgebra A L) {x y : L} (hx : x ∈ L') (hy : y ∈ L') : ⁅x, y⁆ ∈ L'

theorem LieRinehartSubalgebra.mem_carrier {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (L' : LieRinehartSubalgebra A L) {x : L} : x ∈ L'.carrier ↔ x ∈ ↑L'

theorem LieRinehartSubalgebra.mem_mk_iff {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (S : Set L) (h₁ : ∀ {a b : L}, a ∈ S → b ∈ S → a + b ∈ S) (h₂ : S 0) (h₃ : ∀ (c : A) {x : L}, x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier → c • x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier) (h₄ : ∀ {a b : L}, a ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier → b ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier → ⁅a, b⁆ ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier) {x : L} : x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃, lie_mem' := h₄ } ↔ x ∈ S

@[simp]

theorem LieRinehartSubalgebra.mem_toSubmodule {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (L' : LieRinehartSubalgebra A L) {x : L} : x ∈ L'.toSubmodule ↔ x ∈ L'

@[simp]

theorem LieRinehartSubalgebra.mem_mk_iff' {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (p : Submodule A L) (h : ∀ {a b : L}, a ∈ p.carrier → b ∈ p.carrier → ⁅a, b⁆ ∈ p.carrier) {x : L} : x ∈ { toSubmodule := p, lie_mem' := h } ↔ x ∈ p

theorem LieRinehartSubalgebra.mem_coe {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (L' : LieRinehartSubalgebra A L) {x : L} : x ∈ ↑L' ↔ x ∈ L'

@[simp]

theorem LieRinehartSubalgebra.coe_bracket {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (L' : LieRinehartSubalgebra A L) (x y : ↥L') : ↑⁅x, y⁆ = ⁅↑x, ↑y⁆

theorem LieRinehartSubalgebra.ext_iff {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (L' : LieRinehartSubalgebra A L) (x y : ↥L') : x = y ↔ ↑x = ↑y

theorem LieRinehartSubalgebra.coe_zero_iff_zero {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (L' : LieRinehartSubalgebra A L) (x : ↥L') : ↑x = 0 ↔ x = 0

theorem LieRinehartSubalgebra.ext {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (L₁' L₂' : LieRinehartSubalgebra A L) (h : ∀ (x : L), x ∈ L₁' ↔ x ∈ L₂') : L₁' = L₂'

theorem LieRinehartSubalgebra.ext_iff' {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (L₁' L₂' : LieRinehartSubalgebra A L) : L₁' = L₂' ↔ ∀ (x : L), x ∈ L₁' ↔ x ∈ L₂'

@[simp]

theorem LieRinehartSubalgebra.mk_coe {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (S : Set L) (h₁ : ∀ {a b : L}, a ∈ S → b ∈ S → a + b ∈ S) (h₂ : S 0) (h₃ : ∀ (c : A) {x : L}, x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier → c • x ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂ }.carrier) (h₄ : ∀ {a b : L}, a ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier → b ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier → ⁅a, b⁆ ∈ { carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃ }.carrier) : ↑{ carrier := S, add_mem' := h₁, zero_mem' := h₂, smul_mem' := h₃, lie_mem' := h₄ } = S

theorem LieRinehartSubalgebra.toSubmodule_mk {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (p : Submodule A L) (h : ∀ {a b : L}, a ∈ p.carrier → b ∈ p.carrier → ⁅a, b⁆ ∈ p.carrier) : { toSubmodule := p, lie_mem' := h }.toSubmodule = p

theorem LieRinehartSubalgebra.coe_injective {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] : Function.Injective SetLike.coe

theorem LieRinehartSubalgebra.coe_set_eq {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (L₁' L₂' : LieRinehartSubalgebra A L) : ↑L₁' = ↑L₂' ↔ L₁' = L₂'

theorem LieRinehartSubalgebra.toSubmodule_injective {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] : Function.Injective toSubmodule

theorem LieRinehartSubalgebra.coe_toSubmodule {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (L' : LieRinehartSubalgebra A L) : ↑L'.toSubmodule = ↑L'

@[implicit_reducible]

instance LieRinehartSubalgebra.instBracketSubtypeMem {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (L' : LieRinehartSubalgebra A L) {M : Type u_3} [AddCommGroup M] [LieRingModule L M] : Bracket (↥L') M

Equations

• L'.instBracketSubtypeMem = { bracket := fun (x : ↥L') (m : M) => ⁅↑x, m⁆ }

@[simp]

theorem LieRinehartSubalgebra.coe_bracket_of_module {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (L' : LieRinehartSubalgebra A L) {M : Type u_3} [AddCommGroup M] [LieRingModule L M] (x : ↥L') (m : M) : ⁅x, m⁆ = ⁅↑x, m⁆

instance LieRinehartSubalgebra.instIsLieTowerSubtypeMem {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (L' : LieRinehartSubalgebra A L) {M : Type u_3} [AddCommGroup M] [LieRingModule L M] : IsLieTower (↥L') L M

@[implicit_reducible]

instance LieRinehartSubalgebra.lieRingModule {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (L' : LieRinehartSubalgebra A L) {M : Type u_3} [AddCommGroup M] [LieRingModule L M] : LieRingModule (↥L') M

Given a Lie-Rinehart algebra L containing a LieRinehart subalgebra L' ⊆ L, together with a Lie ring module M of L, we may regard M as a Lie ring module of L' by restriction.

Equations

• L'.lieRingModule = { toBracket := L'.instBracketSubtypeMem, add_lie := ⋯, lie_add := ⋯, leibniz_lie := ⋯ }

instance LieRinehartSubalgebra.instLieRinehartRingSubtypeMem {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (L' : LieRinehartSubalgebra A L) [LieRingModule L A] [LieRinehartRing A L] : LieRinehartRing A ↥L'

A Lie-Rinehart subalgebra of a Lie-Rinehart ring forms a new Lie-Rinehart ring.

@[implicit_reducible]

instance LieRinehartSubalgebra.lieAlgebra {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (L' : LieRinehartSubalgebra A L) [LieRingModule L A] [LieRinehartRing A L] (R : Type u_3) [CommRing R] [Algebra R A] [LieAlgebra R L] [LieRinehartAlgebra R A L] : LieAlgebra R ↥L'

A Lie-Rinehart subalgebra of a Lie-Rinehart algebra forms a Lie algebra.

Equations

• L'.lieAlgebra R = { toModule := SubmoduleClass.module' L', lie_smul := ⋯ }

def LieRinehartSubalgebra.toLieSubalgebra {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (L' : LieRinehartSubalgebra A L) [LieRingModule L A] [LieRinehartRing A L] (R : Type u_3) [CommRing R] [Algebra R A] [LieAlgebra R L] [LieRinehartAlgebra R A L] : LieSubalgebra R L

Converts a Lie-Rinehart subalgebra to the corresponding Lie subalgebra.

Equations

• L'.toLieSubalgebra R = { toSubmodule := Submodule.restrictScalars R L'.toSubmodule, lie_mem' := ⋯ }

theorem LieRinehartSubalgebra.toLieSubalgebra_injective {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] [LieRingModule L A] [LieRinehartRing A L] (R : Type u_3) [CommRing R] [Algebra R A] [LieAlgebra R L] [LieRinehartAlgebra R A L] : Function.Injective fun (L' : LieRinehartSubalgebra A L) => L'.toLieSubalgebra R

@[simp]

theorem LieRinehartSubalgebra.toLieSubalgebra_inj {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] [LieRingModule L A] [LieRinehartRing A L] (R : Type u_3) [CommRing R] [Algebra R A] [LieAlgebra R L] [LieRinehartAlgebra R A L] (L₁' L₂' : LieRinehartSubalgebra A L) : L₁'.toLieSubalgebra R = L₂'.toLieSubalgebra R ↔ L₁' = L₂'

theorem LieRinehartSubalgebra.coe_toLieSubalgebra {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (L' : LieRinehartSubalgebra A L) [LieRingModule L A] [LieRinehartRing A L] (R : Type u_3) [CommRing R] [Algebra R A] [LieAlgebra R L] [LieRinehartAlgebra R A L] : ↑(L'.toLieSubalgebra R) = ↑L'

instance LieRinehartSubalgebra.lieModule {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (L' : LieRinehartSubalgebra A L) [LieRingModule L A] [LieRinehartRing A L] (R : Type u_3) [CommRing R] [Algebra R A] [LieAlgebra R L] [LieRinehartAlgebra R A L] {M : Type u_4} [AddCommGroup M] [LieRingModule L M] [Module R M] [LieModule R L M] : LieModule R (↥L') M

Given a Lie-Rinehart algebra L containing a LieRinehart subalgebra L' ⊆ L, together with a Lie module M of L, we may regard M as a Lie module of L' by restriction.

instance LieRinehartSubalgebra.instLieRinehartAlgebraSubtypeMem {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (L' : LieRinehartSubalgebra A L) [LieRingModule L A] [LieRinehartRing A L] (R : Type u_3) [CommRing R] [Algebra R A] [LieAlgebra R L] [LieRinehartAlgebra R A L] : LieRinehartAlgebra R A ↥L'

A Lie-Rinehart subalgebra forms a new Lie-Rinehart algebra.

def LieRinehartSubalgebra.incl {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (L' : LieRinehartSubalgebra A L) [LieRingModule L A] [LieRinehartRing A L] (R : Type u_3) [CommRing R] [Algebra R A] [LieAlgebra R L] [LieRinehartAlgebra R A L] : LieRinehartAlgebra.Hom (AlgHom.id R A) (↥L') L

The embedding of a Lie-Rinehart subalgebra into the ambient space as a morphism of Lie-Rinehart algebras.

Equations

• L'.incl R = { toLinearMap := ↑R L'.subtype, map_lie' := ⋯, map_smul_apply' := ⋯, apply_lie' := ⋯ }

@[simp]

theorem LieRinehartSubalgebra.coe_incl {A : Type u_1} {L : Type u_2} [CommRing A] [LieRing L] [Module A L] (L' : LieRinehartSubalgebra A L) [LieRingModule L A] [LieRinehartRing A L] (R : Type u_3) [CommRing R] [Algebra R A] [LieAlgebra R L] [LieRinehartAlgebra R A L] : ⇑(L'.incl R).toLieHom = Subtype.val