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
  • Submodule.instBot = { bot := let __src := ; { carrier := {0}, add_mem' := , zero_mem' := , smul_mem' := } }
instance Submodule.inhabited' {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
Equations
  • Submodule.inhabited' = { default := }
@[simp]
theorem Submodule.bot_coe {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
= {0}
@[simp]
theorem Submodule.bot_toAddSubmonoid {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
.toAddSubmonoid =
@[simp]
theorem Submodule.bot_toAddSubgroup {R : Type u_4} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] :
.toAddSubgroup =
@[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
  • Submodule.uniqueBot = { toInhabited := inferInstance, uniq := }
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_iff {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] {x : } {y : } :
x = y True
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.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
@[simp]
theorem Submodule.botEquivPUnit_apply {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
∀ (x : ), Submodule.botEquivPUnit x = PUnit.unit
@[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} ), Submodule.botEquivPUnit.symm x = 0

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

Equations
  • Submodule.botEquivPUnit = { toFun := fun (x : ) => PUnit.unit, map_add' := , map_smul' := , invFun := fun (x : PUnit.{?u.42 + 1} ) => 0, left_inv := , right_inv := }
Instances For
    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
    • Submodule.instTop = { top := let __src := ; { carrier := Set.univ, add_mem' := , zero_mem' := , smul_mem' := } }
    @[simp]
    theorem Submodule.top_coe {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
    = Set.univ
    @[simp]
    theorem Submodule.top_toAddSubmonoid {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
    .toAddSubmonoid =
    @[simp]
    theorem Submodule.top_toAddSubgroup {R : Type u_4} {M : Type u_5} [Ring R] [AddCommGroup M] [Module R M] :
    .toAddSubgroup =
    @[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
    @[simp]
    theorem Submodule.topEquiv_symm_apply_coe {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) :
    (Submodule.topEquiv.symm x) = x
    @[simp]
    theorem Submodule.topEquiv_apply {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] (x : ) :
    Submodule.topEquiv x = x
    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
    • Submodule.topEquiv = { toFun := fun (x : ) => x, map_add' := , map_smul' := , invFun := fun (x : M) => x, , left_inv := , right_inv := }
    Instances For

      Infima & suprema in a submodule #

      instance Submodule.instInfSet {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
      Equations
      • Submodule.instInfSet = { sInf := fun (S : Set (Submodule R M)) => { carrier := sS, s, add_mem' := , zero_mem' := , smul_mem' := } }
      instance Submodule.instInf {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] :
      Equations
      • Submodule.instInf = { inf := fun (p q : Submodule R M) => { carrier := p q, add_mem' := , zero_mem' := , smul_mem' := } }
      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 : Submodule R M} {q : Submodule R M} :
      (p q) = p q
      @[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
      @[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 : ι), q p i
      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 Sx S T
      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 Tx S T
      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
      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
      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]
      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 (Submodule.toAddSubmonoid '' s)
      @[simp]
      Equations
      • Submodule.instUniqueOfSubsingleton = { default := , uniq := }
      instance Submodule.unique' {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Subsingleton R] :
      Equations
      • Submodule.unique' = inferInstance
      instance Submodule.instNontrivial {R : Type u_1} {M : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial M] :
      Equations
      • =

      Disjointness of submodules #

      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' 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 : Submodule R M} {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 : Submodule R M} {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 : Submodule R M} {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 : Submodule R M} {p' : Submodule R M} (h : Disjoint p p') {x : p'} :
      x p x = 0

      ℕ-submodules #

      An additive submonoid is equivalent to a ℕ-submodule.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem AddSubmonoid.toNatSubmodule_symm {M : Type u_3} [AddCommMonoid M] :
        AddSubmonoid.toNatSubmodule.symm = Submodule.toAddSubmonoid
        @[simp]
        theorem AddSubmonoid.coe_toNatSubmodule {M : Type u_3} [AddCommMonoid M] (S : AddSubmonoid M) :
        (AddSubmonoid.toNatSubmodule S) = S
        @[simp]
        theorem AddSubmonoid.toNatSubmodule_toAddSubmonoid {M : Type u_3} [AddCommMonoid M] (S : AddSubmonoid M) :
        (AddSubmonoid.toNatSubmodule S).toAddSubmonoid = S
        @[simp]
        theorem Submodule.toAddSubmonoid_toNatSubmodule {M : Type u_3} [AddCommMonoid M] (S : Submodule M) :
        AddSubmonoid.toNatSubmodule S.toAddSubmonoid = S

        ℤ-submodules #

        An additive subgroup is equivalent to a ℤ-submodule.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem AddSubgroup.toIntSubmodule_symm {M : Type u_3} [AddCommGroup M] :
          AddSubgroup.toIntSubmodule.symm = Submodule.toAddSubgroup
          @[simp]
          theorem AddSubgroup.coe_toIntSubmodule {M : Type u_3} [AddCommGroup M] (S : AddSubgroup M) :
          (AddSubgroup.toIntSubmodule S) = S
          @[simp]
          theorem AddSubgroup.toIntSubmodule_toAddSubgroup {M : Type u_3} [AddCommGroup M] (S : AddSubgroup M) :
          (AddSubgroup.toIntSubmodule S).toAddSubgroup = S
          @[simp]
          theorem Submodule.toAddSubgroup_toIntSubmodule {M : Type u_3} [AddCommGroup M] (S : Submodule M) :
          AddSubgroup.toIntSubmodule S.toAddSubgroup = S