Documentation

Mathlib.Order.Category.CompleteLat

The category of complete lattices #

This file defines CompleteLat, the category of complete lattices.

source
def CompleteLat :
Type (u_1 + 1)

The category of complete lattices.

Equations
Instances For
    source
    instance CompleteLat.instCoeSortCompleteLatType :
    CoeSort CompleteLat (Type u_1)
    Equations
    source
    instance CompleteLat.instCompleteLatticeα (X : CompleteLat) :
    CompleteLattice ↑X
    Equations
    source
    def CompleteLat.of (α : Type u_1) [CompleteLattice α] :
    CompleteLat

    Construct a bundled CompleteLat from a CompleteLattice.

    Equations
    Instances For
      source
      @[simp]
      theorem CompleteLat.coe_of (α : Type u_1) [CompleteLattice α] :
      ↑(CompleteLat.of α) = α
      source
      instance CompleteLat.instInhabitedCompleteLat :
      Inhabited CompleteLat
      Equations
      source
      instance CompleteLat.instBundledHomTypeCompleteLatticeCompleteLatticeHom :
      CategoryTheory.BundledHom CompleteLatticeHom
      Equations
      • One or more equations did not get rendered due to their size.
      source
      instance CompleteLat.instConcreteCategoryCompleteLatInstCompleteLatLargeCategory :
      CategoryTheory.ConcreteCategory CompleteLat
      Equations
      source
      instance CompleteLat.hasForgetToBddLat :
      CategoryTheory.HasForget₂ CompleteLat BddLat
      Equations
      • One or more equations did not get rendered due to their size.
      source
      @[simp]
      theorem CompleteLat.Iso.mk_inv_toFun {α : CompleteLat} {β : CompleteLat} (e : ↑α ≃o ↑β) (a : ↑β) :
      (CompleteLat.Iso.mk e).inv.tosInfHom.toFun a = (OrderIso.symm e) a
      source
      @[simp]
      theorem CompleteLat.Iso.mk_hom_toFun {α : CompleteLat} {β : CompleteLat} (e : ↑α ≃o ↑β) (a : ↑α) :
      (CompleteLat.Iso.mk e).hom.tosInfHom.toFun a = e a
      source
      def CompleteLat.Iso.mk {α : CompleteLat} {β : CompleteLat} (e : ↑α ≃o ↑β) :
      α ≅ β

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CompleteLat.dual_map {X : CompleteLat} {Y : CompleteLat} (a : CompleteLatticeHom ↑X ↑Y) :
        CompleteLat.dual.toPrefunctor.map a = CompleteLatticeHom.dual a
        source
        @[simp]
        theorem CompleteLat.dual_obj (X : CompleteLat) :
        CompleteLat.dual.toPrefunctor.obj X = CompleteLat.of (↑X)ᵒᵈ
        source
        def CompleteLat.dual :
        CategoryTheory.Functor CompleteLat CompleteLat

        OrderDual as a functor.

        Equations
        Instances For
          source
          @[simp]
          theorem CompleteLat.dualEquiv_functor :
          CompleteLat.dualEquiv.functor = CompleteLat.dual
          source
          @[simp]
          theorem CompleteLat.dualEquiv_inverse :
          CompleteLat.dualEquiv.inverse = CompleteLat.dual
          source
          def CompleteLat.dualEquiv :
          CompleteLat ≌ CompleteLat

          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
            source
            theorem completeLat_dual_comp_forget_to_bddLat :
            CategoryTheory.Functor.comp CompleteLat.dual (CategoryTheory.forget₂ CompleteLat BddLat) = CategoryTheory.Functor.comp (CategoryTheory.forget₂ CompleteLat BddLat) BddLat.dual