The lattice of invariant submodules

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

See also Mathlib/Algebra/Polynomial/Module/AEval.lean.

def Module.End.invtSubmodule {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f : 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 : End R M) {p : Submodule R M} : p ∈ f.invtSubmodule ↔ p ≤ Submodule.comap f p

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

p is f invariant if and only if p.map f ≤ p.

theorem Module.End.mem_invtSubmodule_iff_mapsTo {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f : End R M) {p : Submodule R M} : p ∈ f.invtSubmodule ↔ Set.MapsTo ⇑f ↑p ↑p

p is f invariant if and only if Set.MapsTo f p p.

theorem Set.Mapsto.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} : MapsTo ⇑f ↑p ↑p → p ∈ f.invtSubmodule

Alias of the reverse direction of Module.End.mem_invtSubmodule_iff_mapsTo.

---

p is f invariant if and only if Set.MapsTo f p p.

theorem Module.End.mem_invtSubmodule_iff_forall_mem_of_mem {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f : End R M) {p : Submodule R M} : p ∈ f.invtSubmodule ↔ ∀ x ∈ p, f x ∈ p

theorem Module.End.mem_invtSubmodule_symm_iff_le_map {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {f : M ≃ₗ[R] M} {p : Submodule R M} : p ∈ invtSubmodule ↑f.symm ↔ p ≤ Submodule.map f p

p is f.symm invariant if and only if p ≤ p.map f.

theorem Module.End.invtSubmodule.inf_mem {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {f : End R M} {p 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 : End R M} {p 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 : 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 : 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 : End R M) : BoundedOrder ↥f.invtSubmodule

Equations

• Module.End.invtSubmodule.instBoundedOrderSubtypeSubmoduleMemSublattice f = { top := ⟨⊤, ⋯⟩, le_top := ⋯, bot := ⟨⊥, ⋯⟩, bot_le := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

theorem Module.End.invtSubmodule.mk_eq_bot_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f : 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 : 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 : End R M) {p 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 : End R M) {p 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 : End R M) {p 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 : End R M) {p 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 : End R M) {p 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 : End R M) {p 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 : End R M) {p : Submodule R M} (hp : p ∈ f.invtSubmodule) {q : Submodule R ↥p} (hq : q ∈ invtSubmodule (LinearMap.restrict f hp)) : Submodule.map p.subtype q ∈ f.invtSubmodule

theorem Module.End.invtSubmodule.comp {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (f : End R M) {p : Submodule R M} {g : End R M} (hf : p ∈ f.invtSubmodule) (hg : p ∈ g.invtSubmodule) : p ∈ invtSubmodule (f ∘ₗ g)

@[simp]

theorem LinearEquiv.map_mem_invtSubmodule_conj_iff {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : Module.End R M} {e : M ≃ₗ[R] N} {p : Submodule R M} : Submodule.map e p ∈ (e.conj f).invtSubmodule ↔ p ∈ f.invtSubmodule

theorem LinearEquiv.map_mem_invtSubmodule_iff {R : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : Module.End R N} {e : M ≃ₗ[R] N} {p : Submodule R M} : Submodule.map e p ∈ f.invtSubmodule ↔ p ∈ (e.symm.conj f).invtSubmodule

theorem Module.End.span_orbit_mem_invtSubmodule (R : Type u_1) {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_3} [Monoid G] [DistribMulAction G M] [SMulCommClass G R M] (x : M) (g : G) : Submodule.span R (MulAction.orbit G x) ∈ invtSubmodule (DistribMulAction.toLinearMap R M g)