Documentation

Mathlib.Algebra.Module.Submodule.Lattice

The lattice structure on Submodules #

This file defines the lattice structure on submodules, Submodule.CompleteLattice, with ⊥ defined as {0} and ⊓ defined as intersection of the underlying carrier. If p and q are submodules of a module, p ≤ q means that p ⊆ q.

Many results about operations on this lattice structure are defined in LinearAlgebra/Basic.lean, most notably those which use span.

Implementation notes #

This structure should match the AddSubmonoid.CompleteLattice structure, and we should try to unify the APIs where possible.

source
instance Submodule.instBotSubmodule {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
Bot (Submodule R M)

The set {0} is the bottom element of the lattice of submodules.

source
instance Submodule.inhabited' {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
Inhabited (Submodule R M)
source
@[simp]
theorem Submodule.bot_coe {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
↑⊥ = {0}
source
@[simp]
theorem Submodule.bot_toAddSubmonoid {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
⊥.toAddSubmonoid = ⊥
source
@[simp]
theorem Submodule.restrictScalars_bot (R : Type u_1) {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMul S R] [IsScalarTower S R M] :
Submodule.restrictScalars S ⊥ = ⊥
source
@[simp]
theorem Submodule.mem_bot (R : Type u_1) {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} :
x ∈ ⊥ ↔ x = 0
source
@[simp]
theorem Submodule.restrictScalars_eq_bot_iff {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMul S R] [IsScalarTower S R M] {p : Submodule R M} :
Submodule.restrictScalars S p = ⊥ ↔ p = ⊥
source
instance Submodule.uniqueBot {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
Unique { x // x ∈ ⊥ }
source
instance Submodule.instOrderBotSubmoduleToLEToPreorderInstPartialOrderSetLike {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
OrderBot (Submodule R M)
source
theorem Submodule.eq_bot_iff {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) :
p = ⊥ ↔ ∀ (x : M), x ∈ p → x = 0
source
theorem Submodule.bot_ext {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (x : { x // x ∈ ⊥ }) (y : { x // x ∈ ⊥ }) :
x = y
source
theorem Submodule.ne_bot_iff {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) :
p ≠ ⊥ ↔ ∃ x, x ∈ p ∧ x ≠ 0
source
theorem Submodule.nonzero_mem_of_bot_lt {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} (bot_lt : ⊥ < p) :
∃ a, a ≠ 0
source
theorem Submodule.exists_mem_ne_zero_of_ne_bot {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} (h : p ≠ ⊥) :
∃ b, b ∈ p ∧ b ≠ 0
source
@[simp]
theorem Submodule.botEquivPUnit_apply {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
∀ (x : { x // x ∈ ⊥ }), ↑Submodule.botEquivPUnit x = PUnit.unit
source
@[simp]
theorem Submodule.botEquivPUnit_symm_apply {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
∀ (x : PUnit.{v + 1} ), ↑(LinearEquiv.symm Submodule.botEquivPUnit) x = 0
source
def Submodule.botEquivPUnit {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
{ x // x ∈ ⊥ } ≃ₗ[R] PUnit.{v + 1}

The bottom submodule is linearly equivalent to punit as an R-module.

Instances For
    source
    theorem Submodule.eq_bot_of_subsingleton {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) [Subsingleton { x // x ∈ p }] :
    p = ⊥
    source
    instance Submodule.instTopSubmodule {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
    Top (Submodule R M)

    The universal set is the top element of the lattice of submodules.

    source
    @[simp]
    theorem Submodule.top_coe {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
    ↑⊤ = Set.univ
    source
    @[simp]
    theorem Submodule.top_toAddSubmonoid {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
    ⊤.toAddSubmonoid = ⊤
    source
    @[simp]
    theorem Submodule.mem_top {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} :
    x ∈ ⊤
    source
    @[simp]
    theorem Submodule.restrictScalars_top (R : Type u_1) {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMul S R] [IsScalarTower S R M] :
    Submodule.restrictScalars S ⊤ = ⊤
    source
    @[simp]
    theorem Submodule.restrictScalars_eq_top_iff {R : Type u_1} {S : Type u_2} {M : Type u_3} [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMul S R] [IsScalarTower S R M] {p : Submodule R M} :
    Submodule.restrictScalars S p = ⊤ ↔ p = ⊤
    source
    instance Submodule.instOrderTopSubmoduleToLEToPreorderInstPartialOrderSetLike {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
    OrderTop (Submodule R M)
    source
    theorem Submodule.eq_top_iff' {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} :
    p = ⊤ ↔ ∀ (x : M), x ∈ p
    source
    @[simp]
    theorem Submodule.topEquiv_symm_apply_coe {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) :
    ↑(↑(LinearEquiv.symm Submodule.topEquiv) x) = x
    source
    @[simp]
    theorem Submodule.topEquiv_apply {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (x : { x // x ∈ ⊤ }) :
    ↑Submodule.topEquiv x = ↑x
    source
    def Submodule.topEquiv {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
    { x // x ∈ ⊤ } ≃ₗ[R] M

    The top submodule is linearly equivalent to the module.

    This is the module version of AddSubmonoid.topEquiv.

    Instances For
      source
      instance Submodule.instInfSetSubmodule {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
      InfSet (Submodule R M)
      source
      instance Submodule.instInfSubmodule {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
      Inf (Submodule R M)
      source
      instance Submodule.completeLattice {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
      CompleteLattice (Submodule R M)
      source
      @[simp]
      theorem Submodule.inf_coe {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R M} :
      ↑(p ⊓ q) = ↑p ∩ ↑q
      source
      @[simp]
      theorem Submodule.mem_inf {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R M} {x : M} :
      x ∈ p ⊓ q ↔ x ∈ p ∧ x ∈ q
      source
      @[simp]
      theorem Submodule.sInf_coe {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (P : Set (Submodule R M)) :
      ↑(sInf P) = ⋂ (p : Submodule R M) (_ : p ∈ P), ↑p
      source
      @[simp]
      theorem Submodule.finset_inf_coe {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_4} (s : Finset ι) (p : ι → Submodule R M) :
      ↑(Finset.inf s p) = ⋂ (i : ι) (_ : i ∈ s), ↑(p i)
      source
      @[simp]
      theorem Submodule.iInf_coe {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_4} (p : ι → Submodule R M) :
      ↑(⨅ (i : ι), p i) = ⋂ (i : ι), ↑(p i)
      source
      @[simp]
      theorem Submodule.mem_sInf {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Set (Submodule R M)} {x : M} :
      x ∈ sInf S ↔ ∀ (p : Submodule R M), p ∈ S → x ∈ p
      source
      @[simp]
      theorem Submodule.mem_iInf {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_4} (p : ι → Submodule R M) {x : M} :
      x ∈ ⨅ (i : ι), p i ↔ ∀ (i : ι), x ∈ p i
      source
      @[simp]
      theorem Submodule.mem_finset_inf {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_4} {s : Finset ι} {p : ι → Submodule R M} {x : M} :
      x ∈ Finset.inf s p ↔ ∀ (i : ι), i ∈ s → x ∈ p i
      source
      theorem Submodule.mem_sup_left {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Submodule R M} {T : Submodule R M} {x : M} :
      x ∈ S → x ∈ S ⊔ T
      source
      theorem Submodule.mem_sup_right {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Submodule R M} {T : Submodule R M} {x : M} :
      x ∈ T → x ∈ S ⊔ T
      source
      theorem Submodule.add_mem_sup {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Submodule R M} {T : Submodule R M} {s : M} {t : M} (hs : s ∈ S) (ht : t ∈ T) :
      s + t ∈ S ⊔ T
      source
      theorem Submodule.sub_mem_sup {R' : Type u_4} {M' : Type u_5} [Ring R'] [AddCommGroup M'] [Module R' M'] {S : Submodule R' M'} {T : Submodule R' M'} {s : M'} {t : M'} (hs : s ∈ S) (ht : t ∈ T) :
      s - t ∈ S ⊔ T
      source
      theorem Submodule.mem_iSup_of_mem {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_4} {b : M} {p : ι → Submodule R M} (i : ι) (h : b ∈ p i) :
      b ∈ ⨆ (i : ι), p i
      source
      theorem Submodule.sum_mem_iSup {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_4} [Fintype ι] {f : ι → M} {p : ι → Submodule R M} (h : ∀ (i : ι), f i ∈ p i) :
      (Finset.sum Finset.univ fun i => f i) ∈ ⨆ (i : ι), p i
      source
      theorem Submodule.sum_mem_biSup {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_4} {s : Finset ι} {f : ι → M} {p : ι → Submodule R M} (h : ∀ (i : ι), i ∈ s → f i ∈ p i) :
      (Finset.sum s fun i => f i) ∈ ⨆ (i : ι) (_ : i ∈ s), p i

      Note that Submodule.mem_iSup is provided in LinearAlgebra/Span.lean.

      source
      theorem Submodule.mem_sSup_of_mem {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Set (Submodule R M)} {s : Submodule R M} (hs : s ∈ S) {x : M} :
      x ∈ s → x ∈ sSup S
      source
      theorem Submodule.disjoint_def {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {p' : Submodule R M} :
      Disjoint p p' ↔ ∀ (x : M), x ∈ p → x ∈ p' → x = 0
      source
      theorem Submodule.disjoint_def' {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {p' : Submodule R M} :
      Disjoint p p' ↔ ∀ (x : M), x ∈ p → ∀ (y : M), y ∈ p' → x = y → x = 0
      source
      theorem Submodule.eq_zero_of_coe_mem_of_disjoint {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {q : Submodule R M} (hpq : Disjoint p q) {a : { x // x ∈ p }} (ha : ↑a ∈ q) :
      a = 0
      source
      def AddSubmonoid.toNatSubmodule {M : Type u_3} [AddCommMonoid M] :
      AddSubmonoid M ≃o Submodule ℕ M

      An additive submonoid is equivalent to a ℕ-submodule.

      Instances For
        source
        @[simp]
        theorem AddSubmonoid.toNatSubmodule_symm {M : Type u_3} [AddCommMonoid M] :
        ↑(OrderIso.symm AddSubmonoid.toNatSubmodule) = Submodule.toAddSubmonoid
        source
        @[simp]
        theorem AddSubmonoid.coe_toNatSubmodule {M : Type u_3} [AddCommMonoid M] (S : AddSubmonoid M) :
        ↑(↑AddSubmonoid.toNatSubmodule S) = ↑S
        source
        @[simp]
        theorem AddSubmonoid.toNatSubmodule_toAddSubmonoid {M : Type u_3} [AddCommMonoid M] (S : AddSubmonoid M) :
        (↑AddSubmonoid.toNatSubmodule S).toAddSubmonoid = S
        source
        @[simp]
        theorem Submodule.toAddSubmonoid_toNatSubmodule {M : Type u_3} [AddCommMonoid M] (S : Submodule ℕ M) :
        ↑AddSubmonoid.toNatSubmodule S.toAddSubmonoid = S
        source
        def AddSubgroup.toIntSubmodule {M : Type u_3} [AddCommGroup M] :
        AddSubgroup M ≃o Submodule ℤ M

        An additive subgroup is equivalent to a ℤ-submodule.

        Instances For
          source
          @[simp]
          theorem AddSubgroup.toIntSubmodule_symm {M : Type u_3} [AddCommGroup M] :
          ↑(OrderIso.symm AddSubgroup.toIntSubmodule) = Submodule.toAddSubgroup
          source
          @[simp]
          theorem AddSubgroup.coe_toIntSubmodule {M : Type u_3} [AddCommGroup M] (S : AddSubgroup M) :
          ↑(↑AddSubgroup.toIntSubmodule S) = ↑S
          source
          @[simp]
          theorem AddSubgroup.toIntSubmodule_toAddSubgroup {M : Type u_3} [AddCommGroup M] (S : AddSubgroup M) :
          Submodule.toAddSubgroup (↑AddSubgroup.toIntSubmodule S) = S
          source
          @[simp]
          theorem Submodule.toAddSubgroup_toIntSubmodule {M : Type u_3} [AddCommGroup M] (S : Submodule ℤ M) :
          ↑AddSubgroup.toIntSubmodule (Submodule.toAddSubgroup S) = S