Skip to content

Commit

Permalink
Split mappings and subsets
Browse files Browse the repository at this point in the history
  • Loading branch information
@LuuBluum
LuuBluum committed Sep 8, 2024
1 parent 2b9762c commit f72ba2d
Show file tree
Hide file tree
Showing 4 changed files with 255 additions and 226 deletions.
4 changes: 2 additions & 2 deletions Cubical/Algebra/DistLattice/Downset.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ open import Cubical.Algebra.Lattice
open import Cubical.Algebra.DistLattice.Base

open import Cubical.Relation.Binary.Order.Poset
open import Cubical.Relation.Binary.Order.Poset.Mappings
open import Cubical.Relation.Binary.Order.Poset.Subset

open Iso

Expand Down Expand Up @@ -45,7 +45,7 @@ module DistLatticeDownset (L' : DistLattice ℓ) where
_ = LPoset .snd

↓ᴰᴸ : L → DistLattice ℓ
fst (↓ᴰᴸ u) = principalDownset IndPoset u .fst
fst (↓ᴰᴸ u) = ↓ u
DistLatticeStr.0l (snd (↓ᴰᴸ u)) = 0l , ∨lLid u
DistLatticeStr.1l (snd (↓ᴰᴸ u)) = u , is-refl u
DistLatticeStr._∨l_ (snd (↓ᴰᴸ u)) (v , v≤u) (w , w≤u) =
Expand Down
6 changes: 3 additions & 3 deletions Cubical/AlgebraicGeometry/ZariskiLattice/Properties.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ open import Cubical.Data.Nat using (ℕ)
open import Cubical.Data.Sigma.Properties
open import Cubical.Data.FinData
open import Cubical.Relation.Binary.Order.Poset
open import Cubical.Relation.Binary.Order.Poset.Mappings
open import Cubical.Relation.Binary.Order.Poset.Subset

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Localisation
Expand Down Expand Up @@ -136,7 +136,7 @@ module LocDownSetIso (R : CommRing ℓ) (f : R .fst) where
D R f ∧l D R r ∎


locDownSupp : R[1/ f ] → principalDownset ZLRPoset (D R f) .fst
locDownSupp : R[1/ f ] → ↓ (D R f)
locDownSupp =
SQ.rec
(isSetΣSndProp squash/ λ x → is-prop-valued x _)
Expand Down Expand Up @@ -188,7 +188,7 @@ module LocDownSetIso (R : CommRing ℓ) (f : R .fst) where
locToDownHom : DistLatticeHom (ZariskiLattice R[1/ f ]AsCommRing) (↓ᴰᴸ (D R f))
locToDownHom = ZLHasUniversalProp _ _ _ isSupportLocDownSupp .fst .fst

toDownSupp : R .fst → principalDownset ZLRPoset (D R f) .fst
toDownSupp : R .fst → ↓ (D R f)
toDownSupp = locDownSupp ∘ _/1

isSupportToDownSupp : IsSupport R (↓ᴰᴸ (D R f)) toDownSupp
Expand Down
222 changes: 1 addition & 221 deletions Cubical/Relation/Binary/Order/Poset/Mappings.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,13 +6,11 @@ open import Cubical.Foundations.Function
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Transport
open import Cubical.Foundations.Univalence

open import Cubical.Algebra.Semigroup

open import Cubical.Data.Sigma
open import Cubical.Data.Sum as ⊎

open import Cubical.Functions.Embedding
open import Cubical.Functions.Image
Expand All @@ -26,6 +24,7 @@ open import Cubical.HITs.SetQuotients

open import Cubical.Relation.Binary.Order.Poset.Base
open import Cubical.Relation.Binary.Order.Poset.Properties
open import Cubical.Relation.Binary.Order.Poset.Subset
open import Cubical.Relation.Binary.Order.Poset.Instances.Embedding
open import Cubical.Relation.Binary.Order.Proset
open import Cubical.Relation.Binary.Base
Expand Down Expand Up @@ -146,225 +145,6 @@ IsPosetEquiv→IsIsotone : (P S : Poset ℓ ℓ')
→ IsIsotone (snd P) (equivFun e) (snd S)
IsIsotone.pres≤ (IsPosetEquiv→IsIsotone P S e eq) x y = equivFun (IsPosetEquiv.pres≤ eq x y)

module _
(P : Poset ℓ ℓ')
where
private
_≤_ = PosetStr._≤_ (snd P)

is = PosetStr.isPoset (snd P)
prop = IsPoset.is-prop-valued is

rfl = IsPoset.is-refl is
anti = IsPoset.is-antisym is
trans = IsPoset.is-trans is

module _
(S : Embedding ⟨ P ⟩ ℓ'')
where
private
f = S .snd .fst
isDownset : Type (ℓ-max (ℓ-max ℓ ℓ') ℓ'')
isDownset = ∀ x → ∀ y → y ≤ f x → y ∈ₑ S

isPropIsDownset : isProp isDownset
isPropIsDownset = isPropΠ3 λ _ y _ → isProp∈ₑ y S

isUpset : Type (ℓ-max (ℓ-max ℓ ℓ') ℓ'')
isUpset = ∀ x → ∀ y → f x ≤ y → y ∈ₑ S

isPropIsUpset : isProp isUpset
isPropIsUpset = isPropΠ3 λ _ y _ → isProp∈ₑ y S

module _
(A : Embedding ⟨ P ⟩ ℓ₀)
(B : Embedding ⟨ P ⟩ ℓ₁)
where
module _
(downA : isDownset A)
(downB : isDownset B)
where
isDownset∩ : isDownset (A ∩ₑ B)
isDownset∩ (x , (a , a≡x) , (b , b≡x)) y y≤x
= (y , (downA a y (subst (y ≤_) (sym a≡x) y≤x) ,
downB b y (subst (y ≤_) (sym b≡x) y≤x))) , refl

isDownset∪ : isDownset (A ∪ₑ B)
isDownset∪ (x , A⊎B) y y≤x
= ∥₁.rec (isProp∈ₑ y (A ∪ₑ B))
(⊎.rec (λ { (a , a≡x) →
(y , ∣ inl (downA a y (subst (y ≤_)
(sym a≡x) y≤x)) ∣₁) , refl })
(λ { (b , b≡x) →
(y , ∣ inr (downB b y (subst (y ≤_)
(sym b≡x) y≤x)) ∣₁) , refl })) A⊎B

module _
(upA : isUpset A)
(upB : isUpset B)
where
isUpset∩ : isUpset (A ∩ₑ B)
isUpset∩ (x , (a , a≡x) , (b , b≡x)) y x≤y
= (y , (upA a y (subst (_≤ y) (sym a≡x) x≤y) ,
upB b y (subst (_≤ y) (sym b≡x) x≤y))) , refl

isUpset∪ : isUpset (A ∪ₑ B)
isUpset∪ (x , A⊎B) y x≤y
= ∥₁.rec (isProp∈ₑ y (A ∪ₑ B))
(⊎.rec (λ { (a , a≡x) →
(y , ∣ inl (upA a y (subst (_≤ y)
(sym a≡x) x≤y)) ∣₁) , refl })
(λ { (b , b≡x) →
(y , ∣ inr (upB b y (subst (_≤ y)
(sym b≡x) x≤y)) ∣₁) , refl })) A⊎B

module _
{I : Type ℓ''}
(S : I → Embedding ⟨ P ⟩ ℓ''')
where
module _
(downS : ∀ i → isDownset (S i))
where
isDownset⋂ : isDownset (⋂ₑ S)
isDownset⋂ (x , ∀x) y y≤x
= (y , λ i → downS i (∀x i .fst) y (subst (y ≤_) (sym (∀x i .snd)) y≤x)) , refl

isDownset⋃ : isDownset (⋃ₑ S)
isDownset⋃ (x , ∃i) y y≤x
= (y , (∥₁.map (λ { (i , a , a≡x) → i , downS i a y (subst (y ≤_) (sym a≡x) y≤x) }) ∃i)) , refl

module _
(upS : ∀ i → isUpset (S i))
where
isUpset⋂ : isUpset (⋂ₑ S)
isUpset⋂ (x , ∀x) y x≤y
= (y , λ i → upS i (∀x i .fst) y (subst (_≤ y) (sym (∀x i .snd)) x≤y)) , refl

isUpset⋃ : isUpset (⋃ₑ S)
isUpset⋃ (x , ∃i) y x≤y
= (y , (∥₁.map (λ { (i , a , a≡x) → i , upS i a y (subst (_≤ y) (sym a≡x) x≤y) }) ∃i)) , refl


module _
(x : ⟨ P ⟩)
where
principalDownset : Embedding ⟨ P ⟩ (ℓ-max ℓ ℓ')
principalDownset = (Σ[ y ∈ ⟨ P ⟩ ] y ≤ x) , EmbeddingΣProp λ _ → prop _ x

principalUpset : Embedding ⟨ P ⟩ (ℓ-max ℓ ℓ')
principalUpset = (Σ[ y ∈ ⟨ P ⟩ ] x ≤ y) , EmbeddingΣProp λ _ → prop x _

isDownsetPrincipalDownset : ∀ x → isDownset (principalDownset x)
isDownsetPrincipalDownset x (y , y≤x) z z≤y = (z , (trans z y x z≤y y≤x)) , refl

isUpsetPrincipalUpset : ∀ x → isUpset (principalUpset x)
isUpsetPrincipalUpset x (y , x≤y) z y≤z = (z , (trans x y z x≤y y≤z)) , refl

principalDownsetMembership : ∀ x y
→ x ≤ y
≃ x ∈ₑ principalDownset y
principalDownsetMembership x y
= propBiimpl→Equiv (prop x y)
(isProp∈ₑ x (principalDownset y))
(λ x≤y → (x , x≤y) , refl)
λ { ((a , a≤y) , fib) → subst (_≤ y) fib a≤y}

principalUpsetMembership : ∀ x y
→ x ≤ y
≃ y ∈ₑ principalUpset x
principalUpsetMembership x y
= propBiimpl→Equiv (prop x y)
(isProp∈ₑ y (principalUpset x))
(λ x≤y → (y , x≤y) , refl)
λ { ((a , x≤a) , fib) → subst (x ≤_) fib x≤a }

principalUpsetInclusion : ∀ x y
→ x ≤ y
→ principalUpset y ⊆ₑ principalUpset x
principalUpsetInclusion x y x≤y z z∈y↑
= equivFun (principalUpsetMembership x z)
(trans x y z x≤y (invEq (principalUpsetMembership y z) z∈y↑))

principalDownsetInclusion : ∀ x y
→ x ≤ y
→ principalDownset x ⊆ₑ principalDownset y
principalDownsetInclusion x y x≤y z z∈x↓
= equivFun (principalDownsetMembership z y)
(trans z x y (invEq (principalDownsetMembership z x) z∈x↓) x≤y)

module _
(S : Embedding ⟨ P ⟩ (ℓ-max ℓ ℓ'))
where
isPrincipalDownset : Type _
isPrincipalDownset = Σ[ x ∈ ⟨ P ⟩ ] S ≡ (principalDownset x)

isPropIsPrincipalDownset : isProp isPrincipalDownset
isPropIsPrincipalDownset (x , S≡x↓) (y , S≡y↓)
= Σ≡Prop (λ x → isSetEmbedding S (principalDownset x))
(anti x y x≤y y≤x)
where x≤y : x ≤ y
x≤y = invEq (principalDownsetMembership x y)
(subst (x ∈ₑ_)
(sym S≡x↓ ∙ S≡y↓)
(equivFun (principalDownsetMembership x x) (rfl x)))

y≤x : y ≤ x
y≤x = invEq (principalDownsetMembership y x)
(subst (y ∈ₑ_)
(sym S≡y↓ ∙ S≡x↓)
(equivFun (principalDownsetMembership y y) (rfl y)))

isPrincipalUpset : Type _
isPrincipalUpset = Σ[ x ∈ ⟨ P ⟩ ] S ≡ (principalUpset x)

isPropIsPrincipalUpset : isProp isPrincipalUpset
isPropIsPrincipalUpset (x , S≡x↑) (y , S≡y↑)
= Σ≡Prop (λ x → isSetEmbedding S (principalUpset x))
(anti x y x≤y y≤x)
where x≤y : x ≤ y
x≤y = invEq (principalUpsetMembership x y)
(subst (y ∈ₑ_)
(sym S≡y↑ ∙ S≡x↑)
(equivFun (principalUpsetMembership y y) (rfl y)))

y≤x : y ≤ x
y≤x = invEq (principalUpsetMembership y x)
(subst (x ∈ₑ_)
(sym S≡x↑ ∙ S≡y↑)
(equivFun (principalUpsetMembership x x) (rfl x)))

isPrincipalDownset→isDownset : isPrincipalDownset → (isDownset S)
isPrincipalDownset→isDownset (x , p) = transport⁻ (cong isDownset p) (isDownsetPrincipalDownset x)

isPrincipalUpset→isUpset : isPrincipalUpset → (isUpset S)
isPrincipalUpset→isUpset (x , p) = transport⁻ (cong isUpset p) (isUpsetPrincipalUpset x)

module PosetDownset (P' : Poset ℓ ℓ') where
private P = ⟨ P' ⟩
open PosetStr (snd P')

↓ᴾ : P → Poset (ℓ-max ℓ ℓ') ℓ'
fst (↓ᴾ u) = principalDownset P' u .fst
PosetStr._≤_ (snd (↓ᴾ u)) v w = v .fst ≤ w .fst
PosetStr.isPoset (snd (↓ᴾ u)) =
isPosetInduced
(PosetStr.isPoset (snd P'))
_
(principalDownset P' u .snd)

module PosetUpset (P' : Poset ℓ ℓ') where
private P = ⟨ P' ⟩
open PosetStr (snd P')

↑ᴾ : P → Poset (ℓ-max ℓ ℓ') ℓ'
fst (↑ᴾ u) = principalUpset P' u .fst
PosetStr._≤_ (snd (↑ᴾ u)) v w = v .fst ≤ w .fst
PosetStr.isPoset (snd (↑ᴾ u)) =
isPosetInduced
(PosetStr.isPoset (snd P'))
_
(principalUpset P' u .snd)

-- Isotone maps are characterized by their actions on down-sets and up-sets
module _
{P : Poset ℓ₀ ℓ₀'}
Expand Down
Loading

0 comments on commit f72ba2d

Please sign in to comment.