Documentation

Mathlib.Order.Category.CompleteLat

The category of complete lattices #

This file defines CompleteLat, the category of complete lattices.

source
structure CompleteLat :
Type (u_1 + 1)

The category of complete lattices.

Instances For
    source
    instance CompleteLat.instCoeSortType :
    CoeSort CompleteLat (Type u_1)
    Equations
    source
    @[reducible, inline]
    abbrev CompleteLat.of (X : Type u_1) [CompleteLattice X] :
    CompleteLat

    Construct a bundled CompleteLat from the underlying type and typeclass.

    Equations
    Instances For
      source
      theorem CompleteLat.coe_of (α : Type u_1) [CompleteLattice α] :
      ↑(of α) = α
      source
      instance CompleteLat.instInhabited :
      Inhabited CompleteLat
      Equations
      source
      instance CompleteLat.instLargeCategory :
      CategoryTheory.LargeCategory CompleteLat
      Equations
      • One or more equations did not get rendered due to their size.
      source
      instance CompleteLat.instConcreteCategoryCompleteLatticeHomCarrier :
      CategoryTheory.ConcreteCategory CompleteLat fun (x1 x2 : CompleteLat) => CompleteLatticeHom ↑x1 ↑x2
      Equations
      • One or more equations did not get rendered due to their size.
      source
      instance CompleteLat.hasForgetToBddLat :
      CategoryTheory.HasForget₂ CompleteLat BddLat
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def CompleteLat.Iso.mk {α β : 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.Iso.mk_inv {α β : CompleteLat} (e : ↑α ≃o ↑β) :
        (mk e).inv = CategoryTheory.ConcreteCategory.ofHom { toFun := ⇑e.symm, map_sInf' := ⋯, map_sSup' := ⋯ }
        source
        @[simp]
        theorem CompleteLat.Iso.mk_hom {α β : CompleteLat} (e : ↑α ≃o ↑β) :
        (mk e).hom = CategoryTheory.ConcreteCategory.ofHom { toFun := ⇑e, map_sInf' := ⋯, map_sSup' := ⋯ }
        source
        def CompleteLat.dual :
        CategoryTheory.Functor CompleteLat CompleteLat

        OrderDual as a functor.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CompleteLat.dual_map {x✝ x✝¹ : CompleteLat} (a : CompleteLatticeHom ↑x✝ ↑x✝¹) :
          dual.map a = CompleteLatticeHom.dual a
          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
            @[simp]
            theorem CompleteLat.dualEquiv_inverse :
            dualEquiv.inverse = dual
            source
            @[simp]
            theorem CompleteLat.dualEquiv_functor :
            dualEquiv.functor = dual
            source
            theorem completeLat_dual_comp_forget_to_bddLat :
            CompleteLat.dual.comp (CategoryTheory.forget₂ CompleteLat BddLat) = (CategoryTheory.forget₂ CompleteLat BddLat).comp BddLat.dual