Homomorphisms of suplattices

module order-theory.homomorphisms-sup-lattices where

Imports

open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.functions
open import foundation.universe-levels

open import order-theory.least-upper-bounds-posets
open import order-theory.order-preserving-maps-posets
open import order-theory.suplattices

Idea

A homomorphism of suplattices is a order preserving map between the underlying posets that preserves least upper bounds.

Definitions

module _
  {l1 l2 l3 l4 l5 l6 : Level}
  (A : Suplattice l1 l2 l3) (B : Suplattice l4 l5 l6)
  where

  preserves-sups :
    (type-Suplattice A → type-Suplattice B) →
    UU (l1 ⊔ lsuc l3 ⊔ l4 ⊔ l5)
  preserves-sups f =
    {I : UU l3} → (b : I → type-Suplattice A) →
    is-least-upper-bound-family-of-elements-Poset
      ( poset-Suplattice B)
      ( f ∘ b)
      ( f (sup-Suplattice A b))

  hom-Suplattice : UU (l1 ⊔ l2 ⊔ lsuc l3 ⊔ l4 ⊔ l5)
  hom-Suplattice =
    Σ ( type-Suplattice A → type-Suplattice B)
      ( λ f →
        preserves-order-Poset (poset-Suplattice A) (poset-Suplattice B) f ×
        preserves-sups f)

  map-hom-Suplattice :
    hom-Suplattice → type-Suplattice A → type-Suplattice B
  map-hom-Suplattice = pr1

  preserves-order-hom-Suplattice :
    (H : hom-Suplattice) →
    preserves-order-Poset
      ( poset-Suplattice A)
      ( poset-Suplattice B)
      ( map-hom-Suplattice H)
  preserves-order-hom-Suplattice = pr1 ∘ pr2

  preserves-sup-hom-Suplattice :
    (H : hom-Suplattice) → preserves-sups (map-hom-Suplattice H)
  preserves-sup-hom-Suplattice = pr2 ∘ pr2