Lie submodules of a Lie algebra #

In this file we define Lie submodules and Lie ideals, we construct the lattice structure on Lie submodules and we use it to define various important operations, notably the Lie span of a subset of a Lie module.

Main definitions #

LieSubmodule
LieSubmodule.wellFounded_of_noetherian
LieSubmodule.lieSpan
LieSubmodule.map
LieSubmodule.comap
LieIdeal
LieIdeal.map
LieIdeal.comap

Tags #

lie algebra, lie submodule, lie ideal, lattice structure

source

structure LieSubmodule (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] extends Submodule :

Type w

A Lie submodule of a Lie module is a submodule that is closed under the Lie bracket. This is a sufficient condition for the subset itself to form a Lie module.

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

Instances For

source

instance LieSubmodule.instSetLikeLieSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

SetLike (LieSubmodule R L M) M

Equations

LieSubmodule.instSetLikeLieSubmodule = { coe := fun (s : LieSubmodule R L M) => s.carrier, coe_injective' := ⋯ }

source

instance LieSubmodule.instAddSubgroupClassLieSubmoduleToSubNegMonoidToAddGroupInstSetLikeLieSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

AddSubgroupClass (LieSubmodule R L M) M

Equations

⋯ = ⋯

source

instance LieSubmodule.instSmulMemClass {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

SMulMemClass (LieSubmodule R L M) R M

Equations

⋯ = ⋯

source

instance LieSubmodule.instZeroLieSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

Zero (LieSubmodule R L M)

The zero module is a Lie submodule of any Lie module.

Equations

LieSubmodule.instZeroLieSubmodule = { zero := let __src := 0; { toSubmodule := __src, lie_mem := ⋯ } }

source

instance LieSubmodule.instInhabitedLieSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

Inhabited (LieSubmodule R L M)

Equations

LieSubmodule.instInhabitedLieSubmodule = { default := 0 }

source

instance LieSubmodule.coeSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

CoeOut (LieSubmodule R L M) (Submodule R M)

Equations

LieSubmodule.coeSubmodule = { coe := LieSubmodule.toSubmodule }

source

theorem LieSubmodule.coe_toSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) :

↑↑N = ↑N

source

@[simp]

theorem LieSubmodule.mem_carrier {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) {x : M} :

x ∈ N.carrier ↔ x ∈ ↑N

source

theorem LieSubmodule.mem_mk_iff {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (S : Set M) (h₁ : ∀ {a b : M}, a ∈ S → b ∈ S → a + b ∈ S) (h₂ : S 0) (h₃ : ∀ (c : R) {x : M}, x ∈ { toAddSubsemigroup := { carrier := S, add_mem' := h₁ }, zero_mem' := h₂ }.carrier → c • x ∈ { toAddSubsemigroup := { carrier := S, add_mem' := h₁ }, zero_mem' := h₂ }.carrier) (h₄ : ∀ {x : L} {m : M}, m ∈ { toAddSubmonoid := { toAddSubsemigroup := { carrier := S, add_mem' := h₁ }, zero_mem' := h₂ }, smul_mem' := h₃ }.carrier → ⁅x, m⁆ ∈ { toAddSubmonoid := { toAddSubsemigroup := { carrier := S, add_mem' := h₁ }, zero_mem' := h₂ }, smul_mem' := h₃ }.carrier) {x : M} :

x ∈ { toSubmodule := { toAddSubmonoid := { toAddSubsemigroup := { carrier := S, add_mem' := h₁ }, zero_mem' := h₂ }, smul_mem' := h₃ }, lie_mem := h₄ } ↔ x ∈ S

source

@[simp]

theorem LieSubmodule.mem_mk_iff' {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (p : Submodule R M) (h : ∀ {x : L} {m : M}, m ∈ p.carrier → ⁅x, m⁆ ∈ p.carrier) {x : M} :

x ∈ { toSubmodule := p, lie_mem := h } ↔ x ∈ p

source

@[simp]

theorem LieSubmodule.mem_coeSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) {x : M} :

x ∈ ↑N ↔ x ∈ N

source

theorem LieSubmodule.mem_coe {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) {x : M} :

x ∈ ↑N ↔ x ∈ N

source

@[simp]

theorem LieSubmodule.zero_mem {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) :

0 ∈ N

source

theorem LieSubmodule.mk_eq_zero {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) {x : M} (h : x ∈ N) :

{ val := x, property := h } = 0 ↔ x = 0

source

@[simp]

theorem LieSubmodule.coe_toSet_mk {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (S : Set M) (h₁ : ∀ {a b : M}, a ∈ S → b ∈ S → a + b ∈ S) (h₂ : S 0) (h₃ : ∀ (c : R) {x : M}, x ∈ { toAddSubsemigroup := { carrier := S, add_mem' := h₁ }, zero_mem' := h₂ }.carrier → c • x ∈ { toAddSubsemigroup := { carrier := S, add_mem' := h₁ }, zero_mem' := h₂ }.carrier) (h₄ : ∀ {x : L} {m : M}, m ∈ { toAddSubmonoid := { toAddSubsemigroup := { carrier := S, add_mem' := h₁ }, zero_mem' := h₂ }, smul_mem' := h₃ }.carrier → ⁅x, m⁆ ∈ { toAddSubmonoid := { toAddSubsemigroup := { carrier := S, add_mem' := h₁ }, zero_mem' := h₂ }, smul_mem' := h₃ }.carrier) :

↑{ toSubmodule := { toAddSubmonoid := { toAddSubsemigroup := { carrier := S, add_mem' := h₁ }, zero_mem' := h₂ }, smul_mem' := h₃ }, lie_mem := h₄ } = S

source

theorem LieSubmodule.coe_toSubmodule_mk {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (p : Submodule R M) (h : ∀ {x : L} {m : M}, m ∈ p.carrier → ⁅x, m⁆ ∈ p.carrier) :

↑{ toSubmodule := p, lie_mem := h } = p

source

theorem LieSubmodule.coeSubmodule_injective {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

Function.Injective LieSubmodule.toSubmodule

source

theorem LieSubmodule.ext {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) (h : ∀ (m : M), m ∈ N ↔ m ∈ N') :

N = N'

source

@[simp]

theorem LieSubmodule.coe_toSubmodule_eq_iff {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) :

↑N = ↑N' ↔ N = N'

source

def LieSubmodule.copy {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (s : Set M) (hs : s = ↑N) :

LieSubmodule R L M

Copy of a LieSubmodule with a new carrier equal to the old one. Useful to fix definitional equalities.

Equations

LieSubmodule.copy N s hs = { toSubmodule := { toAddSubmonoid := { toAddSubsemigroup := { carrier := s, add_mem' := ⋯ }, zero_mem' := ⋯ }, smul_mem' := ⋯ }, lie_mem := ⋯ }

Instances For

source

@[simp]

theorem LieSubmodule.coe_copy {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (S : LieSubmodule R L M) (s : Set M) (hs : s = ↑S) :

↑(LieSubmodule.copy S s hs) = s

source

theorem LieSubmodule.copy_eq {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (S : LieSubmodule R L M) (s : Set M) (hs : s = ↑S) :

LieSubmodule.copy S s hs = S

source

instance LieSubmodule.instLieRingModuleSubtypeMemSubmoduleToSemiringToCommSemiringToAddCommMonoidInstMembershipSetLikeToSubmoduleAddCommGroupToRing {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) :

LieRingModule L ↥↑N

Equations

LieSubmodule.instLieRingModuleSubtypeMemSubmoduleToSemiringToCommSemiringToAddCommMonoidInstMembershipSetLikeToSubmoduleAddCommGroupToRing N = LieRingModule.mk ⋯ ⋯ ⋯

source

instance LieSubmodule.module' {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) {S : Type u_1} [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] :

Module S ↥↑N

Equations

LieSubmodule.module' N = Submodule.module' ↑N

source

instance LieSubmodule.instModuleSubtypeMemSubmoduleToSemiringToCommSemiringToAddCommMonoidInstMembershipSetLikeToSubmoduleAddCommMonoid {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) :

Module R ↥↑N

Equations

LieSubmodule.instModuleSubtypeMemSubmoduleToSemiringToCommSemiringToAddCommMonoidInstMembershipSetLikeToSubmoduleAddCommMonoid N = Submodule.module ↑N

source

instance LieSubmodule.instIsCentralScalarSubtypeMemSubmoduleToSemiringToCommSemiringToAddCommMonoidInstMembershipSetLikeToSubmoduleSmulToSMulToZeroToNegZeroClassToSubNegZeroMonoidToSubtractionMonoidToDivisionAddCommMonoidToSMulZeroClassToZeroToMonoidWithZeroToSMulWithZeroToMulActionWithZeroMulOppositeInstZeroInstMonoidWithZeroInstSemiring {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) {S : Type u_1} [Semiring S] [SMul S R] [SMul Sᵐᵒᵖ R] [Module S M] [Module Sᵐᵒᵖ M] [IsScalarTower S R M] [IsScalarTower Sᵐᵒᵖ R M] [IsCentralScalar S M] :

IsCentralScalar S ↥↑N

Equations

⋯ = ⋯

source

instance LieSubmodule.instLieModule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (N : LieSubmodule R L M) :

LieModule R L ↥↑N

Equations

⋯ = ⋯

source

@[simp]

theorem LieSubmodule.coe_zero {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) :

↑0 = 0

source

@[simp]

theorem LieSubmodule.coe_add {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (m : ↥N) (m' : ↥N) :

↑(m + m') = ↑m + ↑m'

source

@[simp]

theorem LieSubmodule.coe_neg {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (m : ↥N) :

↑(-m) = -↑m

source

@[simp]

theorem LieSubmodule.coe_sub {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (m : ↥N) (m' : ↥N) :

↑(m - m') = ↑m - ↑m'

source

@[simp]

theorem LieSubmodule.coe_smul {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (t : R) (m : ↥N) :

↑(t • m) = t • ↑m

source

@[simp]

theorem LieSubmodule.coe_bracket {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (x : L) (m : ↥N) :

↑⁅x, m⁆ = ⁅x, ↑m⁆

source

@[inline, reducible]

abbrev LieIdeal (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :

Type v

An ideal of a Lie algebra is a Lie submodule of the Lie algebra as a Lie module over itself.

Equations

LieIdeal R L = LieSubmodule R L L

Instances For

source

theorem lie_mem_right (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (x : L) (y : L) (h : y ∈ I) :

⁅x, y⁆ ∈ I

source

theorem lie_mem_left (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (x : L) (y : L) (h : x ∈ I) :

⁅x, y⁆ ∈ I

source

def lieIdealSubalgebra (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) :

LieSubalgebra R L

An ideal of a Lie algebra is a Lie subalgebra.

Equations

lieIdealSubalgebra R L I = let __src := ↑I; { toSubmodule := __src, lie_mem' := ⋯ }

Instances For

source

instance instCoeLieIdealLieSubalgebra (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] :

Coe (LieIdeal R L) (LieSubalgebra R L)

Equations

instCoeLieIdealLieSubalgebra R L = { coe := lieIdealSubalgebra R L }

source

@[simp]

theorem LieIdeal.coe_toSubalgebra (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) :

↑(lieIdealSubalgebra R L I) = ↑I

source

@[simp]

theorem LieIdeal.coe_to_lieSubalgebra_to_submodule (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) :

(lieIdealSubalgebra R L I).toSubmodule = ↑I

source

instance LieIdeal.lieRing (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) :

LieRing ↥↑I

An ideal of L is a Lie subalgebra of L, so it is a Lie ring.

Equations

LieIdeal.lieRing R L I = LieSubalgebra.lieRing R L (lieIdealSubalgebra R L I)

source

instance LieIdeal.lieAlgebra (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) :

LieAlgebra R ↥↑I

Transfer the LieAlgebra instance from the coercion LieIdeal → LieSubalgebra.

Equations

LieIdeal.lieAlgebra R L I = LieSubalgebra.lieAlgebra R L (lieIdealSubalgebra R L I)

source

instance LieIdeal.lieRingModule (M : Type w) [AddCommGroup M] {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) [LieRingModule L M] :

LieRingModule (↥↑I) M

Transfer the LieRingModule instance from the coercion LieIdeal → LieSubalgebra.

Equations

LieIdeal.lieRingModule M I = LieSubalgebra.lieRingModule (lieIdealSubalgebra R L I)

source

@[simp]

theorem LieIdeal.coe_bracket_of_module (M : Type w) [AddCommGroup M] {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) [LieRingModule L M] (x : ↥I) (m : M) :

⁅x, m⁆ = ⁅↑x, m⁆

source

instance LieIdeal.lieModule (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (I : LieIdeal R L) :

LieModule R (↥↑I) M

Transfer the LieModule instance from the coercion LieIdeal → LieSubalgebra.

Equations

⋯ = ⋯

source

theorem Submodule.exists_lieSubmodule_coe_eq_iff {R : Type u} (L : Type v) {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (p : Submodule R M) :

(∃ (N : LieSubmodule R L M), ↑N = p) ↔ ∀ (x : L), ∀ m ∈ p, ⁅x, m⁆ ∈ p

source

def LieSubalgebra.toLieSubmodule {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) :

LieSubmodule R (↥K) L

Given a Lie subalgebra K ⊆ L, if we view L as a K-module by restriction, it contains a distinguished Lie submodule for the action of K, namely K itself.

Equations

LieSubalgebra.toLieSubmodule K = let __src := K.toSubmodule; { toSubmodule := __src, lie_mem := ⋯ }

Instances For

source

@[simp]

theorem LieSubalgebra.coe_toLieSubmodule {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) :

↑(LieSubalgebra.toLieSubmodule K) = K.toSubmodule

source

@[simp]

theorem LieSubalgebra.mem_toLieSubmodule {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K : LieSubalgebra R L} (x : L) :

x ∈ LieSubalgebra.toLieSubmodule K ↔ x ∈ K

source

theorem LieSubalgebra.exists_lieIdeal_coe_eq_iff {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K : LieSubalgebra R L} :

(∃ (I : LieIdeal R L), lieIdealSubalgebra R L I = K) ↔ ∀ (x y : L), y ∈ K → ⁅x, y⁆ ∈ K

source

theorem LieSubalgebra.exists_nested_lieIdeal_coe_eq_iff {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {K : LieSubalgebra R L} {K' : LieSubalgebra R L} (h : K ≤ K') :

(∃ (I : LieIdeal R ↥K'), lieIdealSubalgebra R (↥K') I = LieSubalgebra.ofLe h) ↔ ∀ (x y : L), x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K

source

theorem LieSubmodule.coe_injective {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

Function.Injective SetLike.coe

source

@[simp]

theorem LieSubmodule.coeSubmodule_le_coeSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) :

↑N ≤ ↑N' ↔ N ≤ N'

source

instance LieSubmodule.instBotLieSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

Bot (LieSubmodule R L M)

Equations

LieSubmodule.instBotLieSubmodule = { bot := 0 }

source

@[simp]

theorem LieSubmodule.bot_coe {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

↑⊥ = {0}

source

@[simp]

theorem LieSubmodule.bot_coeSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

↑⊥ = ⊥

source

@[simp]

theorem LieSubmodule.coeSubmodule_eq_bot_iff {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) :

↑N = ⊥ ↔ N = ⊥

source

@[simp]

theorem LieSubmodule.mem_bot {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (x : M) :

x ∈ ⊥ ↔ x = 0

source

instance LieSubmodule.instTopLieSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

Top (LieSubmodule R L M)

Equations

LieSubmodule.instTopLieSubmodule = { top := let __src := ⊤; { toSubmodule := __src, lie_mem := ⋯ } }

source

@[simp]

theorem LieSubmodule.top_coe {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

↑⊤ = Set.univ

source

@[simp]

theorem LieSubmodule.top_coeSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

↑⊤ = ⊤

source

@[simp]

theorem LieSubmodule.coeSubmodule_eq_top_iff {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) :

↑N = ⊤ ↔ N = ⊤

source

@[simp]

theorem LieSubmodule.mem_top {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (x : M) :

x ∈ ⊤

source

instance LieSubmodule.instInfLieSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

Inf (LieSubmodule R L M)

Equations

LieSubmodule.instInfLieSubmodule = { inf := fun (N N' : LieSubmodule R L M) => let __src := ↑N ⊓ ↑N'; { toSubmodule := __src, lie_mem := ⋯ } }

source

instance LieSubmodule.instInfSetLieSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

InfSet (LieSubmodule R L M)

Equations

LieSubmodule.instInfSetLieSubmodule = { sInf := fun (S : Set (LieSubmodule R L M)) => { toSubmodule := sInf {x : Submodule R M | ∃ s ∈ S, ↑s = x}, lie_mem := ⋯ } }

source

@[simp]

theorem LieSubmodule.inf_coe {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) :

↑(N ⊓ N') = ↑N ∩ ↑N'

source

@[simp]

theorem LieSubmodule.inf_coe_toSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) :

↑(N ⊓ N') = ↑N ⊓ ↑N'

source

@[simp]

theorem LieSubmodule.sInf_coe_toSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (S : Set (LieSubmodule R L M)) :

↑(sInf S) = sInf {x : Submodule R M | ∃ s ∈ S, ↑s = x}

source

theorem LieSubmodule.sInf_coe_toSubmodule' {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (S : Set (LieSubmodule R L M)) :

↑(sInf S) = ⨅ N ∈ S, ↑N

source

@[simp]

theorem LieSubmodule.iInf_coe_toSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {ι : Sort u_1} (p : ι → LieSubmodule R L M) :

↑(⨅ (i : ι), p i) = ⨅ (i : ι), ↑(p i)

source

@[simp]

theorem LieSubmodule.sInf_coe {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (S : Set (LieSubmodule R L M)) :

↑(sInf S) = ⋂ s ∈ S, ↑s

source

@[simp]

theorem LieSubmodule.iInf_coe {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {ι : Sort u_1} (p : ι → LieSubmodule R L M) :

↑(⨅ (i : ι), p i) = ⋂ (i : ι), ↑(p i)

source

@[simp]

theorem LieSubmodule.mem_iInf {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {ι : Sort u_1} (p : ι → LieSubmodule R L M) {x : M} :

x ∈ ⨅ (i : ι), p i ↔ ∀ (i : ι), x ∈ p i

source

instance LieSubmodule.instSupLieSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

Sup (LieSubmodule R L M)

Equations

LieSubmodule.instSupLieSubmodule = { sup := fun (N N' : LieSubmodule R L M) => { toSubmodule := ↑N ⊔ ↑N', lie_mem := ⋯ } }

source

instance LieSubmodule.instSupSetLieSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

SupSet (LieSubmodule R L M)

Equations

LieSubmodule.instSupSetLieSubmodule = { sSup := fun (S : Set (LieSubmodule R L M)) => { toSubmodule := sSup {x : Submodule R M | ∃ p ∈ S, ↑p = x}, lie_mem := ⋯ } }

source

@[simp]

theorem LieSubmodule.sup_coe_toSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) :

↑(N ⊔ N') = ↑N ⊔ ↑N'

source

@[simp]

theorem LieSubmodule.sSup_coe_toSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (S : Set (LieSubmodule R L M)) :

↑(sSup S) = sSup {x : Submodule R M | ∃ s ∈ S, ↑s = x}

source

theorem LieSubmodule.sSup_coe_toSubmodule' {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (S : Set (LieSubmodule R L M)) :

↑(sSup S) = ⨆ N ∈ S, ↑N

source

@[simp]

theorem LieSubmodule.iSup_coe_toSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {ι : Sort u_1} (p : ι → LieSubmodule R L M) :

↑(⨆ (i : ι), p i) = ⨆ (i : ι), ↑(p i)

source

instance LieSubmodule.instCompleteLatticeLieSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

CompleteLattice (LieSubmodule R L M)

The set of Lie submodules of a Lie module form a complete lattice.

Equations

LieSubmodule.instCompleteLatticeLieSubmodule = let __src := Function.Injective.completeLattice LieSubmodule.toSubmodule ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯; CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

source

theorem LieSubmodule.mem_iSup_of_mem {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {ι : Sort u_1} {b : M} {N : ι → LieSubmodule R L M} (i : ι) (h : b ∈ N i) :

b ∈ ⨆ (i : ι), N i

source

theorem LieSubmodule.iSup_induction {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {ι : Sort u_1} (N : ι → LieSubmodule R L M) {C : M → Prop} {x : M} (hx : x ∈ ⨆ (i : ι), N i) (hN : ∀ (i : ι), ∀ y ∈ N i, C y) (h0 : C 0) (hadd : ∀ (y z : M), C y → C z → C (y + z)) :

C x

source

theorem LieSubmodule.iSup_induction' {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {ι : Sort u_1} (N : ι → LieSubmodule R L M) {C : (x : M) → x ∈ ⨆ (i : ι), N i → Prop} (hN : ∀ (i : ι) (x : M) (hx : x ∈ N i), C x ⋯) (h0 : C 0 ⋯) (hadd : ∀ (x y : M) (hx : x ∈ ⨆ (i : ι), N i) (hy : y ∈ ⨆ (i : ι), N i), C x hx → C y hy → C (x + y) ⋯) {x : M} (hx : x ∈ ⨆ (i : ι), N i) :

C x hx

source

theorem LieSubmodule.disjoint_iff_coe_toSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) :

Disjoint N N' ↔ Disjoint ↑N ↑N'

source

theorem LieSubmodule.codisjoint_iff_coe_toSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) :

Codisjoint N N' ↔ Codisjoint ↑N ↑N'

source

theorem LieSubmodule.independent_iff_coe_toSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {ι : Type u_1} {N : ι → LieSubmodule R L M} :

CompleteLattice.Independent N ↔ CompleteLattice.Independent fun (i : ι) => ↑(N i)

source

theorem LieSubmodule.iSup_eq_top_iff_coe_toSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {ι : Sort u_1} {N : ι → LieSubmodule R L M} :

⨆ (i : ι), N i = ⊤ ↔ ⨆ (i : ι), ↑(N i) = ⊤

source

instance LieSubmodule.instAddLieSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

Add (LieSubmodule R L M)

Equations

LieSubmodule.instAddLieSubmodule = { add := Sup.sup }

source

instance LieSubmodule.instZeroLieSubmodule_1 {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

Zero (LieSubmodule R L M)

Equations

LieSubmodule.instZeroLieSubmodule_1 = { zero := ⊥ }

source

instance LieSubmodule.instAddCommMonoidLieSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

AddCommMonoid (LieSubmodule R L M)

Equations

LieSubmodule.instAddCommMonoidLieSubmodule = AddCommMonoid.mk ⋯

source

@[simp]

theorem LieSubmodule.add_eq_sup {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) :

N + N' = N ⊔ N'

source

@[simp]

theorem LieSubmodule.mem_inf {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) (x : M) :

x ∈ N ⊓ N' ↔ x ∈ N ∧ x ∈ N'

source

theorem LieSubmodule.mem_sup {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (N' : LieSubmodule R L M) (x : M) :

x ∈ N ⊔ N' ↔ ∃ y ∈ N, ∃ z ∈ N', y + z = x

source

theorem LieSubmodule.eq_bot_iff {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) :

N = ⊥ ↔ ∀ m ∈ N, m = 0

source

instance LieSubmodule.subsingleton_of_bot {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

Subsingleton (LieSubmodule R L ↥↑⊥)

Equations

⋯ = ⋯

source

instance LieSubmodule.instIsModularLatticeLieSubmoduleToLatticeToConditionallyCompleteLatticeInstCompleteLatticeLieSubmodule {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

IsModularLattice (LieSubmodule R L M)

Equations

⋯ = ⋯

source

@[simp]

theorem LieSubmodule.toSubmodule_orderEmbedding_apply (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (self : LieSubmodule R L M) :

(LieSubmodule.toSubmodule_orderEmbedding R L M) self = ↑self

source

def LieSubmodule.toSubmodule_orderEmbedding (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

LieSubmodule R L M ↪o Submodule R M

The natural functor that forgets the action of L as an order embedding.

Equations

LieSubmodule.toSubmodule_orderEmbedding R L M = { toEmbedding := { toFun := LieSubmodule.toSubmodule, inj' := ⋯ }, map_rel_iff' := ⋯ }

Instances For

source

theorem LieSubmodule.wellFounded_of_noetherian (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [IsNoetherian R M] :

WellFounded fun (x x_1 : LieSubmodule R L M) => x > x_1

source

theorem LieSubmodule.wellFounded_of_isArtinian (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [IsArtinian R M] :

WellFounded fun (x x_1 : LieSubmodule R L M) => x < x_1

source

@[simp]

theorem LieSubmodule.subsingleton_iff (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

Subsingleton (LieSubmodule R L M) ↔ Subsingleton M

source

@[simp]

theorem LieSubmodule.nontrivial_iff (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

Nontrivial (LieSubmodule R L M) ↔ Nontrivial M

source

instance LieSubmodule.instNontrivialLieSubmodule (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [Nontrivial M] :

Nontrivial (LieSubmodule R L M)

Equations

⋯ = ⋯

source

theorem LieSubmodule.nontrivial_iff_ne_bot (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} :

Nontrivial ↥↑N ↔ N ≠ ⊥

source

def LieSubmodule.incl {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) :

↥↑N →ₗ⁅R,L⁆ M

The inclusion of a Lie submodule into its ambient space is a morphism of Lie modules.

Equations

LieSubmodule.incl N = let __src := Submodule.subtype ↑N; { toLinearMap := __src, map_lie' := ⋯ }

Instances For

source

@[simp]

theorem LieSubmodule.incl_coe {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) :

↑(LieSubmodule.incl N) = Submodule.subtype ↑N

source

@[simp]

theorem LieSubmodule.incl_apply {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) (m : ↥N) :

(LieSubmodule.incl N) m = ↑m

source

theorem LieSubmodule.incl_eq_val {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) :

⇑(LieSubmodule.incl N) = Subtype.val

source

theorem LieSubmodule.injective_incl {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) :

Function.Injective ⇑(LieSubmodule.incl N)

source

def LieSubmodule.inclusion {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} {N' : LieSubmodule R L M} (h : N ≤ N') :

↥↑N →ₗ⁅R,L⁆ ↥↑N'

Given two nested Lie submodules N ⊆ N', the inclusion N ↪ N' is a morphism of Lie modules.

Equations

LieSubmodule.inclusion h = let __spread.0 := Submodule.inclusion ⋯; { toLinearMap := __spread.0, map_lie' := ⋯ }

Instances For

source

@[simp]

theorem LieSubmodule.coe_inclusion {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} {N' : LieSubmodule R L M} (h : N ≤ N') (m : ↥N) :

↑((LieSubmodule.inclusion h) m) = ↑m

source

theorem LieSubmodule.inclusion_apply {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} {N' : LieSubmodule R L M} (h : N ≤ N') (m : ↥N) :

(LieSubmodule.inclusion h) m = { val := ↑m, property := ⋯ }

source

theorem LieSubmodule.inclusion_injective {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} {N' : LieSubmodule R L M} (h : N ≤ N') :

Function.Injective ⇑(LieSubmodule.inclusion h)

source

def LieSubmodule.lieSpan (R : Type u) (L : Type v) {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (s : Set M) :

LieSubmodule R L M

The lieSpan of a set s ⊆ M is the smallest Lie submodule of M that contains s.

Equations

LieSubmodule.lieSpan R L s = sInf {N : LieSubmodule R L M | s ⊆ ↑N}

Instances For

source

theorem LieSubmodule.mem_lieSpan {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {s : Set M} {x : M} :

x ∈ LieSubmodule.lieSpan R L s ↔ ∀ (N : LieSubmodule R L M), s ⊆ ↑N → x ∈ N

source

theorem LieSubmodule.subset_lieSpan {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {s : Set M} :

s ⊆ ↑(LieSubmodule.lieSpan R L s)

source

theorem LieSubmodule.submodule_span_le_lieSpan {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {s : Set M} :

Submodule.span R s ≤ ↑(LieSubmodule.lieSpan R L s)

source

@[simp]

theorem LieSubmodule.lieSpan_le {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {s : Set M} {N : LieSubmodule R L M} :

LieSubmodule.lieSpan R L s ≤ N ↔ s ⊆ ↑N

source

theorem LieSubmodule.lieSpan_mono {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {s : Set M} {t : Set M} (h : s ⊆ t) :

LieSubmodule.lieSpan R L s ≤ LieSubmodule.lieSpan R L t

source

theorem LieSubmodule.lieSpan_eq {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) :

LieSubmodule.lieSpan R L ↑N = N

source

theorem LieSubmodule.coe_lieSpan_submodule_eq_iff {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {p : Submodule R M} :

↑(LieSubmodule.lieSpan R L ↑p) = p ↔ ∃ (N : LieSubmodule R L M), ↑N = p

source

def LieSubmodule.gi (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

GaloisInsertion (LieSubmodule.lieSpan R L) SetLike.coe

lieSpan forms a Galois insertion with the coercion from LieSubmodule to Set.

Equations

LieSubmodule.gi R L M = { choice := fun (s : Set M) (x : ↑(LieSubmodule.lieSpan R L s) ≤ s) => LieSubmodule.lieSpan R L s, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }

Instances For

source

@[simp]

theorem LieSubmodule.span_empty (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

LieSubmodule.lieSpan R L ∅ = ⊥

source

@[simp]

theorem LieSubmodule.span_univ (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

LieSubmodule.lieSpan R L Set.univ = ⊤

source

theorem LieSubmodule.lieSpan_eq_bot_iff (R : Type u) (L : Type v) (M : Type w) [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {s : Set M} :

LieSubmodule.lieSpan R L s = ⊥ ↔ ∀ m ∈ s, m = 0

source

theorem LieSubmodule.span_union (R : Type u) (L : Type v) {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (s : Set M) (t : Set M) :

LieSubmodule.lieSpan R L (s ∪ t) = LieSubmodule.lieSpan R L s ⊔ LieSubmodule.lieSpan R L t

source

theorem LieSubmodule.span_iUnion (R : Type u) (L : Type v) {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {ι : Sort u_1} (s : ι → Set M) :

LieSubmodule.lieSpan R L (⋃ (i : ι), s i) = ⨆ (i : ι), LieSubmodule.lieSpan R L (s i)

source

theorem LieSubmodule.isCompactElement_lieSpan_singleton (R : Type u) (L : Type v) {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (m : M) :

CompleteLattice.IsCompactElement (LieSubmodule.lieSpan R L {m})

source

@[simp]

theorem LieSubmodule.sSup_image_lieSpan_singleton (R : Type u) (L : Type v) {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) :

sSup ((fun (x : M) => LieSubmodule.lieSpan R L {x}) '' ↑N) = N

source

instance LieSubmodule.instIsCompactlyGenerated (R : Type u) (L : Type v) {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] :

IsCompactlyGenerated (LieSubmodule R L M)

Equations

⋯ = ⋯

source

def LieSubmodule.map {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] (f : M →ₗ⁅R,L⁆ M') (N : LieSubmodule R L M) :

LieSubmodule R L M'

A morphism of Lie modules f : M → M' pushes forward Lie submodules of M to Lie submodules of M'.

Equations

LieSubmodule.map f N = let __src := Submodule.map ↑f ↑N; { toSubmodule := __src, lie_mem := ⋯ }

Instances For

source

@[simp]

theorem LieSubmodule.coe_map {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] (f : M →ₗ⁅R,L⁆ M') (N : LieSubmodule R L M) :

↑(LieSubmodule.map f N) = ⇑f '' ↑N

source

@[simp]

theorem LieSubmodule.coeSubmodule_map {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] (f : M →ₗ⁅R,L⁆ M') (N : LieSubmodule R L M) :

↑(LieSubmodule.map f N) = Submodule.map ↑f ↑N

source

def LieSubmodule.comap {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] (f : M →ₗ⁅R,L⁆ M') (N' : LieSubmodule R L M') :

LieSubmodule R L M

A morphism of Lie modules f : M → M' pulls back Lie submodules of M' to Lie submodules of M.

Equations

LieSubmodule.comap f N' = let __src := Submodule.comap ↑f ↑N'; { toSubmodule := __src, lie_mem := ⋯ }

Instances For

source

@[simp]

theorem LieSubmodule.coeSubmodule_comap {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] (f : M →ₗ⁅R,L⁆ M') (N' : LieSubmodule R L M') :

↑(LieSubmodule.comap f N') = Submodule.comap ↑f ↑N'

source

theorem LieSubmodule.map_le_iff_le_comap {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N : LieSubmodule R L M} {N' : LieSubmodule R L M'} :

LieSubmodule.map f N ≤ N' ↔ N ≤ LieSubmodule.comap f N'

source

theorem LieSubmodule.gc_map_comap {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] (f : M →ₗ⁅R,L⁆ M') :

GaloisConnection (LieSubmodule.map f) (LieSubmodule.comap f)

source

theorem LieSubmodule.map_inf_le {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N : LieSubmodule R L M} {N₂ : LieSubmodule R L M} :

LieSubmodule.map f (N ⊓ N₂) ≤ LieSubmodule.map f N ⊓ LieSubmodule.map f N₂

source

theorem LieSubmodule.map_inf {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N : LieSubmodule R L M} {N₂ : LieSubmodule R L M} (hf : Function.Injective ⇑f) :

LieSubmodule.map f (N ⊓ N₂) = LieSubmodule.map f N ⊓ LieSubmodule.map f N₂

source

@[simp]

theorem LieSubmodule.map_sup {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N : LieSubmodule R L M} {N₂ : LieSubmodule R L M} :

LieSubmodule.map f (N ⊔ N₂) = LieSubmodule.map f N ⊔ LieSubmodule.map f N₂

source

@[simp]

theorem LieSubmodule.comap_inf {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N' : LieSubmodule R L M'} {N₂' : LieSubmodule R L M'} :

LieSubmodule.comap f (N' ⊓ N₂') = LieSubmodule.comap f N' ⊓ LieSubmodule.comap f N₂'

source

@[simp]

theorem LieSubmodule.map_iSup {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {ι : Sort u_1} (N : ι → LieSubmodule R L M) :

LieSubmodule.map f (⨆ (i : ι), N i) = ⨆ (i : ι), LieSubmodule.map f (N i)

source

@[simp]

theorem LieSubmodule.mem_map {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N : LieSubmodule R L M} (m' : M') :

m' ∈ LieSubmodule.map f N ↔ ∃ m ∈ N, f m = m'

source

theorem LieSubmodule.mem_map_of_mem {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N : LieSubmodule R L M} {m : M} (h : m ∈ N) :

f m ∈ LieSubmodule.map f N

source

@[simp]

theorem LieSubmodule.mem_comap {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N' : LieSubmodule R L M'} {m : M} :

m ∈ LieSubmodule.comap f N' ↔ f m ∈ N'

source

theorem LieSubmodule.comap_incl_eq_top {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} {N₂ : LieSubmodule R L M} :

LieSubmodule.comap (LieSubmodule.incl N) N₂ = ⊤ ↔ N ≤ N₂

source

theorem LieSubmodule.comap_incl_eq_bot {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} {N₂ : LieSubmodule R L M} :

LieSubmodule.comap (LieSubmodule.incl N) N₂ = ⊥ ↔ N ⊓ N₂ = ⊥

source

theorem LieSubmodule.map_mono {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N : LieSubmodule R L M} {N₂ : LieSubmodule R L M} (h : N ≤ N₂) :

LieSubmodule.map f N ≤ LieSubmodule.map f N₂

source

theorem LieSubmodule.map_comp {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N : LieSubmodule R L M} {M'' : Type u_1} [AddCommGroup M''] [Module R M''] [LieRingModule L M''] {g : M' →ₗ⁅R,L⁆ M''} :

LieSubmodule.map (LieModuleHom.comp g f) N = LieSubmodule.map g (LieSubmodule.map f N)

source

@[simp]

theorem LieSubmodule.map_id {R : Type u} {L : Type v} {M : Type w} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} :

LieSubmodule.map LieModuleHom.id N = N

source

@[simp]

theorem LieSubmodule.map_bot {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} :

LieSubmodule.map f ⊥ = ⊥

source

theorem LieSubmodule.map_le_map_iff {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} {N : LieSubmodule R L M} {N₂ : LieSubmodule R L M} (hf : Function.Injective ⇑f) :

LieSubmodule.map f N ≤ LieSubmodule.map f N₂ ↔ N ≤ N₂

source

theorem LieSubmodule.map_injective_of_injective {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} (hf : Function.Injective ⇑f) :

Function.Injective (LieSubmodule.map f)

source

@[simp]

theorem LieSubmodule.mapOrderEmbedding_apply {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} (hf : Function.Injective ⇑f) (N : LieSubmodule R L M) :

(LieSubmodule.mapOrderEmbedding hf) N = LieSubmodule.map f N

source

def LieSubmodule.mapOrderEmbedding {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} (hf : Function.Injective ⇑f) :

LieSubmodule R L M ↪o LieSubmodule R L M'

An injective morphism of Lie modules embeds the lattice of submodules of the domain into that of the target.

Equations

LieSubmodule.mapOrderEmbedding hf = { toEmbedding := { toFun := LieSubmodule.map f, inj' := ⋯ }, map_rel_iff' := ⋯ }

Instances For

source

noncomputable def LieSubmodule.equivMapOfInjective {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] {f : M →ₗ⁅R,L⁆ M'} (N : LieSubmodule R L M) (hf : Function.Injective ⇑f) :

↥↑N ≃ₗ⁅R,L⁆ ↥↑(LieSubmodule.map f N)

For an injective morphism of Lie modules, any Lie submodule is equivalent to its image.

Equations

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

Instances For

source

@[simp]

theorem LieSubmodule.orderIsoMapComap_apply {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] (e : M ≃ₗ⁅R,L⁆ M') (N : LieSubmodule R L M) :

(LieSubmodule.orderIsoMapComap e) N = LieSubmodule.map e.toLieModuleHom N

source

@[simp]

theorem LieSubmodule.orderIsoMapComap_symm_apply {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] (e : M ≃ₗ⁅R,L⁆ M') (N' : LieSubmodule R L M') :

(RelIso.symm (LieSubmodule.orderIsoMapComap e)) N' = LieSubmodule.comap e.toLieModuleHom N'

source

def LieSubmodule.orderIsoMapComap {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] [AddCommGroup M'] [Module R M'] [LieRingModule L M'] (e : M ≃ₗ⁅R,L⁆ M') :

LieSubmodule R L M ≃o LieSubmodule R L M'

An equivalence of Lie modules yields an order-preserving equivalence of their lattices of Lie Submodules.

Equations

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

Instances For

source

@[simp]

theorem LieIdeal.top_coe_lieSubalgebra {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] :

lieIdealSubalgebra R L ⊤ = ⊤

source

def LieIdeal.map {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (I : LieIdeal R L) :

LieIdeal R L'

A morphism of Lie algebras f : L → L' pushes forward Lie ideals of L to Lie ideals of L'.

Note that unlike LieSubmodule.map, we must take the lieSpan of the image. Mathematically this is because although f makes L' into a Lie module over L, in general the L submodules of L' are not the same as the ideals of L'.

Equations

LieIdeal.map f I = LieSubmodule.lieSpan R L' ↑(Submodule.map (↑f) (lieIdealSubalgebra R L I).toSubmodule)

Instances For

source

def LieIdeal.comap {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (J : LieIdeal R L') :

LieIdeal R L

A morphism of Lie algebras f : L → L' pulls back Lie ideals of L' to Lie ideals of L.

Note that f makes L' into a Lie module over L (turning f into a morphism of Lie modules) and so this is a special case of LieSubmodule.comap but we do not exploit this fact.

Equations

LieIdeal.comap f J = let __src := Submodule.comap (↑f) (lieIdealSubalgebra R L' J).toSubmodule; { toSubmodule := __src, lie_mem := ⋯ }

Instances For

source

@[simp]

theorem LieIdeal.map_coeSubmodule {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (I : LieIdeal R L) (h : ↑(LieIdeal.map f I) = ⇑f '' ↑I) :

↑(LieIdeal.map f I) = Submodule.map ↑f ↑I

source

@[simp]

theorem LieIdeal.comap_coeSubmodule {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (J : LieIdeal R L') :

↑(LieIdeal.comap f J) = Submodule.comap ↑f ↑J

source

theorem LieIdeal.map_le {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') (I : LieIdeal R L) (J : LieIdeal R L') :

LieIdeal.map f I ≤ J ↔ ⇑f '' ↑I ⊆ ↑J

source

theorem LieIdeal.mem_map {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} {x : L} (hx : x ∈ I) :

f x ∈ LieIdeal.map f I

source

@[simp]

theorem LieIdeal.mem_comap {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} {J : LieIdeal R L'} {x : L} :

x ∈ LieIdeal.comap f J ↔ f x ∈ J

source

theorem LieIdeal.map_le_iff_le_comap {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} {J : LieIdeal R L'} :

LieIdeal.map f I ≤ J ↔ I ≤ LieIdeal.comap f J

source

theorem LieIdeal.gc_map_comap {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] (f : L →ₗ⁅R⁆ L') :

GaloisConnection (LieIdeal.map f) (LieIdeal.comap f)

source

@[simp]

theorem LieIdeal.map_sup {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} {I₂ : LieIdeal R L} :

LieIdeal.map f (I ⊔ I₂) = LieIdeal.map f I ⊔ LieIdeal.map f I₂

source

theorem LieIdeal.map_comap_le {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} {J : LieIdeal R L'} :

LieIdeal.map f (LieIdeal.comap f J) ≤ J

source

theorem LieIdeal.comap_map_le {R : Type u} {L : Type v} {L' : Type w₂} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} {I : LieIdeal R L} :

I ≤ LieIdeal.comap f (LieIdeal.map f I)

Documentation

Mathlib.Algebra.Lie.Submodule

Lie submodules of a Lie algebra #

Main definitions #

Tags #