From aafcb2683d717d14b32c9e08e6356a992c2d526e Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 18 Feb 2024 23:26:41 -0800 Subject: [PATCH] Prove the transport of 'height lattice' property given an isomorphism Signed-off-by: Danila Fedorin --- Isomorphism.agda | 61 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 61 insertions(+) create mode 100644 Isomorphism.agda diff --git a/Isomorphism.agda b/Isomorphism.agda new file mode 100644 index 0000000..99a7efb --- /dev/null +++ b/Isomorphism.agda @@ -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')) + }