82 lines
4.7 KiB
Plaintext
82 lines
4.7 KiB
Plaintext
module Isomorphism where
|
||
|
||
open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
|
||
open import Function.Definitions using (Injective)
|
||
open import Lattice
|
||
open import Equivalence
|
||
open import Relation.Binary.Core using (_Preserves_⟶_ )
|
||
open import Data.Nat using (ℕ)
|
||
open import Data.Product using (_,_)
|
||
open import Relation.Nullary using (¬_)
|
||
|
||
IsInverseˡ : ∀ {a b} {A : Set a} {B : Set b}
|
||
(_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set b)
|
||
(f : A → B) (g : B → A) → Set b
|
||
IsInverseˡ {A = A} {B = B} _≈₁_ _≈₂_ f g = ∀ (x : B) → f (g x) ≈₂ x
|
||
|
||
IsInverseʳ : ∀ {a b} {A : Set a} {B : Set b}
|
||
(_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set b)
|
||
(f : A → B) (g : B → A) → Set a
|
||
IsInverseʳ {A = A} {B = B} _≈₁_ _≈₂_ f g = ∀ (x : A) → g (f x) ≈₁ x
|
||
|
||
module TransportFiniteHeight
|
||
{a b : Level} {A : Set a} {B : Set b}
|
||
{_≈₁_ : A → A → Set a} {_≈₂_ : B → B → Set b}
|
||
{_⊔₁_ : A → A → A} {_⊔₂_ : B → B → B}
|
||
{_⊓₁_ : A → A → A} {_⊓₂_ : B → B → B}
|
||
{height : ℕ}
|
||
(fhlA : IsFiniteHeightLattice A height _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_)
|
||
{f : A → B} {g : B → A}
|
||
(f-preserves-≈₁ : f Preserves _≈₁_ ⟶ _≈₂_) (g-preserves-≈₂ : g Preserves _≈₂_ ⟶ _≈₁_)
|
||
(f-⊔-distr : ∀ (a₁ a₂ : A) → f (a₁ ⊔₁ a₂) ≈₂ ((f a₁) ⊔₂ (f a₂)))
|
||
(g-⊔-distr : ∀ (b₁ b₂ : B) → g (b₁ ⊔₂ b₂) ≈₁ ((g b₁) ⊔₁ (g b₂)))
|
||
(inverseˡ : IsInverseˡ _≈₁_ _≈₂_ f g) (inverseʳ : IsInverseʳ _≈₁_ _≈₂_ f g) where
|
||
|
||
open IsFiniteHeightLattice fhlA using () renaming (_≺_ to _≺₁_; ≺-cong to ≺₁-cong; ≈-equiv to ≈₁-equiv)
|
||
open IsLattice lB using () renaming (_≺_ to _≺₂_; ≺-cong to ≺₂-cong; ≈-equiv to ≈₂-equiv)
|
||
|
||
open IsEquivalence ≈₁-equiv using () renaming (≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans)
|
||
open IsEquivalence ≈₂-equiv using () renaming (≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans)
|
||
|
||
open import Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong using () renaming (Chain to Chain₁; done to done₁; step to step₁)
|
||
open import Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong using () renaming (Chain to Chain₂; done to done₂; step to step₂)
|
||
|
||
private
|
||
f-Injective : Injective _≈₁_ _≈₂_ f
|
||
f-Injective {x} {y} fx≈fy = ≈₁-trans (≈₁-sym (inverseʳ x)) (≈₁-trans (g-preserves-≈₂ fx≈fy) (inverseʳ y))
|
||
|
||
g-Injective : Injective _≈₂_ _≈₁_ g
|
||
g-Injective {x} {y} gx≈gy = ≈₂-trans (≈₂-sym (inverseˡ x)) (≈₂-trans (f-preserves-≈₁ gx≈gy) (inverseˡ y))
|
||
|
||
f-preserves-̷≈ : f Preserves (λ x y → ¬ x ≈₁ y) ⟶ (λ x y → ¬ x ≈₂ y)
|
||
f-preserves-̷≈ x̷≈y = λ fx≈fy → x̷≈y (f-Injective fx≈fy)
|
||
|
||
g-preserves-̷≈ : g Preserves (λ x y → ¬ x ≈₂ y) ⟶ (λ x y → ¬ x ≈₁ y)
|
||
g-preserves-̷≈ x̷≈y = λ gx≈gy → x̷≈y (g-Injective gx≈gy)
|
||
|
||
portChain₁ : ∀ {a₁ a₂ : A} {h : ℕ} → Chain₁ a₁ a₂ h → Chain₂ (f a₁) (f a₂) h
|
||
portChain₁ (done₁ a₁≈a₂) = done₂ (f-preserves-≈₁ a₁≈a₂)
|
||
portChain₁ (step₁ {a₁} {a₂} (a₁≼a₂ , a₁̷≈a₂) a₂≈a₂' c) = step₂ (≈₂-trans (≈₂-sym (f-⊔-distr a₁ a₂)) (f-preserves-≈₁ a₁≼a₂) , f-preserves-̷≈ a₁̷≈a₂) (f-preserves-≈₁ a₂≈a₂') (portChain₁ c)
|
||
|
||
portChain₂ : ∀ {b₁ b₂ : B} {h : ℕ} → Chain₂ b₁ b₂ h → Chain₁ (g b₁) (g b₂) h
|
||
portChain₂ (done₂ a₂≈a₁) = done₁ (g-preserves-≈₂ a₂≈a₁)
|
||
portChain₂ (step₂ {b₁} {b₂} (b₁≼b₂ , b₁̷≈b₂) b₂≈b₂' c) = step₁ (≈₁-trans (≈₁-sym (g-⊔-distr b₁ b₂)) (g-preserves-≈₂ b₁≼b₂) , g-preserves-̷≈ b₁̷≈b₂) (g-preserves-≈₂ b₂≈b₂') (portChain₂ c)
|
||
|
||
isFiniteHeightLattice : IsFiniteHeightLattice B height _≈₂_ _⊔₂_ _⊓₂_
|
||
isFiniteHeightLattice =
|
||
let
|
||
(((a₁ , a₂) , c) , bounded₁) = IsFiniteHeightLattice.fixedHeight fhlA
|
||
in record
|
||
{ isLattice = lB
|
||
; fixedHeight = (((f a₁ , f a₂), portChain₁ c) , λ c' → bounded₁ (portChain₂ c'))
|
||
}
|
||
|
||
finiteHeightLattice : FiniteHeightLattice B
|
||
finiteHeightLattice = record
|
||
{ height = height
|
||
; _≈_ = _≈₂_
|
||
; _⊔_ = _⊔₂_
|
||
; _⊓_ = _⊓₂_
|
||
; isFiniteHeightLattice = isFiniteHeightLattice
|
||
}
|