# Homomorphisms of meet sup lattices

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

Created on 2022-11-07.
Last modified on 2023-06-10.

module order-theory.homomorphisms-meet-sup-lattices where

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

open import order-theory.homomorphisms-meet-semilattices
open import order-theory.homomorphisms-sup-lattices
open import order-theory.meet-suplattices
open import order-theory.order-preserving-maps-posets


## Idea

A homomorphism of meet-suplattices is a homomorphism of meet-semilattices that in addition preserves least upper bounds.

## Definitions

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

preserves-meets-sups :
(type-Meet-Suplattice A → type-Meet-Suplattice B) →
UU (l1 ⊔ lsuc l2 ⊔ l3)
preserves-meets-sups f =
preserves-meet
( meet-semilattice-Meet-Suplattice A)
( meet-semilattice-Meet-Suplattice B)
( f) ×
preserves-sups
( suplattice-Meet-Suplattice A)
( suplattice-Meet-Suplattice B)
( f)

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

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

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

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

preserves-meets-Meet-Suplattice :
(H : hom-Meet-Suplattice) →
preserves-meet
( meet-semilattice-Meet-Suplattice A)
( meet-semilattice-Meet-Suplattice B)
( map-hom-Meet-Suplattice H)
preserves-meets-Meet-Suplattice = pr1 ∘ preserves-meets-sups-Meet-Suplattice

preserves-sups-Meet-Suplattice :
(H : hom-Meet-Suplattice) →
preserves-sups
( suplattice-Meet-Suplattice A)
( suplattice-Meet-Suplattice B)
( map-hom-Meet-Suplattice H)
preserves-sups-Meet-Suplattice = pr2 ∘ preserves-meets-sups-Meet-Suplattice