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
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.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
Idea
A frame homomorphism is an order preserving map between posets that additionally preserves binary meets and arbitrary joins.
Definitions
module _ {l1 l2 l3 l4 : Level} (A : Frame l1 l2) (B : Frame l3 l4) where 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 × preserves-meets-sups ( 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) → preserves-meets-sups ( 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) → preserves-meet ( 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) → preserves-sups ( suplattice-Frame A) ( suplattice-Frame B) ( map-hom-Frame H) preserves-sups-hom-Frame = pr2 ∘ preserves-meets-sups-hom-Frame
Recent changes
- 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 2023-05-07. Egbert Rijke. Cleaning up order theory some more (#599).
- 2023-05-05. Egbert Rijke. Cleaning up order theory 3 (#593).
- 2023-05-05. Egbert Rijke. cleaning up order theory (#591).
- 2023-05-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).