agda-spa/Isomorphism.agda
Danila Fedorin 97a4165b58 Expose bundles from FiniteValueMap
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-03-01 21:35:40 -08:00

72 lines
4.2 KiB
Agda
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

module Isomorphism where
open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔_)
open import Function.Definitions using (Inverseˡ; Inverseʳ; 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 (¬_)
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ˡ : Inverseˡ _≈₁_ _≈₂_ f g) (inverseʳ : Inverseʳ _≈₁_ _≈₂_ 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
}