{-# OPTIONS --cubical-compatible --safe #-}
open import Algebra.Lattice
using (RawLattice; IsLattice; IsDistributiveLattice; isDistributiveLatticeʳʲᵐ)
open import Algebra.Lattice.Morphism.Structures using (IsLatticeMonomorphism)
module Algebra.Lattice.Morphism.LatticeMonomorphism
{a b ℓ₁ ℓ₂} {L₁ : RawLattice a ℓ₁} {L₂ : RawLattice b ℓ₂} {⟦_⟧}
(isLatticeMonomorphism : IsLatticeMonomorphism L₁ L₂ ⟦_⟧)
where
open import Algebra using (Absorptive; _Absorbs_; _DistributesOverʳ_)
import Algebra.Morphism.MagmaMonomorphism as MagmaMonomorphisms
import Algebra.Lattice.Properties.Lattice as LatticeProperties
open import Data.Product.Base using (_,_; map)
open import Relation.Binary.Bundles using (Setoid)
import Relation.Binary.Morphism.RelMonomorphism as RelMonomorphisms
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
open IsLatticeMonomorphism isLatticeMonomorphism
open RawLattice L₁ renaming (_≈_ to _≈₁_; _∨_ to _∨_; _∧_ to _∧_)
open RawLattice L₂ renaming (_≈_ to _≈₂_; _∨_ to _⊔_; _∧_ to _⊓_)
open MagmaMonomorphisms ∨-isMagmaMonomorphism public
using () renaming
( cong to ∨-cong
; assoc to ∨-assoc
; comm to ∨-comm
; idem to ∨-idem
; sel to ∨-sel
; cancelˡ to ∨-cancelˡ
; cancelʳ to ∨-cancelʳ
; cancel to ∨-cancel
)
open MagmaMonomorphisms ∧-isMagmaMonomorphism public
using () renaming
( cong to ∧-cong
; assoc to ∧-assoc
; comm to ∧-comm
; idem to ∧-idem
; sel to ∧-sel
; cancelˡ to ∧-cancelˡ
; cancelʳ to ∧-cancelʳ
; cancel to ∧-cancel
)
module _ (⊔-⊓-isLattice : IsLattice _≈₂_ _⊔_ _⊓_) where
open IsLattice ⊔-⊓-isLattice using (isEquivalence) renaming
( ∨-congˡ to ⊔-congˡ
; ∨-congʳ to ⊔-congʳ
; ∧-cong to ⊓-cong
; ∧-congˡ to ⊓-congˡ
; ∨-absorbs-∧ to ⊔-absorbs-⊓
; ∧-absorbs-∨ to ⊓-absorbs-⊔
)
setoid : Setoid b ℓ₂
setoid = record { isEquivalence = isEquivalence }
open ≈-Reasoning setoid
∨-absorbs-∧ : _Absorbs_ _≈₁_ _∨_ _∧_
∨-absorbs-∧ x y = injective (begin
$\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2625}{\htmlId{2654}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#1324}{\htmlId{2656}{\htmlClass{Function Operator}{\text{∨}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2625}{\htmlId{2658}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#1336}{\htmlId{2660}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2627}{\htmlId{2662}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ≈⟨ ∨-homo x (x ∧ y) ⟩
$\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2625}{\htmlId{2717}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊔ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2625}{\htmlId{2725}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#1336}{\htmlId{2727}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2627}{\htmlId{2729}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ≈⟨ ⊔-congˡ (∧-homo x y) ⟩
$\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2625}{\htmlId{2784}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊔ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2625}{\htmlId{2792}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊓ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2627}{\htmlId{2800}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ≈⟨ ⊔-absorbs-⊓ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2625}{\htmlId{2836}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2627}{\htmlId{2842}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⟩
$\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2625}{\htmlId{2854}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ∎)
∧-absorbs-∨ : _Absorbs_ _≈₁_ _∧_ _∨_
∧-absorbs-∨ x y = injective (begin
$\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2946}{\htmlId{2975}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#1336}{\htmlId{2977}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{2979}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2946}{\htmlId{2980}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#1324}{\htmlId{2982}{\htmlClass{Function Operator}{\text{∨}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2948}{\htmlId{2984}{\htmlClass{Bound}{\text{y}}}}\,\,\htmlId{2985}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ≈⟨ ∧-homo x (x ∨ y) ⟩
$\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2946}{\htmlId{3038}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊓ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2946}{\htmlId{3046}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#1324}{\htmlId{3048}{\htmlClass{Function Operator}{\text{∨}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2948}{\htmlId{3050}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ≈⟨ ⊓-congˡ (∨-homo x y) ⟩
$\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2946}{\htmlId{3105}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊓ ($\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2946}{\htmlId{3114}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊔ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2948}{\htmlId{3122}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$) ≈⟨ ⊓-absorbs-⊔ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2946}{\htmlId{3157}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2948}{\htmlId{3163}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⟩
$\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#2946}{\htmlId{3175}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ∎)
absorptive : Absorptive _≈₁_ _∨_ _∧_
absorptive = ∨-absorbs-∧ , ∧-absorbs-∨
distribʳ : _DistributesOverʳ_ _≈₂_ _⊔_ _⊓_ → _DistributesOverʳ_ _≈₁_ _∨_ _∧_
distribʳ distribʳ x y z = injective (begin
$\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3396}{\htmlId{3425}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#1336}{\htmlId{3427}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3398}{\htmlId{3429}{\htmlClass{Bound}{\text{z}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#1324}{\htmlId{3431}{\htmlClass{Function Operator}{\text{∨}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3394}{\htmlId{3433}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ ∨-homo (y ∧ z) x ⟩
$\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3396}{\htmlId{3488}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#1336}{\htmlId{3490}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3398}{\htmlId{3492}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ⊔ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3394}{\htmlId{3500}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ ⊔-congʳ (∧-homo y z) ⟩
$\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3396}{\htmlId{3555}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⊓ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3398}{\htmlId{3563}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ⊔ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3394}{\htmlId{3571}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ distribʳ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3394}{\htmlId{3604}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3396}{\htmlId{3610}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3398}{\htmlId{3616}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ⟩
($\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3396}{\htmlId{3629}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ⊔ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3394}{\htmlId{3637}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$) ⊓ ($\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3398}{\htmlId{3647}{\htmlClass{Bound}{\text{z}}}}\, \end{pmatrix}$ ⊔ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3394}{\htmlId{3655}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$) ≈⟨ ⊓-cong (∨-homo y x) (∨-homo z x) ⟨
$\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3396}{\htmlId{3707}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#1324}{\htmlId{3709}{\htmlClass{Function Operator}{\text{∨}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3394}{\htmlId{3711}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ⊓ $\begin{pmatrix} \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3398}{\htmlId{3719}{\htmlClass{Bound}{\text{z}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#1324}{\htmlId{3721}{\htmlClass{Function Operator}{\text{∨}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3394}{\htmlId{3723}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈⟨ ∧-homo (y ∨ x) (z ∨ x) ⟨
$\begin{pmatrix} \,\htmlId{3776}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3396}{\htmlId{3777}{\htmlClass{Bound}{\text{y}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#1324}{\htmlId{3779}{\htmlClass{Function Operator}{\text{∨}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3394}{\htmlId{3781}{\htmlClass{Bound}{\text{x}}}}\,\,\htmlId{3782}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#1336}{\htmlId{3784}{\htmlClass{Function Operator}{\text{∧}}}}\, \,\htmlId{3786}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3398}{\htmlId{3787}{\htmlClass{Bound}{\text{z}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#1324}{\htmlId{3789}{\htmlClass{Function Operator}{\text{∨}}}}\, \,\href{Algebra.Lattice.Morphism.LatticeMonomorphism.html#3394}{\htmlId{3791}{\htmlClass{Bound}{\text{x}}}}\,\,\htmlId{3792}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ∎)
isLattice : IsLattice _≈₂_ _⊔_ _⊓_ → IsLattice _≈₁_ _∨_ _∧_
isLattice isLattice = record
{ isEquivalence = RelMonomorphisms.isEquivalence isRelMonomorphism L.isEquivalence
; ∨-comm = ∨-comm LP.∨-isMagma L.∨-comm
; ∨-assoc = ∨-assoc LP.∨-isMagma L.∨-assoc
; ∨-cong = ∨-cong LP.∨-isMagma
; ∧-comm = ∧-comm LP.∧-isMagma L.∧-comm
; ∧-assoc = ∧-assoc LP.∧-isMagma L.∧-assoc
; ∧-cong = ∧-cong LP.∧-isMagma
; absorptive = absorptive isLattice
} where
module L = IsLattice isLattice
module LP = LatticeProperties (record { isLattice = isLattice })
isDistributiveLattice : IsDistributiveLattice _≈₂_ _⊔_ _⊓_ →
IsDistributiveLattice _≈₁_ _∨_ _∧_
isDistributiveLattice isDL = isDistributiveLatticeʳʲᵐ (record
{ isLattice = isLattice L.isLattice
; ∨-distribʳ-∧ = distribʳ L.isLattice L.∨-distribʳ-∧
}) where module L = IsDistributiveLattice isDL