The lattice of invariant submodules

In this file we defined the type Module.End.invtSubmodule, associated to a linear endomorphism of a module. Its utilty stems primarily from those occasions on which we wish to take advantage of the lattice structure of invariant submodules.

See also Module.AEval.

def Module.End.invtSubmodule {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f : Module.End R M) : Sublattice (Submodule R M)

Given an endomorphism, f of some module, this is the sublattice of all f-invariant submodules.

Equations

• f.invtSubmodule = { carrier := {p : Submodule R M | p ≤ Submodule.comap f p}, supClosed' := ⋯, infClosed' := ⋯ }

theorem Module.End.mem_invtSubmodule {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f : Module.End R M) {p : Submodule R M} : p ∈ f.invtSubmodule ↔ p ≤ Submodule.comap f p

theorem Module.End.invtSubmodule.inf_mem {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {f : Module.End R M} {p : Submodule R M} {q : Submodule R M} (hp : p ∈ f.invtSubmodule) (hq : q ∈ f.invtSubmodule) : p ⊓ q ∈ f.invtSubmodule

theorem Module.End.invtSubmodule.sup_mem {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {f : Module.End R M} {p : Submodule R M} {q : Submodule R M} (hp : p ∈ f.invtSubmodule) (hq : q ∈ f.invtSubmodule) : p ⊔ q ∈ f.invtSubmodule

@[simp]

theorem Module.End.invtSubmodule.top_mem {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f : Module.End R M) : ⊤ ∈ f.invtSubmodule

@[simp]

theorem Module.End.invtSubmodule.bot_mem {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f : Module.End R M) : ⊥ ∈ f.invtSubmodule

instance Module.End.invtSubmodule.instBoundedOrderSubtypeSubmoduleMemSublattice {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f : Module.End R M) : BoundedOrder ↥f.invtSubmodule

Equations

• Module.End.invtSubmodule.instBoundedOrderSubtypeSubmoduleMemSublattice f = BoundedOrder.mk

@[simp]

theorem Module.End.invtSubmodule.zero {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] : Module.End.invtSubmodule 0 = ⊤

@[simp]

theorem Module.End.invtSubmodule.id {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] : Module.End.invtSubmodule LinearMap.id = ⊤

theorem Module.End.invtSubmodule.mk_eq_bot_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f : Module.End R M) {p : Submodule R M} (hp : p ∈ f.invtSubmodule) : ⟨p, hp⟩ = ⊥ ↔ p = ⊥

theorem Module.End.invtSubmodule.mk_eq_top_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f : Module.End R M) {p : Submodule R M} (hp : p ∈ f.invtSubmodule) : ⟨p, hp⟩ = ⊤ ↔ p = ⊤

@[simp]

theorem Module.End.invtSubmodule.disjoint_mk_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f : Module.End R M) {p : Submodule R M} {q : Submodule R M} (hp : p ∈ f.invtSubmodule) (hq : q ∈ f.invtSubmodule) : Disjoint ⟨p, hp⟩ ⟨q, hq⟩ ↔ Disjoint p q

theorem Module.End.invtSubmodule.disjoint_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f : Module.End R M) {p : ↥f.invtSubmodule} {q : ↥f.invtSubmodule} : Disjoint p q ↔ Disjoint ↑p ↑q

@[simp]

theorem Module.End.invtSubmodule.codisjoint_mk_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f : Module.End R M) {p : Submodule R M} {q : Submodule R M} (hp : p ∈ f.invtSubmodule) (hq : q ∈ f.invtSubmodule) : Codisjoint ⟨p, hp⟩ ⟨q, hq⟩ ↔ Codisjoint p q

theorem Module.End.invtSubmodule.codisjoint_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f : Module.End R M) {p : ↥f.invtSubmodule} {q : ↥f.invtSubmodule} : Codisjoint p q ↔ Codisjoint ↑p ↑q

@[simp]

theorem Module.End.invtSubmodule.isCompl_mk_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f : Module.End R M) {p : Submodule R M} {q : Submodule R M} (hp : p ∈ f.invtSubmodule) (hq : q ∈ f.invtSubmodule) : IsCompl ⟨p, hp⟩ ⟨q, hq⟩ ↔ IsCompl p q

theorem Module.End.invtSubmodule.isCompl_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f : Module.End R M) {p : ↥f.invtSubmodule} {q : ↥f.invtSubmodule} : IsCompl p q ↔ IsCompl ↑p ↑q

theorem Module.End.invtSubmodule.map_subtype_mem_of_mem_invtSubmodule {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f : Module.End R M) {p : Submodule R M} (hp : p ∈ f.invtSubmodule) {q : Submodule R ↥p} (hq : q ∈ Module.End.invtSubmodule (LinearMap.restrict f hp)) : Submodule.map p.subtype q ∈ f.invtSubmodule