------------------------------------------------------------------------
-- The Agda standard library
--
-- The composition of morphisms between algebraic lattice structures.
------------------------------------------------------------------------
{-# OPTIONS --safe --cubical-compatible #-}
module Algebra.Lattice.Morphism.Construct.Composition where
open import Algebra.Lattice.Bundles using (RawLattice)
open import Algebra.Lattice.Morphism.Structures
using (IsLatticeHomomorphism; IsLatticeIsomorphism; IsLatticeMonomorphism)
open import Function.Base using (_∘_)
import Function.Construct.Composition as Func
open import Level using (Level)
open import Relation.Binary.Morphism.Construct.Composition
using (isRelHomomorphism)
open import Relation.Binary.Definitions using (Transitive)
private
variable
a b c ℓ₁ ℓ₂ ℓ₃ : Level
------------------------------------------------------------------------
-- Lattices
module _ {L₁ : RawLattice a ℓ₁}
{L₂ : RawLattice b ℓ₂}
{L₃ : RawLattice c ℓ₃}
(open RawLattice)
(≈₃-trans : Transitive (_≈_ L₃))
{f : Carrier L₁ → Carrier L₂}
{g : Carrier L₂ → Carrier L₃}
where
isLatticeHomomorphism
: IsLatticeHomomorphism L₁ L₂ f
→ IsLatticeHomomorphism L₂ L₃ g
→ IsLatticeHomomorphism L₁ L₃ (g ∘ f)
isLatticeHomomorphism f-homo g-homo = record
{ isRelHomomorphism = isRelHomomorphism F.isRelHomomorphism G.isRelHomomorphism
; ∧-homo = λ x y → ≈₃-trans (G.⟦⟧-cong (F.∧-homo x y)) (G.∧-homo (f x) (f y))
; ∨-homo = λ x y → ≈₃-trans (G.⟦⟧-cong (F.∨-homo x y)) (G.∨-homo (f x) (f y))
} where module F = IsLatticeHomomorphism f-homo; module G = IsLatticeHomomorphism g-homo
isLatticeMonomorphism
: IsLatticeMonomorphism L₁ L₂ f
→ IsLatticeMonomorphism L₂ L₃ g
→ IsLatticeMonomorphism L₁ L₃ (g ∘ f)
isLatticeMonomorphism f-mono g-mono = record
{ isLatticeHomomorphism = isLatticeHomomorphism F.isLatticeHomomorphism G.isLatticeHomomorphism
; injective = F.injective ∘ G.injective
} where module F = IsLatticeMonomorphism f-mono; module G = IsLatticeMonomorphism g-mono
isLatticeIsomorphism
: IsLatticeIsomorphism L₁ L₂ f
→ IsLatticeIsomorphism L₂ L₃ g
→ IsLatticeIsomorphism L₁ L₃ (g ∘ f)
isLatticeIsomorphism f-iso g-iso = record
{ isLatticeMonomorphism = isLatticeMonomorphism F.isLatticeMonomorphism G.isLatticeMonomorphism
; surjective = Func.surjective _ _ (_≈_ L₃) F.surjective G.surjective
} where module F = IsLatticeIsomorphism f-iso; module G = IsLatticeIsomorphism g-iso
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