Compare commits

..

3 Commits

Author SHA1 Message Date
aafcb2683d Prove the transport of 'height lattice' property given an isomorphism
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-18 23:26:41 -08:00
8c9f39ac35 Add some additional 'equivalence' definitions to Equivalence
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-18 21:46:42 -08:00
6384f7006e Make 'lattice' public
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-18 20:18:38 -08:00
3 changed files with 77 additions and 6 deletions

View File

@ -4,8 +4,18 @@ open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
open import Relation.Binary.Definitions
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym)
record IsEquivalence {a} (A : Set a) (_≈_ : A A Set a) : Set a where
field
≈-refl : {a : A} a a
≈-sym : {a b : A} a b b a
≈-trans : {a b c : A} a b b c a c
module _ {a} (A : Set a) (_≈_ : A A Set a) where
IsReflexive : Set a
IsReflexive = {a : A} a a
IsSymmetric : Set a
IsSymmetric = {a b : A} a b b a
IsTransitive : Set a
IsTransitive = {a b c : A} a b b c a c
record IsEquivalence : Set a where
field
≈-refl : IsReflexive
≈-sym : IsSymmetric
≈-trans : IsTransitive

61
Isomorphism.agda Normal file
View File

@ -0,0 +1,61 @@
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₂)
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'))
}

View File

@ -20,7 +20,7 @@ IterProd k = iterate k (λ t → A × t) B
-- To make iteration more convenient, package the definitions in Lattice
-- records, perform the recursion, and unpackage.
private module _ where
module _ where
lattice : {k : } Lattice (IterProd k)
lattice {0} = record
{ _≈_ = _≈₂_