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.

Implementation notes #

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

Bottom element of a submodule #

source
šŸ”ø coverage
@[implicit_reducible]
instance Submodule.instBot {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
šŸ”ø coverage
@[implicit_reducible]
instance Submodule.inhabited' {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
Inhabited (Submodule R M)
source
šŸ“ coverage
@[simp]
theorem Submodule.bot_coe {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
ā†‘āŠ„ = {0}
source
šŸ“ coverage
@[simp]
theorem Submodule.bot_toAddSubmonoid {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
āŠ„.toAddSubmonoid = āŠ„
source
šŸ“ coverage
@[simp]
theorem Submodule.bot_toAddSubgroup {R : Type u_4} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] :
āŠ„.toAddSubgroup = āŠ„
source
šŸ“ coverage
@[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
šŸ“ coverage
@[simp]
theorem Submodule.mk_eq_bot {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (carrier : AddSubmonoid M) (smul_mem' : āˆ€ (c : R) {x : M}, x āˆˆ carrier.carrier ā†’ c ā€¢ x āˆˆ carrier.carrier) :
{ toAddSubmonoid := carrier, smul_mem' := smul_mem' } = āŠ„ ā†” carrier = āŠ„
source
šŸ”ø coverage
@[implicit_reducible]
instance Submodule.uniqueBot {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
Unique ā†„āŠ„
source
šŸ”ø coverage
@[implicit_reducible]
instance Submodule.instOrderBot {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
OrderBot (Submodule R M)
source
šŸ“ coverage
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 āˆˆ p, x = 0
source
theorem Submodule.bot_ext {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (x y : ā†„āŠ„) :
x = y
source
theorem Submodule.bot_ext_iff {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {x y : ā†„āŠ„} :
x = y ā†” True
source
šŸ“ coverage
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 āˆˆ p, x ā‰  0
source
šŸ“ coverage
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 : ā†„p), a ā‰  0
source
šŸ“ coverage
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 āˆˆ p, b ā‰  0
source
šŸ”ø coverage
def Submodule.botEquivPUnit {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
ā†„āŠ„ ā‰ƒā‚—[R] PUnit.{v + 1}

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

Instances For
    source
    šŸ“ coverage
    @[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}) :
    botEquivPUnit.symm xāœ = 0
    source
    šŸ“ coverage
    @[simp]
    theorem Submodule.botEquivPUnit_apply {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (xāœ : ā†„āŠ„) :
    botEquivPUnit xāœ = PUnit.unit
    source
    šŸ“ coverage
    theorem Submodule.subsingleton_iff_eq_bot {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} :
    Subsingleton ā†„p ā†” p = āŠ„
    source
    šŸ“ coverage
    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 ā†„p] :
    p = āŠ„
    source
    šŸ“ coverage
    theorem Submodule.nontrivial_iff_ne_bot {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} :
    Nontrivial ā†„p ā†” p ā‰  āŠ„

    Top element of a submodule #

    source
    šŸ”ø coverage
    @[implicit_reducible]
    instance Submodule.instTop {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
    šŸ“ coverage
    @[simp]
    theorem Submodule.top_coe {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
    ā†‘āŠ¤ = Set.univ
    source
    šŸ“ coverage
    @[simp]
    theorem Submodule.coe_eq_univ {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} :
    ā†‘p = Set.univ ā†” p = āŠ¤
    source
    šŸ“ coverage
    @[simp]
    theorem Submodule.mem_top {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} :
    x āˆˆ āŠ¤
    source
    šŸ“ coverage
    @[simp]
    theorem Submodule.top_toAddSubmonoid {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
    āŠ¤.toAddSubmonoid = āŠ¤
    source
    šŸ“ coverage
    @[simp]
    theorem Submodule.top_toAddSubgroup {R : Type u_4} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] :
    āŠ¤.toAddSubgroup = āŠ¤
    source
    šŸ“ coverage
    @[simp]
    theorem Submodule.toAddSubgroup_eq_top {R : Type u_4} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] {p : Submodule R M} :
    p.toAddSubgroup = āŠ¤ ā†” p = āŠ¤
    source
    šŸ“ coverage
    @[simp]
    theorem Submodule.mk_eq_top {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (carrier : AddSubmonoid M) (smul_mem' : āˆ€ (c : R) {x : M}, x āˆˆ carrier.carrier ā†’ c ā€¢ x āˆˆ carrier.carrier) :
    { toAddSubmonoid := carrier, smul_mem' := smul_mem' } = āŠ¤ ā†” carrier = āŠ¤
    source
    šŸ”ø coverage
    @[implicit_reducible]
    instance Submodule.instOrderTop {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
    OrderTop (Submodule R M)
    source
    šŸ“ coverage
    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
    šŸ”ø coverage
    def Submodule.topEquiv {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
    ā†„āŠ¤ ā‰ƒā‚—[R] M

    The top submodule is linearly equivalent to the module.

    This is the module version of AddSubmonoid.topEquiv.

    Instances For
      source
      šŸ“ coverage
      @[simp]
      theorem Submodule.topEquiv_apply {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (x : ā†„āŠ¤) :
      topEquiv x = ā†‘x
      source
      šŸ“ coverage
      @[simp]
      theorem Submodule.topEquiv_symm_apply_coe {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) :
      ā†‘(topEquiv.symm x) = x

      Infima & suprema in a submodule #

      source
      šŸ”ø coverage
      @[implicit_reducible]
      instance Submodule.instInfSet {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
      InfSet (Submodule R M)
      source
      šŸ“ coverage
      theorem Submodule.isGLB_sInf {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S : Set (Submodule R M)} :
      IsGLB S (sInf S)
      source
      šŸ”ø coverage
      @[implicit_reducible]
      instance Submodule.instMin {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
      Min (Submodule R M)
      source
      šŸ”ø coverage
      @[implicit_reducible]
      instance Submodule.completeLattice {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
      CompleteLattice (Submodule R M)
      source
      šŸ“ coverage
      @[simp]
      theorem Submodule.coe_inf {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p q : Submodule R M} :
      ā†‘(p āŠ“ q) = ā†‘p āˆ© ā†‘q
      source
      šŸ“ coverage
      @[simp]
      theorem Submodule.mem_inf {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p q : Submodule R M} {x : M} :
      x āˆˆ p āŠ“ q ā†” x āˆˆ p āˆ§ x āˆˆ q
      source
      šŸ“ coverage
      @[simp]
      theorem Submodule.coe_sInf {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (P : Set (Submodule R M)) :
      ā†‘(sInf P) = ā‹‚ p āˆˆ P, ā†‘p
      source
      šŸ“ coverage
      @[simp]
      theorem Submodule.coe_finsetInf {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {Ī¹ : Type u_4} (s : Finset Ī¹) (p : Ī¹ ā†’ Submodule R M) :
      ā†‘(s.inf p) = ā‹‚ i āˆˆ s, ā†‘(p i)
      source
      šŸ“ coverage
      @[simp]
      theorem Submodule.coe_iInf {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
      šŸ“ coverage
      @[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 āˆˆ S, x āˆˆ p
      source
      šŸ“ coverage
      @[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
      šŸ“ coverage
      @[simp]
      theorem Submodule.mem_finsetInf {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 āˆˆ s.inf p ā†” āˆ€ i āˆˆ s, x āˆˆ p i
      source
      šŸ“ coverage
      theorem Submodule.inf_iInf {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {Ī¹ : Sort u_4} [Nonempty Ī¹] {p : Ī¹ ā†’ Submodule R M} (q : Submodule R M) :
      q āŠ“ ā؅ (i : Ī¹), p i = ā؅ (i : Ī¹), q āŠ“ p i
      source
      šŸ“ coverage
      theorem Submodule.mem_sup_left {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S T : Submodule R M} {x : M} :
      x āˆˆ S ā†’ x āˆˆ S āŠ” T
      source
      šŸ“ coverage
      theorem Submodule.mem_sup_right {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S T : Submodule R M} {x : M} :
      x āˆˆ T ā†’ x āˆˆ S āŠ” T
      source
      šŸ“ coverage
      theorem Submodule.add_mem_sup {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {S T : Submodule R M} {s t : M} (hs : s āˆˆ S) (ht : t āˆˆ T) :
      s + t āˆˆ S āŠ” T
      source
      šŸ“ coverage
      theorem Submodule.sub_mem_sup {R' : Type u_4} {M' : Type u_5} [Ring R'] [AddCommGroup M'] [Module R' M'] {S T : Submodule R' M'} {s t : M'} (hs : s āˆˆ S) (ht : t āˆˆ T) :
      s - t āˆˆ S āŠ” T
      source
      šŸ“ coverage
      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
      šŸ“ coverage
      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) :
      āˆ‘ i : Ī¹, f i āˆˆ ā؆ (i : Ī¹), p i
      source
      šŸ“ coverage
      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 āˆˆ s, f i āˆˆ p i) :
      āˆ‘ i āˆˆ s, f i āˆˆ ā؆ i āˆˆ s, p i

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

      source
      šŸ“ coverage
      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
      šŸ“ coverage
      @[simp]
      theorem Submodule.toAddSubmonoid_sSup {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set (Submodule R M)) :
      (sSup s).toAddSubmonoid = sSup (toAddSubmonoid '' s)
      source
      šŸ“ coverage
      @[simp]
      theorem Submodule.subsingleton_iff (R : Type u_1) {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
      Subsingleton (Submodule R M) ā†” Subsingleton M
      source
      šŸ“ coverage
      @[simp]
      theorem Submodule.nontrivial_iff (R : Type u_1) {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
      Nontrivial (Submodule R M) ā†” Nontrivial M
      source
      šŸ”ø coverage
      @[implicit_reducible]
      instance Submodule.instUniqueOfSubsingleton {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Subsingleton M] :
      Unique (Submodule R M)
      source
      šŸ”ø coverage
      @[implicit_reducible]
      instance Submodule.unique' {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Subsingleton R] :
      Unique (Submodule R M)
      source
      šŸ“ coverage
      instance Submodule.instNontrivial {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial M] :
      Nontrivial (Submodule R M)

      Disjointness of submodules #

      source
      šŸ“ coverage
      theorem Submodule.disjoint_def {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p p' : Submodule R M} :
      Disjoint p p' ā†” āˆ€ x āˆˆ p, x āˆˆ p' ā†’ x = 0
      source
      šŸ“ coverage
      theorem Submodule.disjoint_def' {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p p' : Submodule R M} :
      Disjoint p p' ā†” āˆ€ x āˆˆ p, āˆ€ y āˆˆ p', x = y ā†’ x = 0
      source
      šŸ“ coverage
      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 q : Submodule R M} (hpq : Disjoint p q) {a : ā†„p} (ha : ā†‘a āˆˆ q) :
      a = 0
      source
      šŸ“ coverage
      theorem Submodule.mem_right_iff_eq_zero_of_disjoint {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p p' : Submodule R M} (h : Disjoint p p') {x : ā†„p} :
      ā†‘x āˆˆ p' ā†” x = 0
      source
      šŸ“ coverage
      theorem Submodule.mem_left_iff_eq_zero_of_disjoint {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p p' : Submodule R M} (h : Disjoint p p') {x : ā†„p'} :
      ā†‘x āˆˆ p ā†” x = 0
      source
      šŸ“ coverage
      theorem Submodule.disjoint_iff_add_eq_zero {M : Type u_4} {R : Type u_5} [Ring R] [AddCommGroup M] [Module R M] {Nā‚ Nā‚‚ : Submodule R M} :
      Disjoint Nā‚ Nā‚‚ ā†” āˆ€ {x y : M}, x āˆˆ Nā‚ ā†’ y āˆˆ Nā‚‚ ā†’ x + y = 0 ā†’ x = 0 āˆ§ y = 0

      Version of AddSubgroup.disjoint_iff_add_eq_zero for submodules.

      ā„•-submodules #

      source
      šŸ”ø coverage
      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
        šŸ“ coverage
        @[simp]
        theorem AddSubmonoid.toNatSubmodule_symm {M : Type u_3} [AddCommMonoid M] :
        ā‡‘toNatSubmodule.symm = Submodule.toAddSubmonoid
        source
        šŸ“ coverage
        @[simp]
        theorem AddSubmonoid.coe_toNatSubmodule {M : Type u_3} [AddCommMonoid M] (S : AddSubmonoid M) :
        ā†‘(toNatSubmodule S) = ā†‘S
        source
        šŸ“ coverage
        @[simp]
        theorem AddSubmonoid.toNatSubmodule_toAddSubmonoid {M : Type u_3} [AddCommMonoid M] (S : AddSubmonoid M) :
        (toNatSubmodule S).toAddSubmonoid = S
        source
        šŸ“ coverage
        @[simp]
        theorem Submodule.toAddSubmonoid_toNatSubmodule {M : Type u_3} [AddCommMonoid M] (S : Submodule ā„• M) :
        AddSubmonoid.toNatSubmodule S.toAddSubmonoid = S

        ā„¤-submodules #

        source
        šŸ”ø coverage
        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
          šŸ“ coverage
          @[simp]
          theorem AddSubgroup.toIntSubmodule_symm {M : Type u_3} [AddCommGroup M] :
          ā‡‘toIntSubmodule.symm = Submodule.toAddSubgroup
          source
          šŸ“ coverage
          @[simp]
          theorem AddSubgroup.coe_toIntSubmodule {M : Type u_3} [AddCommGroup M] (S : AddSubgroup M) :
          ā†‘(toIntSubmodule S) = ā†‘S
          source
          šŸ“ coverage
          @[simp]
          theorem AddSubgroup.toIntSubmodule_toAddSubgroup {M : Type u_3} [AddCommGroup M] (S : AddSubgroup M) :
          (toIntSubmodule S).toAddSubgroup = S
          source
          šŸ“ coverage
          theorem Submodule.toAddSubgroup_toIntSubmodule {M : Type u_3} [AddCommGroup M] (S : Submodule ā„¤ M) :
          AddSubgroup.toIntSubmodule S.toAddSubgroup = S