# Homomorphisms of meet-semilattices

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Ian Ray.

Created on 2022-11-07.

module order-theory.homomorphisms-meet-semilattices where

Imports
open import foundation.action-on-identifications-functions
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-prop-Semigroup
( 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-set-Meet-Semilattice : Set (l1 ⊔ l2)
hom-set-Meet-Semilattice =
hom-set-Semigroup
( semigroup-Meet-Semilattice A)
( semigroup-Meet-Semilattice B)

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

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

module _
(f : 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) ∙
( ap map-hom-Meet-Semilattice H)

hom-poset-hom-Meet-Semilattice :
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 :
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 :
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 :
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-set-Order-Theoretic-Meet-Semilattice : Set (l1 ⊔ l2 ⊔ l3 ⊔ l4)
hom-set-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)