Homomorphisms of meet-semilattices

module order-theory.homomorphisms-meet-semilattices where
Imports
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.subtypes
open import foundation.universe-levels

open import group-theory.homomorphisms-semigroups

open import order-theory.greatest-lower-bounds-posets
open import order-theory.meet-semilattices
open import order-theory.order-preserving-maps-posets

Idea

A homomorphism of meet-semilattice is a map that preserves meets. It follows that homomorphisms of meet-semilattices are order preserving.

Definitions

Homomorphisms of algebraic meet-semilattices

module _
  {l1 l2 : Level}
  (A : Meet-Semilattice l1) (B : Meet-Semilattice l2)
  where

  preserves-meet-Prop :
    (type-Meet-Semilattice A  type-Meet-Semilattice B)  Prop (l1  l2)
  preserves-meet-Prop =
    preserves-mul-semigroup-Prop
      ( semigroup-Meet-Semilattice A)
      ( semigroup-Meet-Semilattice B)

  preserves-meet :
    (type-Meet-Semilattice A  type-Meet-Semilattice B)  UU (l1  l2)
  preserves-meet =
    preserves-mul-Semigroup
      ( semigroup-Meet-Semilattice A)
      ( semigroup-Meet-Semilattice B)

  is-prop-preserves-meet :
    (f : type-Meet-Semilattice A  type-Meet-Semilattice B) 
    is-prop (preserves-meet f)
  is-prop-preserves-meet =
    is-prop-preserves-mul-Semigroup
      ( semigroup-Meet-Semilattice A)
      ( semigroup-Meet-Semilattice B)

  hom-Meet-Semilattice : Set (l1  l2)
  hom-Meet-Semilattice =
    hom-Semigroup (semigroup-Meet-Semilattice A) (semigroup-Meet-Semilattice B)

  type-hom-Meet-Semilattice : UU (l1  l2)
  type-hom-Meet-Semilattice = type-Set hom-Meet-Semilattice

  is-set-type-hom-Meet-Semilattice : is-set type-hom-Meet-Semilattice
  is-set-type-hom-Meet-Semilattice = is-set-type-Set hom-Meet-Semilattice

  module _
    (f : type-hom-Meet-Semilattice)
    where

    map-hom-Meet-Semilattice :
      type-Meet-Semilattice A  type-Meet-Semilattice B
    map-hom-Meet-Semilattice = pr1 f

    preserves-meet-hom-Meet-Semilattice :
      preserves-meet map-hom-Meet-Semilattice
    preserves-meet-hom-Meet-Semilattice = pr2 f

    preserves-order-hom-Meet-Semilattice :
      preserves-order-Poset
        ( poset-Meet-Semilattice A)
        ( poset-Meet-Semilattice B)
        ( map-hom-Meet-Semilattice)
    preserves-order-hom-Meet-Semilattice x y H =
      ( inv (preserves-meet-hom-Meet-Semilattice x y)) 
      ( ap map-hom-Meet-Semilattice H)

    hom-poset-hom-Meet-Semilattice :
      type-hom-Poset (poset-Meet-Semilattice A) (poset-Meet-Semilattice B)
    pr1 hom-poset-hom-Meet-Semilattice = map-hom-Meet-Semilattice
    pr2 hom-poset-hom-Meet-Semilattice = preserves-order-hom-Meet-Semilattice

Homomorphisms of order-theoretic meet-semilattices

module _
  {l1 l2 l3 l4 : Level}
  (A : Order-Theoretic-Meet-Semilattice l1 l2)
  (B : Order-Theoretic-Meet-Semilattice l3 l4)
  where

  preserves-meet-hom-Poset-Prop :
    type-hom-Poset
      ( poset-Order-Theoretic-Meet-Semilattice A)
      ( poset-Order-Theoretic-Meet-Semilattice B)  Prop (l1  l3  l4)
  preserves-meet-hom-Poset-Prop (f , H) =
    Π-Prop
      ( type-Order-Theoretic-Meet-Semilattice A)
      ( λ x 
        Π-Prop
          ( type-Order-Theoretic-Meet-Semilattice A)
          ( λ y 
            is-greatest-binary-lower-bound-Poset-Prop
              ( poset-Order-Theoretic-Meet-Semilattice B)
              ( f x)
              ( f y)
              ( f (meet-Order-Theoretic-Meet-Semilattice A x y))))

  preserves-meet-hom-Poset :
    type-hom-Poset
      ( poset-Order-Theoretic-Meet-Semilattice A)
      ( poset-Order-Theoretic-Meet-Semilattice B)  UU (l1  l3  l4)
  preserves-meet-hom-Poset f =
    type-Prop (preserves-meet-hom-Poset-Prop f)

  is-prop-preserves-meet-hom-Prop :
    ( f :
      type-hom-Poset
        ( poset-Order-Theoretic-Meet-Semilattice A)
        ( poset-Order-Theoretic-Meet-Semilattice B)) 
    is-prop (preserves-meet-hom-Poset f)
  is-prop-preserves-meet-hom-Prop f =
    is-prop-type-Prop (preserves-meet-hom-Poset-Prop f)

  hom-Order-Theoretic-Meet-Semilattice : Set (l1  l2  l3  l4)
  hom-Order-Theoretic-Meet-Semilattice =
    set-subset
      ( hom-set-Poset
        ( poset-Order-Theoretic-Meet-Semilattice A)
        ( poset-Order-Theoretic-Meet-Semilattice B))
      ( preserves-meet-hom-Poset-Prop)