Documentation

Mathlib.Order.Category.Lat

The category of lattices #

This defines Lat, the category of lattices.

Note that Lat doesn't correspond to the literature definition of [Lat] (https://ncatlab.org/nlab/show/Lat) as we don't require bottom or top elements. Instead, Lat corresponds to BddLat.

TODO #

The free functor from Lat to BddLat is X → WithTop (WithBot X).

def Lat :
Type (u_1 + 1)

The category of lattices.

Equations
Instances For
    Equations
    instance Lat.instLatticeα (X : Lat) :
    Lattice X
    Equations
    • X.instLatticeα = X.str
    def Lat.of (α : Type u_1) [Lattice α] :

    Construct a bundled Lat from a Lattice.

    Equations
    Instances For
      @[simp]
      theorem Lat.coe_of (α : Type u_1) [Lattice α] :
      (Lat.of α) = α
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem Lat.Iso.mk_hom_toSupHom_toFun {α : Lat} {β : Lat} (e : α ≃o β) (a : α) :
      (Lat.Iso.mk e).hom.toSupHom a = e a
      @[simp]
      theorem Lat.Iso.mk_inv_toSupHom_toFun {α : Lat} {β : Lat} (e : α ≃o β) (a : β) :
      (Lat.Iso.mk e).inv.toSupHom a = e.symm a
      def Lat.Iso.mk {α : Lat} {β : Lat} (e : α ≃o β) :
      α β

      Constructs an isomorphism of lattices from an order isomorphism between them.

      Equations
      • Lat.Iso.mk e = { hom := { toFun := e, map_sup' := , map_inf' := }, inv := { toFun := e.symm, map_sup' := , map_inf' := }, hom_inv_id := , inv_hom_id := }
      Instances For
        @[simp]
        theorem Lat.dual_obj (X : Lat) :
        Lat.dual.obj X = Lat.of (↑X)ᵒᵈ
        @[simp]
        theorem Lat.dual_map :
        ∀ {X Y : Lat} (a : LatticeHom X Y), Lat.dual.map a = LatticeHom.dual a

        OrderDual as a functor.

        Equations
        Instances For

          The equivalence between Lat and itself induced by OrderDual both ways.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For