Documentation

Mathlib.Order.Sublattice

Sublattices #

This file defines sublattices.

TODO #

Subsemilattices, if people care about them.

Tags #

sublattice

structure Sublattice (α : Type u_2) [Lattice α] :
Type u_2

A sublattice of a lattice is a set containing the suprema and infima of any of its elements.

  • carrier : Set α

    The underlying set of a sublattice. Do not use directly. Instead, use the coercion Sublattice α → Set α, which Lean should automatically insert for you in most cases.

  • supClosed' : SupClosed self.carrier
  • infClosed' : InfClosed self.carrier
Instances For
    theorem Sublattice.supClosed' {α : Type u_2} [Lattice α] (self : Sublattice α) :
    SupClosed self.carrier
    theorem Sublattice.infClosed' {α : Type u_2} [Lattice α] (self : Sublattice α) :
    InfClosed self.carrier
    instance Sublattice.instSetLike {α : Type u_2} [Lattice α] :
    Equations
    • Sublattice.instSetLike = { coe := fun (L : Sublattice α) => L.carrier, coe_injective' := }
    @[reducible, inline]
    abbrev Sublattice.ofIsSublattice {α : Type u_2} [Lattice α] (s : Set α) (hs : IsSublattice s) :

    Turn a set closed under supremum and infimum into a sublattice.

    Equations
    Instances For
      theorem Sublattice.coe_inj {α : Type u_2} [Lattice α] {L : Sublattice α} {M : Sublattice α} :
      L = M L = M
      @[simp]
      theorem Sublattice.supClosed {α : Type u_2} [Lattice α] (L : Sublattice α) :
      @[simp]
      theorem Sublattice.infClosed {α : Type u_2} [Lattice α] (L : Sublattice α) :
      @[simp]
      theorem Sublattice.isSublattice {α : Type u_2} [Lattice α] (L : Sublattice α) :
      @[simp]
      theorem Sublattice.mem_carrier {α : Type u_2} [Lattice α] {L : Sublattice α} {a : α} :
      a L.carrier a L
      @[simp]
      theorem Sublattice.mem_mk {α : Type u_2} [Lattice α] {s : Set α} {a : α} (h_sup : SupClosed s) (h_inf : InfClosed s) :
      a { carrier := s, supClosed' := h_sup, infClosed' := h_inf } a s
      @[simp]
      theorem Sublattice.coe_mk {α : Type u_2} [Lattice α] {s : Set α} (h_sup : SupClosed s) (h_inf : InfClosed s) :
      { carrier := s, supClosed' := h_sup, infClosed' := h_inf } = s
      @[simp]
      theorem Sublattice.mk_le_mk {α : Type u_2} [Lattice α] {s : Set α} {t : Set α} (hs_sup : SupClosed s) (hs_inf : InfClosed s) (ht_sup : SupClosed t) (ht_inf : InfClosed t) :
      { carrier := s, supClosed' := hs_sup, infClosed' := hs_inf } { carrier := t, supClosed' := ht_sup, infClosed' := ht_inf } s t
      @[simp]
      theorem Sublattice.mk_lt_mk {α : Type u_2} [Lattice α] {s : Set α} {t : Set α} (hs_sup : SupClosed s) (hs_inf : InfClosed s) (ht_sup : SupClosed t) (ht_inf : InfClosed t) :
      { carrier := s, supClosed' := hs_sup, infClosed' := hs_inf } < { carrier := t, supClosed' := ht_sup, infClosed' := ht_inf } s t
      def Sublattice.copy {α : Type u_2} [Lattice α] (L : Sublattice α) (s : Set α) (hs : s = L) :

      Copy of a sublattice with a new carrier equal to the old one. Useful to fix definitional equalities.

      Equations
      • L.copy s hs = { carrier := s, supClosed' := , infClosed' := }
      Instances For
        @[simp]
        theorem Sublattice.coe_copy {α : Type u_2} [Lattice α] (L : Sublattice α) (s : Set α) (hs : s = L) :
        (L.copy s hs) = s
        theorem Sublattice.copy_eq {α : Type u_2} [Lattice α] (L : Sublattice α) (s : Set α) (hs : s = L) :
        L.copy s hs = L
        theorem Sublattice.ext {α : Type u_2} [Lattice α] {L : Sublattice α} {M : Sublattice α} :
        (∀ (a : α), a L a M)L = M

        Two sublattices are equal if they have the same elements.

        instance Sublattice.instSupCoe {α : Type u_2} [Lattice α] {L : Sublattice α} :
        Sup L

        A sublattice of a lattice inherits a supremum.

        Equations
        • Sublattice.instSupCoe = { sup := fun (a b : L) => a b, }
        instance Sublattice.instInfCoe {α : Type u_2} [Lattice α] {L : Sublattice α} :
        Inf L

        A sublattice of a lattice inherits an infimum.

        Equations
        • Sublattice.instInfCoe = { inf := fun (a b : L) => a b, }
        @[simp]
        theorem Sublattice.coe_sup {α : Type u_2} [Lattice α] {L : Sublattice α} (a : L) (b : L) :
        (a b) = a b
        @[simp]
        theorem Sublattice.coe_inf {α : Type u_2} [Lattice α] {L : Sublattice α} (a : L) (b : L) :
        (a b) = a b
        @[simp]
        theorem Sublattice.mk_sup_mk {α : Type u_2} [Lattice α] {L : Sublattice α} (a : α) (b : α) (ha : a L) (hb : b L) :
        a, ha b, hb = a b,
        @[simp]
        theorem Sublattice.mk_inf_mk {α : Type u_2} [Lattice α] {L : Sublattice α} (a : α) (b : α) (ha : a L) (hb : b L) :
        a, ha b, hb = a b,
        instance Sublattice.instLatticeCoe {α : Type u_2} [Lattice α] (L : Sublattice α) :
        Lattice L

        A sublattice of a lattice inherits a lattice structure.

        Equations

        A sublattice of a distributive lattice inherits a distributive lattice structure.

        Equations
        def Sublattice.subtype {α : Type u_2} [Lattice α] (L : Sublattice α) :
        LatticeHom (L) α

        The natural lattice hom from a sublattice to the original lattice.

        Equations
        • L.subtype = { toFun := Subtype.val, map_sup' := , map_inf' := }
        Instances For
          @[simp]
          theorem Sublattice.coe_subtype {α : Type u_2} [Lattice α] (L : Sublattice α) :
          L.subtype = Subtype.val
          theorem Sublattice.subtype_apply {α : Type u_2} [Lattice α] (L : Sublattice α) (a : L) :
          L.subtype a = a
          theorem Sublattice.subtype_injective {α : Type u_2} [Lattice α] (L : Sublattice α) :
          Function.Injective L.subtype
          def Sublattice.inclusion {α : Type u_2} [Lattice α] {L : Sublattice α} {M : Sublattice α} (h : L M) :
          LatticeHom L M

          The inclusion homomorphism from a sublattice L to a bigger sublattice M.

          Equations
          Instances For
            @[simp]
            theorem Sublattice.coe_inclusion {α : Type u_2} [Lattice α] {L : Sublattice α} {M : Sublattice α} (h : L M) :
            theorem Sublattice.inclusion_apply {α : Type u_2} [Lattice α] {L : Sublattice α} {M : Sublattice α} (h : L M) (a : L) :
            @[simp]
            @[simp]
            theorem Sublattice.subtype_comp_inclusion {α : Type u_2} [Lattice α] {L : Sublattice α} {M : Sublattice α} (h : L M) :
            M.subtype.comp (Sublattice.inclusion h) = L.subtype
            instance Sublattice.instTop {α : Type u_2} [Lattice α] :

            The maximum sublattice of a lattice.

            Equations
            • Sublattice.instTop = { top := { carrier := Set.univ, supClosed' := , infClosed' := } }
            instance Sublattice.instBot {α : Type u_2} [Lattice α] :

            The empty sublattice of a lattice.

            Equations
            • Sublattice.instBot = { bot := { carrier := , supClosed' := , infClosed' := } }
            instance Sublattice.instInf {α : Type u_2} [Lattice α] :

            The inf of two sublattices is their intersection.

            Equations
            • Sublattice.instInf = { inf := fun (L M : Sublattice α) => { carrier := L M, supClosed' := , infClosed' := } }
            instance Sublattice.instInfSet {α : Type u_2} [Lattice α] :

            The inf of sublattices is their intersection.

            Equations
            • Sublattice.instInfSet = { sInf := fun (S : Set (Sublattice α)) => { carrier := LS, L, supClosed' := , infClosed' := } }
            Equations
            • Sublattice.instInhabited = { default := }
            def Sublattice.topEquiv {α : Type u_2} [Lattice α] :
            ≃o α

            The top sublattice is isomorphic to the lattice.

            This is the sublattice version of Equiv.Set.univ α.

            Equations
            • Sublattice.topEquiv = { toEquiv := Equiv.Set.univ α, map_rel_iff' := }
            Instances For
              @[simp]
              theorem Sublattice.coe_top {α : Type u_2} [Lattice α] :
              = Set.univ
              @[simp]
              theorem Sublattice.coe_bot {α : Type u_2} [Lattice α] :
              =
              @[simp]
              theorem Sublattice.coe_inf' {α : Type u_2} [Lattice α] (L : Sublattice α) (M : Sublattice α) :
              (L M) = L M
              @[simp]
              theorem Sublattice.coe_sInf {α : Type u_2} [Lattice α] (S : Set (Sublattice α)) :
              (sInf S) = LS, L
              @[simp]
              theorem Sublattice.coe_iInf {ι : Sort u_1} {α : Type u_2} [Lattice α] (f : ιSublattice α) :
              (⨅ (i : ι), f i) = ⋂ (i : ι), (f i)
              @[simp]
              theorem Sublattice.coe_eq_univ {α : Type u_2} [Lattice α] {L : Sublattice α} :
              L = Set.univ L =
              @[simp]
              theorem Sublattice.coe_eq_empty {α : Type u_2} [Lattice α] {L : Sublattice α} :
              L = L =
              @[simp]
              theorem Sublattice.not_mem_bot {α : Type u_2} [Lattice α] (a : α) :
              a
              @[simp]
              theorem Sublattice.mem_top {α : Type u_2} [Lattice α] (a : α) :
              @[simp]
              theorem Sublattice.mem_inf {α : Type u_2} [Lattice α] {L : Sublattice α} {M : Sublattice α} {a : α} :
              a L M a L a M
              @[simp]
              theorem Sublattice.mem_sInf {α : Type u_2} [Lattice α] {a : α} {S : Set (Sublattice α)} :
              a sInf S LS, a L
              @[simp]
              theorem Sublattice.mem_iInf {ι : Sort u_1} {α : Type u_2} [Lattice α] {a : α} {f : ιSublattice α} :
              a ⨅ (i : ι), f i ∀ (i : ι), a f i

              Sublattices of a lattice form a complete lattice.

              Equations
              Equations
              • Sublattice.instUniqueOfIsEmpty = { toInhabited := Sublattice.instInhabited, uniq := }
              def Sublattice.comap {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (L : Sublattice β) :

              The preimage of a sublattice along a lattice homomorphism.

              Equations
              Instances For
                @[simp]
                theorem Sublattice.coe_comap {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (L : Sublattice β) (f : LatticeHom α β) :
                (Sublattice.comap f L) = f ⁻¹' L
                @[simp]
                theorem Sublattice.mem_comap {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {f : LatticeHom α β} {a : α} {L : Sublattice β} :
                theorem Sublattice.comap_mono {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {f : LatticeHom α β} :
                @[simp]
                theorem Sublattice.comap_id {α : Type u_2} [Lattice α] (L : Sublattice α) :
                @[simp]
                theorem Sublattice.comap_comap {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Lattice α] [Lattice β] [Lattice γ] (L : Sublattice γ) (g : LatticeHom β γ) (f : LatticeHom α β) :
                def Sublattice.map {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (L : Sublattice α) :

                The image of a sublattice along a monoid homomorphism is a sublattice.

                Equations
                • Sublattice.map f L = { carrier := f '' L, supClosed' := , infClosed' := }
                Instances For
                  @[simp]
                  theorem Sublattice.coe_map {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (L : Sublattice α) :
                  (Sublattice.map f L) = f '' L
                  @[simp]
                  theorem Sublattice.mem_map {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} {f : LatticeHom α β} {b : β} :
                  b Sublattice.map f L aL, f a = b
                  theorem Sublattice.mem_map_of_mem {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} (f : LatticeHom α β) {a : α} :
                  a Lf a Sublattice.map f L
                  theorem Sublattice.apply_coe_mem_map {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} (f : LatticeHom α β) (a : L) :
                  f a Sublattice.map f L
                  theorem Sublattice.map_mono {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {f : LatticeHom α β} :
                  @[simp]
                  theorem Sublattice.map_id {α : Type u_2} [Lattice α] {L : Sublattice α} :
                  @[simp]
                  theorem Sublattice.map_map {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Lattice α] [Lattice β] [Lattice γ] {L : Sublattice α} (g : LatticeHom β γ) (f : LatticeHom α β) :
                  theorem Sublattice.mem_map_equiv {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} {f : α ≃o β} {a : β} :
                  a Sublattice.map { toFun := f, map_sup' := , map_inf' := } L f.symm a L
                  theorem Sublattice.apply_mem_map_iff {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} {f : LatticeHom α β} {a : α} (hf : Function.Injective f) :
                  theorem Sublattice.map_equiv_eq_comap_symm {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : α ≃o β) (L : Sublattice α) :
                  Sublattice.map { toFun := f, map_sup' := , map_inf' := } L = Sublattice.comap { toFun := f.symm, map_sup' := , map_inf' := } L
                  theorem Sublattice.comap_equiv_eq_map_symm {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : β ≃o α) (L : Sublattice α) :
                  Sublattice.comap { toFun := f, map_sup' := , map_inf' := } L = Sublattice.map { toFun := f.symm, map_sup' := , map_inf' := } L
                  theorem Sublattice.map_symm_eq_iff_eq_map {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} {M : Sublattice β} {e : β ≃o α} :
                  Sublattice.map { toFun := e.symm, map_sup' := , map_inf' := } L = M L = Sublattice.map { toFun := e, map_sup' := , map_inf' := } M
                  theorem Sublattice.map_le_iff_le_comap {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] {L : Sublattice α} {f : LatticeHom α β} {M : Sublattice β} :
                  @[simp]
                  theorem Sublattice.map_bot {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) :
                  theorem Sublattice.map_sup {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (L : Sublattice α) (M : Sublattice α) :
                  theorem Sublattice.map_iSup {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (L : ιSublattice α) :
                  Sublattice.map f (⨆ (i : ι), L i) = ⨆ (i : ι), Sublattice.map f (L i)
                  @[simp]
                  theorem Sublattice.comap_top {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) :
                  theorem Sublattice.comap_inf {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (L : Sublattice β) (M : Sublattice β) (f : LatticeHom α β) :
                  theorem Sublattice.comap_iInf {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (s : ιSublattice β) :
                  Sublattice.comap f (iInf s) = ⨅ (i : ι), Sublattice.comap f (s i)
                  theorem Sublattice.map_inf_le {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (L : Sublattice α) (M : Sublattice α) (f : LatticeHom α β) :
                  theorem Sublattice.le_comap_sup {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (L : Sublattice β) (M : Sublattice β) (f : LatticeHom α β) :
                  theorem Sublattice.le_comap_iSup {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (L : ιSublattice β) :
                  ⨆ (i : ι), Sublattice.comap f (L i) Sublattice.comap f (⨆ (i : ι), L i)
                  theorem Sublattice.map_inf {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (L : Sublattice α) (M : Sublattice α) (f : LatticeHom α β) (hf : Function.Injective f) :
                  theorem Sublattice.map_top {α : Type u_2} {β : Type u_3} [Lattice α] [Lattice β] (f : LatticeHom α β) (h : Function.Surjective f) :