Documentation

Mathlib.Order.Category.CompleteLat

The category of complete lattices #

This file defines CompleteLat, the category of complete lattices.

def CompleteLat :
Type (u_1 + 1)

The category of complete lattices.

Equations
Instances For
    Equations
    Equations
    • X.instCompleteLatticeα = X.str

    Construct a bundled CompleteLat from a CompleteLattice.

    Equations
    Instances For
      @[simp]
      theorem CompleteLat.coe_of (α : Type u_1) [CompleteLattice α] :
      (CompleteLat.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 CompleteLat.Iso.mk_inv_toFun {α : CompleteLat} {β : CompleteLat} (e : α ≃o β) (a : β) :
      (CompleteLat.Iso.mk e).inv.toFun a = e.symm a
      @[simp]
      theorem CompleteLat.Iso.mk_hom_toFun {α : CompleteLat} {β : CompleteLat} (e : α ≃o β) (a : α) :
      (CompleteLat.Iso.mk e).hom.toFun a = e a
      def CompleteLat.Iso.mk {α : CompleteLat} {β : CompleteLat} (e : α ≃o β) :
      α β

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

      Equations
      • CompleteLat.Iso.mk e = { hom := { toFun := e, map_sInf' := , map_sSup' := }, inv := { toFun := e.symm, map_sInf' := , map_sSup' := }, hom_inv_id := , inv_hom_id := }
      Instances For
        @[simp]
        theorem CompleteLat.dual_map {X : CompleteLat} {Y : CompleteLat} (a : CompleteLatticeHom X Y) :
        CompleteLat.dual.map a = CompleteLatticeHom.dual a

        OrderDual as a functor.

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

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

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