Documentation

Mathlib.Order.Category.CompleteLat

The category of complete lattices #

This file defines CompleteLat, the category of complete lattices.

source
🔶 coverage
structure CompleteLat :
Type (u_1 + 1)

The category of complete lattices.

Instances For
    source
    🔸 coverage
    @[implicit_reducible]
    instance CompleteLat.instCoeSortType :
    CoeSort CompleteLat (Type u_1)
    source
    📐 coverage
    theorem CompleteLat.coe_of (α : Type u_1) [CompleteLattice α] :
    ↑{ carrier := α, str := inst✝ } = α
    source
    🔸 coverage
    @[implicit_reducible]
    instance CompleteLat.instInhabited :
    Inhabited CompleteLat
    source
    🔸 coverage
    @[implicit_reducible]
    instance CompleteLat.instLargeCategory :
    CategoryTheory.LargeCategory CompleteLat
    source
    🔸 coverage
    @[implicit_reducible]
    instance CompleteLat.instConcreteCategoryCompleteLatticeHomCarrier :
    CategoryTheory.ConcreteCategory CompleteLat fun (x1 x2 : CompleteLat) => CompleteLatticeHom ↑x1 ↑x2
    source
    🔸 coverage
    @[implicit_reducible]
    instance CompleteLat.hasForgetToBddLat :
    CategoryTheory.HasForget₂ CompleteLat BddLat
    source
    🔸 coverage
    def CompleteLat.Iso.mk {α β : CompleteLat} (e : ↑α ≃o ↑β) :
    α ≅ β

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

    Instances For
      source
      📐 coverage
      @[simp]
      theorem CompleteLat.Iso.mk_inv {α β : CompleteLat} (e : ↑α ≃o ↑β) :
      (mk e).inv = CategoryTheory.ConcreteCategory.ofHom { toFun := ⇑e.symm, map_sInf' := ⋯, map_sSup' := ⋯ }
      source
      📐 coverage
      @[simp]
      theorem CompleteLat.Iso.mk_hom {α β : CompleteLat} (e : ↑α ≃o ↑β) :
      (mk e).hom = CategoryTheory.ConcreteCategory.ofHom { toFun := ⇑e, map_sInf' := ⋯, map_sSup' := ⋯ }
      source
      🔸 coverage
      def CompleteLat.dual :
      CategoryTheory.Functor CompleteLat CompleteLat

      OrderDual as a functor.

      Instances For
        source
        📐 coverage
        @[simp]
        theorem CompleteLat.dual_map {x✝ x✝¹ : CompleteLat} (a : CompleteLatticeHom ↑x✝ ↑x✝¹) :
        dual.map a = CompleteLatticeHom.dual a
        source
        🔸 coverage
        def CompleteLat.dualEquiv :
        CompleteLat ≌ CompleteLat

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

        Instances For
          source
          📐 coverage
          @[simp]
          theorem CompleteLat.dualEquiv_functor :
          dualEquiv.functor = dual
          source
          📐 coverage
          @[simp]
          theorem CompleteLat.dualEquiv_inverse :
          dualEquiv.inverse = dual
          source
          📐 coverage
          theorem completeLat_dual_comp_forget_to_bddLat :
          CompleteLat.dual.comp (CategoryTheory.forget₂ CompleteLat BddLat) = (CategoryTheory.forget₂ CompleteLat BddLat).comp BddLat.dual