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
              source
              instance CompleteLat.instConcreteCategoryCompleteLatticeHomCarrier :
              CategoryTheory.ConcreteCategory CompleteLat fun (x1 x2 : CompleteLat) => CompleteLatticeHom ↑x1 ↑x2
              Equations
                source
                instance CompleteLat.hasForgetToBddLat :
                CategoryTheory.HasForget₂ CompleteLat BddLat
                Equations
                  source
                  def CompleteLat.Iso.mk {α β : CompleteLat} (e : ↑α ≃o ↑β) :
                  α ≅ β

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

                  Equations
                    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
                        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
                            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