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.

Bottom element of a submodule #

instance Submodule.instBot {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :

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

Equations
    instance Submodule.inhabited' {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
    Equations
      @[simp]
      theorem Submodule.bot_coe {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
      = {0}
      @[simp]
      @[simp]
      theorem Submodule.bot_toAddSubgroup {R : Type u_4} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] :
      @[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
      instance Submodule.uniqueBot {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
      Equations
        instance Submodule.instOrderBot {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
        Equations
          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 = xp, x = 0
          theorem Submodule.bot_ext {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (x y : ) :
          x = y
          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
          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 xp, x 0
          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
          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 ) :
          bp, b 0

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

          Equations
            Instances For
              @[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}) :
              @[simp]
              theorem Submodule.botEquivPUnit_apply {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (x✝ : ) :
              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} :
              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 =
              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} :

              Top element of a submodule #

              instance Submodule.instTop {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :

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

              Equations
                @[simp]
                theorem Submodule.top_coe {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
                @[simp]
                @[simp]
                theorem Submodule.top_toAddSubgroup {R : Type u_4} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] :
                @[simp]
                theorem Submodule.mem_top {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} :
                instance Submodule.instOrderTop {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
                Equations
                  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
                  def Submodule.topEquiv {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :

                  The top submodule is linearly equivalent to the module.

                  This is the module version of AddSubmonoid.topEquiv.

                  Equations
                    Instances For
                      @[simp]
                      theorem Submodule.topEquiv_apply {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (x : ) :
                      topEquiv x = x
                      @[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 #

                      instance Submodule.instInfSet {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
                      Equations
                        instance Submodule.instMin {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
                        Equations
                          instance Submodule.completeLattice {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
                          Equations
                            @[simp]
                            theorem Submodule.inf_coe {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {p q : Submodule R M} :
                            (pq) = p q
                            @[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 pq x p x q
                            @[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) = pP, p
                            @[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) :
                            (s.inf p) = is, (p i)
                            @[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)
                            @[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 pS, x p
                            @[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
                            @[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 s.inf p is, x p i
                            theorem Submodule.inf_iInf {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_4} [Nonempty ι] {p : ιSubmodule R M} (q : Submodule R M) :
                            q⨅ (i : ι), p i = ⨅ (i : ι), qp i
                            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 Sx ST
                            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 Tx ST
                            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 ST
                            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 ST
                            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
                            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
                            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 : is, f i p i) :
                            is, f i is, p i

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

                            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 sx sSup S
                            @[simp]
                            @[simp]
                            Equations
                              instance Submodule.unique' {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Subsingleton R] :
                              Equations

                                Disjointness of submodules #

                                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' xp, x p'x = 0
                                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' xp, yp', x = yx = 0
                                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
                                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
                                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

                                ℕ-submodules #

                                An additive submonoid is equivalent to a ℕ-submodule.

                                Equations
                                  Instances For
                                    @[simp]

                                    ℤ-submodules #

                                    An additive subgroup is equivalent to a ℤ-submodule.

                                    Equations
                                      Instances For
                                        @[simp]
                                        theorem AddSubgroup.coe_toIntSubmodule {M : Type u_3} [AddCommGroup M] (S : AddSubgroup M) :
                                        (toIntSubmodule S) = S