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
Recent changes
- 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 2023-05-09. Egbert Rijke. Locales (#605).
- 2023-05-08. Egbert Rijke. Refactoring frames (#603).
- 2023-05-07. Egbert Rijke. Cleaning up order theory some more (#599).
- 2023-05-05. Egbert Rijke. Cleaning up order theory 3 (#593).