------------------------------------------------------------------------
-- The Agda standard library
--
-- Morphisms between algebraic lattice structures
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Algebra.Lattice.Morphism.Structures where
open import Algebra.Core using (Op₂)
open import Algebra.Morphism using (module MagmaMorphisms)
open import Algebra.Lattice.Bundles using (RawLattice)
import Algebra.Morphism.Definitions as MorphismDefinitions
open import Level using (Level; _⊔_)
open import Function.Definitions using (Injective; Surjective)
open import Relation.Binary.Morphism.Structures using (IsRelHomomorphism)
open import Relation.Binary.Core using (Rel)
private
variable
a b ℓ₁ ℓ₂ : Level
------------------------------------------------------------------------
-- Morphisms over lattice-like structures
------------------------------------------------------------------------
module LatticeMorphisms (L₁ : RawLattice a ℓ₁) (L₂ : RawLattice b ℓ₂) where
open RawLattice L₁ renaming
( Carrier to A; _≈_ to _≈₁_
; _∧_ to _∧₁_; _∨_ to _∨₁_
; ∧-rawMagma to ∧-rawMagma₁
; ∨-rawMagma to ∨-rawMagma₁)
open RawLattice L₂ renaming
( Carrier to B; _≈_ to _≈₂_
; _∧_ to _∧₂_; _∨_ to _∨₂_
; ∧-rawMagma to ∧-rawMagma₂
; ∨-rawMagma to ∨-rawMagma₂)
module ∨ = MagmaMorphisms ∨-rawMagma₁ ∨-rawMagma₂
module ∧ = MagmaMorphisms ∧-rawMagma₁ ∧-rawMagma₂
open MorphismDefinitions A B _≈₂_
record IsLatticeHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧
∧-homo : Homomorphic₂ ⟦_⟧ _∧₁_ _∧₂_
∨-homo : Homomorphic₂ ⟦_⟧ _∨₁_ _∨₂_
open IsRelHomomorphism isRelHomomorphism public
renaming (cong to ⟦⟧-cong)
∧-isMagmaHomomorphism : ∧.IsMagmaHomomorphism ⟦_⟧
∧-isMagmaHomomorphism = record
{ isRelHomomorphism = isRelHomomorphism
; homo = ∧-homo
}
∨-isMagmaHomomorphism : ∨.IsMagmaHomomorphism ⟦_⟧
∨-isMagmaHomomorphism = record
{ isRelHomomorphism = isRelHomomorphism
; homo = ∨-homo
}
record IsLatticeMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
isLatticeHomomorphism : IsLatticeHomomorphism ⟦_⟧
injective : Injective _≈₁_ _≈₂_ ⟦_⟧
open IsLatticeHomomorphism isLatticeHomomorphism public
∨-isMagmaMonomorphism : ∨.IsMagmaMonomorphism ⟦_⟧
∨-isMagmaMonomorphism = record
{ isMagmaHomomorphism = ∨-isMagmaHomomorphism
; injective = injective
}
∧-isMagmaMonomorphism : ∧.IsMagmaMonomorphism ⟦_⟧
∧-isMagmaMonomorphism = record
{ isMagmaHomomorphism = ∧-isMagmaHomomorphism
; injective = injective
}
open ∧.IsMagmaMonomorphism ∧-isMagmaMonomorphism public
using (isRelMonomorphism)
record IsLatticeIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
field
isLatticeMonomorphism : IsLatticeMonomorphism ⟦_⟧
surjective : Surjective _≈₁_ _≈₂_ ⟦_⟧
open IsLatticeMonomorphism isLatticeMonomorphism public
∨-isMagmaIsomorphism : ∨.IsMagmaIsomorphism ⟦_⟧
∨-isMagmaIsomorphism = record
{ isMagmaMonomorphism = ∨-isMagmaMonomorphism
; surjective = surjective
}
∧-isMagmaIsomorphism : ∧.IsMagmaIsomorphism ⟦_⟧
∧-isMagmaIsomorphism = record
{ isMagmaMonomorphism = ∧-isMagmaMonomorphism
; surjective = surjective
}
open ∧.IsMagmaIsomorphism ∧-isMagmaIsomorphism public
using (isRelIsomorphism)
------------------------------------------------------------------------
-- Re-export contents of modules publicly
open LatticeMorphisms public
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4