Documentation

Mathlib.Order.ModularLattice

Modular Lattices #

This file defines (semi)modular lattices, a kind of lattice useful in algebra. For examples, look to the subobject lattices of abelian groups, submodules, and ideals, or consider any distributive lattice.

Typeclasses #

We define (semi)modularity typeclasses as Prop-valued mixins.

Main Definitions #

Main Results #

References #

TODO #

A weakly upper modular lattice is a lattice where a ⊔ b covers a and b if a and b both cover a ⊓ b.

  • covBy_sup_of_inf_covBy_covBy : ∀ {a b : α}, a b aa b ba a b

    a ⊔ b covers a and b if a and b both cover a ⊓ b.

Instances
    theorem IsWeakUpperModularLattice.covBy_sup_of_inf_covBy_covBy {α : Type u_2} :
    ∀ {inst : Lattice α} [self : IsWeakUpperModularLattice α] {a b : α}, a b aa b ba a b

    a ⊔ b covers a and b if a and b both cover a ⊓ b.

    A weakly lower modular lattice is a lattice where a and b cover a ⊓ b if a ⊔ b covers both a and b.

    • inf_covBy_of_covBy_covBy_sup : ∀ {a b : α}, a a bb a ba b a

      a and b cover a ⊓ b if a ⊔ b covers both a and b

    Instances
      theorem IsWeakLowerModularLattice.inf_covBy_of_covBy_covBy_sup {α : Type u_2} :
      ∀ {inst : Lattice α} [self : IsWeakLowerModularLattice α] {a b : α}, a a bb a ba b a

      a and b cover a ⊓ b if a ⊔ b covers both a and b

      class IsUpperModularLattice (α : Type u_2) [Lattice α] :

      An upper modular lattice, aka semimodular lattice, is a lattice where a ⊔ b covers a and b if either a or b covers a ⊓ b.

      • covBy_sup_of_inf_covBy : ∀ {a b : α}, a b ab a b

        a ⊔ b covers a and b if either a or b covers a ⊓ b

      Instances
        theorem IsUpperModularLattice.covBy_sup_of_inf_covBy {α : Type u_2} :
        ∀ {inst : Lattice α} [self : IsUpperModularLattice α] {a b : α}, a b ab a b

        a ⊔ b covers a and b if either a or b covers a ⊓ b

        class IsLowerModularLattice (α : Type u_2) [Lattice α] :

        A lower modular lattice is a lattice where a and b both cover a ⊓ b if a ⊔ b covers either a or b.

        • inf_covBy_of_covBy_sup : ∀ {a b : α}, a a ba b b

          a and b both cover a ⊓ b if a ⊔ b covers either a or b

        Instances
          theorem IsLowerModularLattice.inf_covBy_of_covBy_sup {α : Type u_2} :
          ∀ {inst : Lattice α} [self : IsLowerModularLattice α] {a b : α}, a a ba b b

          a and b both cover a ⊓ b if a ⊔ b covers either a or b

          class IsModularLattice (α : Type u_2) [Lattice α] :

          A modular lattice is one with a limited associativity between and .

          • sup_inf_le_assoc_of_le : ∀ {x : α} (y : α) {z : α}, x z(x y) z x y z

            Whenever x ≤ z, then for any y, (x ⊔ y) ⊓ z ≤ x ⊔ (y ⊓ z)

          Instances
            theorem IsModularLattice.sup_inf_le_assoc_of_le {α : Type u_2} :
            ∀ {inst : Lattice α} [self : IsModularLattice α] {x : α} (y : α) {z : α}, x z(x y) z x y z

            Whenever x ≤ z, then for any y, (x ⊔ y) ⊓ z ≤ x ⊔ (y ⊓ z)

            theorem covBy_sup_of_inf_covBy_of_inf_covBy_left {α : Type u_1} [Lattice α] [IsWeakUpperModularLattice α] {a : α} {b : α} :
            a b aa b ba a b
            theorem covBy_sup_of_inf_covBy_of_inf_covBy_right {α : Type u_1} [Lattice α] [IsWeakUpperModularLattice α] {a : α} {b : α} :
            a b aa b bb a b
            theorem CovBy.sup_of_inf_of_inf_left {α : Type u_1} [Lattice α] [IsWeakUpperModularLattice α] {a : α} {b : α} :
            a b aa b ba a b

            Alias of covBy_sup_of_inf_covBy_of_inf_covBy_left.

            theorem CovBy.sup_of_inf_of_inf_right {α : Type u_1} [Lattice α] [IsWeakUpperModularLattice α] {a : α} {b : α} :
            a b aa b bb a b

            Alias of covBy_sup_of_inf_covBy_of_inf_covBy_right.

            theorem inf_covBy_of_covBy_sup_of_covBy_sup_left {α : Type u_1} [Lattice α] [IsWeakLowerModularLattice α] {a : α} {b : α} :
            a a bb a ba b a
            theorem inf_covBy_of_covBy_sup_of_covBy_sup_right {α : Type u_1} [Lattice α] [IsWeakLowerModularLattice α] {a : α} {b : α} :
            a a bb a ba b b
            theorem CovBy.inf_of_sup_of_sup_left {α : Type u_1} [Lattice α] [IsWeakLowerModularLattice α] {a : α} {b : α} :
            a a bb a ba b a

            Alias of inf_covBy_of_covBy_sup_of_covBy_sup_left.

            theorem CovBy.inf_of_sup_of_sup_right {α : Type u_1} [Lattice α] [IsWeakLowerModularLattice α] {a : α} {b : α} :
            a a bb a ba b b

            Alias of inf_covBy_of_covBy_sup_of_covBy_sup_right.

            theorem covBy_sup_of_inf_covBy_left {α : Type u_1} [Lattice α] [IsUpperModularLattice α] {a : α} {b : α} :
            a b ab a b
            theorem covBy_sup_of_inf_covBy_right {α : Type u_1} [Lattice α] [IsUpperModularLattice α] {a : α} {b : α} :
            a b ba a b
            theorem CovBy.sup_of_inf_left {α : Type u_1} [Lattice α] [IsUpperModularLattice α] {a : α} {b : α} :
            a b ab a b

            Alias of covBy_sup_of_inf_covBy_left.

            theorem CovBy.sup_of_inf_right {α : Type u_1} [Lattice α] [IsUpperModularLattice α] {a : α} {b : α} :
            a b ba a b

            Alias of covBy_sup_of_inf_covBy_right.

            theorem inf_covBy_of_covBy_sup_left {α : Type u_1} [Lattice α] [IsLowerModularLattice α] {a : α} {b : α} :
            a a ba b b
            theorem inf_covBy_of_covBy_sup_right {α : Type u_1} [Lattice α] [IsLowerModularLattice α] {a : α} {b : α} :
            b a ba b a
            theorem CovBy.inf_of_sup_left {α : Type u_1} [Lattice α] [IsLowerModularLattice α] {a : α} {b : α} :
            a a ba b b

            Alias of inf_covBy_of_covBy_sup_left.

            theorem CovBy.inf_of_sup_right {α : Type u_1} [Lattice α] [IsLowerModularLattice α] {a : α} {b : α} :
            b a ba b a

            Alias of inf_covBy_of_covBy_sup_right.

            theorem sup_inf_assoc_of_le {α : Type u_1} [Lattice α] [IsModularLattice α] {x : α} (y : α) {z : α} (h : x z) :
            (x y) z = x y z
            theorem IsModularLattice.inf_sup_inf_assoc {α : Type u_1} [Lattice α] [IsModularLattice α] {x : α} {y : α} {z : α} :
            x z y z = (x z y) z
            theorem inf_sup_assoc_of_le {α : Type u_1} [Lattice α] [IsModularLattice α] {x : α} (y : α) {z : α} (h : z x) :
            x y z = x (y z)
            theorem IsModularLattice.sup_inf_sup_assoc {α : Type u_1} [Lattice α] [IsModularLattice α] {x : α} {y : α} {z : α} :
            (x z) (y z) = (x z) y z
            theorem eq_of_le_of_inf_le_of_le_sup {α : Type u_1} [Lattice α] [IsModularLattice α] {x : α} {y : α} {z : α} (hxy : x y) (hinf : y z x) (hsup : y x z) :
            x = y
            theorem eq_of_le_of_inf_le_of_sup_le {α : Type u_1} [Lattice α] [IsModularLattice α] {x : α} {y : α} {z : α} (hxy : x y) (hinf : y z x z) (hsup : y z x z) :
            x = y
            theorem sup_lt_sup_of_lt_of_inf_le_inf {α : Type u_1} [Lattice α] [IsModularLattice α] {x : α} {y : α} {z : α} (hxy : x < y) (hinf : y z x z) :
            x z < y z
            theorem inf_lt_inf_of_lt_of_sup_le_sup {α : Type u_1} [Lattice α] [IsModularLattice α] {x : α} {y : α} {z : α} (hxy : x < y) (hinf : y z x z) :
            x z < y z
            theorem strictMono_inf_prod_sup {α : Type u_1} [Lattice α] [IsModularLattice α] {z : α} :
            StrictMono fun (x : α) => (x z, x z)
            theorem wellFounded_lt_exact_sequence {α : Type u_1} [Lattice α] [IsModularLattice α] {β : Type u_2} {γ : Type u_3} [PartialOrder β] [Preorder γ] [h₁ : WellFoundedLT β] [h₂ : WellFoundedLT γ] (K : α) (f₁ : βα) (f₂ : αβ) (g₁ : γα) (g₂ : αγ) (gci : GaloisCoinsertion f₁ f₂) (gi : GaloisInsertion g₂ g₁) (hf : ∀ (a : α), f₁ (f₂ a) = a K) (hg : ∀ (a : α), g₁ (g₂ a) = a K) :

            A generalization of the theorem that if N is a submodule of M and N and M / N are both Artinian, then M is Artinian.

            theorem wellFounded_gt_exact_sequence {α : Type u_1} [Lattice α] [IsModularLattice α] {β : Type u_2} {γ : Type u_3} [Preorder β] [PartialOrder γ] [WellFoundedGT β] [WellFoundedGT γ] (K : α) (f₁ : βα) (f₂ : αβ) (g₁ : γα) (g₂ : αγ) (gci : GaloisCoinsertion f₁ f₂) (gi : GaloisInsertion g₂ g₁) (hf : ∀ (a : α), f₁ (f₂ a) = a K) (hg : ∀ (a : α), g₁ (g₂ a) = a K) :

            A generalization of the theorem that if N is a submodule of M and N and M / N are both Noetherian, then M is Noetherian.

            @[simp]
            theorem infIccOrderIsoIccSup_symm_apply_coe {α : Type u_1} [Lattice α] [IsModularLattice α] (a : α) (b : α) (x : (Set.Icc b (a b))) :
            ((RelIso.symm (infIccOrderIsoIccSup a b)) x) = a x
            @[simp]
            theorem infIccOrderIsoIccSup_apply_coe {α : Type u_1} [Lattice α] [IsModularLattice α] (a : α) (b : α) (x : (Set.Icc (a b) a)) :
            ((infIccOrderIsoIccSup a b) x) = x b
            def infIccOrderIsoIccSup {α : Type u_1} [Lattice α] [IsModularLattice α] (a : α) (b : α) :
            (Set.Icc (a b) a) ≃o (Set.Icc b (a b))

            The diamond isomorphism between the intervals [a ⊓ b, a] and [b, a ⊔ b]

            Equations
            Instances For
              theorem inf_strictMonoOn_Icc_sup {α : Type u_1} [Lattice α] [IsModularLattice α] {a : α} {b : α} :
              StrictMonoOn (fun (c : α) => a c) (Set.Icc b (a b))
              theorem sup_strictMonoOn_Icc_inf {α : Type u_1} [Lattice α] [IsModularLattice α] {a : α} {b : α} :
              StrictMonoOn (fun (c : α) => c b) (Set.Icc (a b) a)
              @[simp]
              theorem infIooOrderIsoIooSup_apply_coe {α : Type u_1} [Lattice α] [IsModularLattice α] (a : α) (b : α) (c : (Set.Ioo (a b) a)) :
              ((infIooOrderIsoIooSup a b) c) = c b
              @[simp]
              theorem infIooOrderIsoIooSup_symm_apply_coe {α : Type u_1} [Lattice α] [IsModularLattice α] (a : α) (b : α) (c : (Set.Ioo b (a b))) :
              ((RelIso.symm (infIooOrderIsoIooSup a b)) c) = a c
              def infIooOrderIsoIooSup {α : Type u_1} [Lattice α] [IsModularLattice α] (a : α) (b : α) :
              (Set.Ioo (a b) a) ≃o (Set.Ioo b (a b))

              The diamond isomorphism between the intervals ]a ⊓ b, a[ and }b, a ⊔ b[.

              Equations
              Instances For
                @[instance 100]
                Equations
                • =
                @[instance 100]
                Equations
                • =
                def IsCompl.IicOrderIsoIci {α : Type u_1} [Lattice α] [BoundedOrder α] [IsModularLattice α] {a : α} {b : α} (h : IsCompl a b) :
                (Set.Iic a) ≃o (Set.Ici b)

                The diamond isomorphism between the intervals Set.Iic a and Set.Ici b.

                Equations
                Instances For
                  theorem isModularLattice_iff_inf_sup_inf_assoc {α : Type u_1} [Lattice α] :
                  IsModularLattice α ∀ (x y z : α), x z y z = (x z y) z
                  @[instance 100]
                  Equations
                  • =
                  theorem Disjoint.disjoint_sup_right_of_disjoint_sup_left {α : Type u_1} {a : α} {b : α} {c : α} [Lattice α] [OrderBot α] [IsModularLattice α] (h : Disjoint a b) (hsup : Disjoint (a b) c) :
                  Disjoint a (b c)
                  theorem Disjoint.disjoint_sup_left_of_disjoint_sup_right {α : Type u_1} {a : α} {b : α} {c : α} [Lattice α] [OrderBot α] [IsModularLattice α] (h : Disjoint b c) (hsup : Disjoint a (b c)) :
                  Disjoint (a b) c
                  theorem Disjoint.isCompl_sup_right_of_isCompl_sup_left {α : Type u_1} {a : α} {b : α} {c : α} [Lattice α] [BoundedOrder α] [IsModularLattice α] (h : Disjoint a b) (hcomp : IsCompl (a b) c) :
                  IsCompl a (b c)
                  theorem Disjoint.isCompl_sup_left_of_isCompl_sup_right {α : Type u_1} {a : α} {b : α} {c : α} [Lattice α] [BoundedOrder α] [IsModularLattice α] (h : Disjoint b c) (hcomp : IsCompl a (b c)) :
                  IsCompl (a b) c
                  theorem Set.Iic.isCompl_inf_inf_of_isCompl_of_le {α : Type u_1} [Lattice α] [BoundedOrder α] [IsModularLattice α] {a : α} {b : α} {c : α} (h₁ : IsCompl b c) (h₂ : b a) :
                  IsCompl a b, a c,
                  Equations
                  • =
                  Equations
                  • =