Documentation

TauCeti.Algebra.Lie.Submodule.Interval

Submodules of a Lie submodule #

Inclusion identifies the Lie submodules of N with the interval of ambient Lie submodules contained in N. This transports lattice properties, such as complete reducibility, between the two descriptions.

References #

The interval order isomorphism adapts Mathlib's Submodule.MapSubtype.orderIso and Submodule.mapIic from Mathlib.Algebra.Module.Submodule.Range to Lie submodules.

source
def LieSubmodule.mapIic {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) :
LieSubmodule R L ↥N ≃o ↑(Set.Iic N)

Inclusion identifies the submodules of a Lie submodule with the ambient submodules contained in it.

Instances For
    source
    @[simp]
    theorem LieSubmodule.coe_mapIic_apply {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) (P : LieSubmodule R L ↥N) :
    ↑(N.mapIic P) = map N.incl P

    The ambient submodule corresponding to a submodule of N is its image under inclusion.

    source
    theorem LieSubmodule.mapIic_symm_apply {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) (P : ↑(Set.Iic N)) :
    N.mapIic.symm P = comap N.incl ↑P

    The submodule of N corresponding to an ambient submodule is its inverse image.

    This is not a simp lemma: unfolding the inverse prevents simplification by the order isomorphism's round-trip laws.

    source
    theorem LieSubmodule.mem_mapIic_apply {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) {P : LieSubmodule R L ↥N} {x : M} :
    x ∈ ↑(N.mapIic P) ↔ ∃ (h : x ∈ N), ⟨x, h⟩ ∈ P

    An ambient vector belongs to the image exactly when it lifts to the original submodule of N.

    Together with mem_mapIic_symm_apply, this characterizes membership in both directions of mapIic without unfolding its construction. It is available for explicit rewriting; it is not tagged simp because the image-under-inclusion simp lemmas already give this normal form.

    source
    @[simp]
    theorem LieSubmodule.mem_mapIic_symm_apply {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) {P : ↑(Set.Iic N)} {x : ↥N} :
    x ∈ N.mapIic.symm P ↔ ↑x ∈ ↑P

    Membership in the inverse image is ambient membership after inclusion.