The dimension of a Lie submodule

A Lie submodule and its carrier submodule have the same underlying type, so they have the same dimension; the same holds for a Lie subalgebra and the Lie submodule it becomes over itself. This file states those definitional equalities once, as the bridges that dimension counts over Lie submodules pass through: the linear-algebra lemmas about dimensions of direct sums are stated for Submodule, while the Lie-theoretic dimension lemmas are stated for LieSubmodule.

Main results

• Ado.finrank_toSubmodule: a Lie submodule has the dimension of its carrier submodule.
• Ado.finrank_toLieSubmodule: a Lie subalgebra has the dimension of the Lie submodule it determines over itself.
• LieSubmodule.finrank_bot: the trivial Lie submodule has dimension zero.
• LieSubmodule.finrank_eq_zero_of_eq_bot: the hypothesis form of the same fact.

@[simp]

theorem Ado.finrank_toSubmodule {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] (N : LieSubmodule R L M) : Module.finrank R ↥↑N = Module.finrank R ↥N

The type underlying a Lie submodule is the type underlying its carrier submodule, so the two have the same dimension.

@[simp]

theorem Ado.finrank_toLieSubmodule {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (K : LieSubalgebra R L) : Module.finrank R ↥K.toLieSubmodule = Module.finrank R ↥K

The type underlying a Lie subalgebra is the type underlying the Lie submodule it determines over itself, so the two have the same dimension.

@[simp]

theorem LieSubmodule.finrank_bot {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [Nontrivial R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] : Module.finrank R ↥⊥ = 0

The trivial Lie submodule has dimension zero. Ado.finrank_toSubmodule is oriented away from Submodule, so simp cannot reach finrank_bot for submodules from here; this is the LieSubmodule normal form.

theorem LieSubmodule.finrank_eq_zero_of_eq_bot {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [Nontrivial R] [LieRing L] [AddCommGroup M] [Module R M] [LieRingModule L M] {N : LieSubmodule R L M} (h : N = ⊥) : Module.finrank R ↥N = 0

A trivial Lie submodule has dimension zero. Unlike Submodule.finrank_eq_zero, which is an equivalence, this needs no finiteness or rank condition; it is the one-directional form in which a vanishing weight space contributes nothing to a dimension count.