Homomorphisms of frames

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

Created on 2022-10-18.
Last modified on 2023-06-10.

module order-theory.homomorphisms-frames where
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.frames
open import order-theory.homomorphisms-meet-semilattices
open import order-theory.homomorphisms-meet-sup-lattices
open import order-theory.homomorphisms-sup-lattices
open import order-theory.order-preserving-maps-posets


A frame homomorphism is an order preserving map between posets that additionally preserves binary meets and arbitrary joins.


module _
  {l1 l2 l3 l4 : Level} (A : Frame l1 l2) (B : Frame l3 l4)

  hom-Frame : UU (l1  lsuc l2  l3)
  hom-Frame = Σ (type-Frame A  type-Frame B)
     f  preserves-order-Poset (poset-Frame A) (poset-Frame B) f ×
        ( meet-suplattice-Frame A)
        ( meet-suplattice-Frame B)
        ( f))

  map-hom-Frame : hom-Frame  type-Frame A  type-Frame B
  map-hom-Frame = pr1

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

  preserves-meets-sups-hom-Frame :
    (H : hom-Frame) 
      ( meet-suplattice-Frame A)
      ( meet-suplattice-Frame B)
      ( map-hom-Frame H)
  preserves-meets-sups-hom-Frame = pr2  pr2

  preserves-meets-hom-Frame :
    (H : hom-Frame) 
      ( meet-semilattice-Frame A)
      ( meet-semilattice-Frame B)
      ( map-hom-Frame H)
  preserves-meets-hom-Frame = pr1  preserves-meets-sups-hom-Frame

  preserves-sups-hom-Frame :
    (H : hom-Frame) 
      ( suplattice-Frame A)
      ( suplattice-Frame B)
      ( map-hom-Frame H)
  preserves-sups-hom-Frame = pr2  preserves-meets-sups-hom-Frame

Recent changes