FLRP.Parachute.Representation¶
Reading a parachute representation¶
This is the FLRP.Parachute.Representation module of the Agda Universal Algebra Library.
FLRP.Parachute proves that core-freeness propagates in a group whose interval
[H , G] has the shape of a parachute (ParachuteConfig). This
module supplies the shape: from an isomorphism between [H , G] and the parachute
lattice 𝒫(L₁ , … , Lₙ) of Classical.Structures.Lattice.Parachute it reads off
- the configuration itself (
config) — the atoms and their meet, join, and covering properties; - for each
i, an isomorphism[Kᵢ , G] ≅ Lᵢ(canopyIso) — the sense in whichLᵢis a canopy of the representation, and the step that lets a property core-free enforceable byLᵢspeak aboutG; - the translation of "
|Lᵢ| > 2" into theBigCanopydatum the propagation theorem consumes (bigCanopy).
Everything here is transport along an order isomorphism, so the module opens with the small toolkit that makes such transport routine: an order isomorphism preserves and reflects the order, and preserves equality.
Transport along an interval isomorphism¶
An IntervalIso is an order isomorphism, so it preserves equality
(two elements comparable both ways map to comparable images) and reflects the
order (transport back and repair the round trip). Both directions are needed
below, because the parachute's structure is stated in the lattice and consumed in
the interval.
module IntervalIsoTools (𝒢 : Group 0ℓ 0ℓ) (H : Pred 𝕌[ proj₁ 𝒢 ] 0ℓ) (H-sg : IsSubgroup 𝒢 H) (𝓛 : Lattice) (iso : IntervalIso 𝒢 H H-sg 𝓛) where open UpperInterval 𝒢 H H-sg open GroupParachute 𝒢 H H-sg using ( IsAll ; Hᵢ ; Gᵢ ; ⊇→IsAll ) open OrderIso iso open Lattice-Order 𝓛 using ( _≤_ ; ≤-trans ; ≤-antisym ; ≤-reflexive ) open Setoid 𝔻[ 𝓛 .proj₁ ] using () renaming ( Carrier to L ; _≈_ to _≈ᴸ_ ; sym to ≈ᴸ-sym ) -- Monotonicity with the endpoints explicit. Neither `to`, `from`, nor `set` -- is injective, so an implicit endpoint under any of them is never inferred; -- every consumer below passes them. to-mono′ : (M N : Interval≈) → M ≤ᵢ N → to M ≤ to N to-mono′ M N le = to-mono {M} {N} le from-mono′ : (u v : L) → u ≤ v → from u ≤ᵢ from v from-mono′ u v le = from-mono {u} {v} le -- An order isomorphism preserves equality ... to-≈ : (M N : Interval≈) → M ≈ᵢ N → to M ≈ᴸ to N to-≈ M N (M⊆N , N⊆M) = ≤-antisym (to-mono′ M N M⊆N) (to-mono′ N M N⊆M) from-≈ : (u v : L) → u ≈ᴸ v → from u ≈ᵢ from v from-≈ u v e = from-mono′ u v (≤-reflexive e) , from-mono′ v u (≤-reflexive (≈ᴸ-sym e)) -- ... and reflects the order: transport back and repair both round trips. reflect : (M N : Interval≈) → to M ≤ to N → M ≤ᵢ N reflect M N le z = proj₁ (from∘to N) (from-mono′ (to M) (to N) le (proj₂ (from∘to M) z)) -- The two ends of the interval, transported. A member whose image is below a -- bottom of `𝑳` collapses to `H`; a member whose image is above a top is all -- of `G`. module Ends ((⊥ᴸ , ⊥ᴸmin) : BottomOf 𝓛) ((⊤ᴸ , ⊤ᴸmax) : TopOf 𝓛) where -- The image of the interval's top is a top of `𝑳`, and dually at the bottom. top-≤ : ⊤ᴸ ≤ to Gᵢ top-≤ = ≤-trans (≤-reflexive (≈ᴸ-sym (to∘from ⊤ᴸ))) (to-mono′ (from ⊤ᴸ) Gᵢ (λ _ → lift tt)) ≤-bot : to Hᵢ ≤ ⊥ᴸ ≤-bot = ≤-trans (to-mono′ Hᵢ (from ⊥ᴸ) (above (from ⊥ᴸ))) (≤-reflexive (to∘from ⊥ᴸ)) below-bot : (M : Interval≈) → to M ≤ ⊥ᴸ → set M ⊆ H below-bot M le = reflect M Hᵢ (≤-trans le (⊥ᴸmin (to Hᵢ))) above-top : (C : Interval≈) → ⊤ᴸ ≤ to C → IsAll C above-top C le = ⊇→IsAll C (reflect Gᵢ C (≤-trans (⊤ᴸmax (to Gᵢ)) le))
Composing with a lattice isomorphism¶
An interval isomorphism composes on the right with an isomorphism of lattices, so
group representability transports along lattice isomorphisms. (Its mirror,
composition on the interval side, is compose-IntervalIso of
FLRP.Enforceable.)
-- An isomorphism of (the meet orders of) two lattices. LatticeIso : Lattice → Lattice → Type 0ℓ LatticeIso 𝓜@(𝑴 , _) 𝓛@(𝑳 , _) = OrderIso (Setoid._≈_ 𝔻[ 𝑴 ]) (Lattice-Order._≤_ 𝓜) (Setoid._≈_ 𝔻[ 𝑳 ]) (Lattice-Order._≤_ 𝓛) compose-IntervalIsoʳ : (𝒢 : Group 0ℓ 0ℓ) (H : Pred 𝕌[ proj₁ 𝒢 ] 0ℓ) (H-sg : IsSubgroup 𝒢 H) (𝓜 𝓛 : Lattice) → IntervalIso 𝒢 H H-sg 𝓜 → LatticeIso 𝓜 𝓛 → IntervalIso 𝒢 H H-sg 𝓛 compose-IntervalIsoʳ 𝒢 H H-sg 𝓜@(𝑴 , _) 𝓛@(𝑳 , _) I J = record { to = λ m → J.to (I.to m) ; from = λ u → I.from (J.from u) ; to-mono = λ le → J.to-mono (I.to-mono le) ; from-mono = λ le → I.from-mono (J.from-mono le) ; to∘from = λ u → ≈ᴸ-trans (to-≈ᴶ (I.to∘from (J.from u))) (J.to∘from u) ; from∘to = λ m → ≈ᵢ-trans { I.from (J.from (J.to (I.to m))) } { I.from (I.to m) } { m } (from-≈ᴵ (J.from∘to (I.to m))) (I.from∘to m) } where module I = OrderIso I module J = OrderIso J open GroupParachute 𝒢 H H-sg using ( ≈ᵢ-trans ) open Lattice-Order 𝓜 renaming ( ≤-reflexive to ≤ᴹ-reflexive ) using () open Lattice-Order 𝓛 renaming ( ≤-antisym to ≤ᴸ-antisym ) using () open Setoid 𝔻[ 𝑴 ] renaming ( sym to ≈ᴹ-sym ; Carrier to M ; _≈_ to _≈ᴹ_ ) using () open Setoid 𝔻[ 𝑳 ] renaming ( trans to ≈ᴸ-trans ; Carrier to L ; _≈_ to _≈ᴸ_ ) using () to-≈ᴶ : {x y : M} → x ≈ᴹ y → J.to x ≈ᴸ J.to y to-≈ᴶ e = ≤ᴸ-antisym (J.to-mono (≤ᴹ-reflexive e)) (J.to-mono (≤ᴹ-reflexive (≈ᴹ-sym e))) from-≈ᴵ : {x y : M} → x ≈ᴹ y → UpperInterval._≈ᵢ_ 𝒢 H H-sg (I.from x) (I.from y) from-≈ᴵ e = I.from-mono (≤ᴹ-reflexive e) , I.from-mono (≤ᴹ-reflexive (≈ᴹ-sym e))
The configuration of a parachute representation¶
Fix a family of canopies with their extrema and the decision procedure the parachute construction needs, and a group representation of the resulting parachute lattice.
open Setoid module ParachuteRep {m : ℕ} (𝑳s : Fin (suc m) → Lattice) (𝒕 : ∀ i → TopOf (𝑳s i)) (top? : ∀ i (x : 𝕌[ 𝑳s i .proj₁ ]) → Dec (𝔻[ 𝑳s i .proj₁ ] ._≈_ x (𝒕 i .proj₁))) (𝒃 : ∀ i → BottomOf (𝑳s i)) (nondeg : ∀ i → ¬ 𝔻[ 𝑳s i .proj₁ ] ._≈_ (𝒃 i .proj₁) (𝒕 i .proj₁)) where open LatticeParachute 𝑳s 𝒕 top? 𝒃 nondeg public -- "|Lᵢ| > 2": the i-th canopy has an element strictly between its two ends. record BigCanopyᴸ (i : Fin (suc m)) : Type 0ℓ where field elt : 𝕌[ 𝑳s i .proj₁ ] elt-not-bot : ¬ [ i ] elt ≤ bot i elt-not-top : NonTop i elt module Over (𝒢 : Group 0ℓ 0ℓ) (H : Pred 𝕌[ 𝒢 .proj₁ ] 0ℓ) (H-sg : IsSubgroup 𝒢 H) (iso : IntervalIso 𝒢 H H-sg ⊕ᵖ-Lattice) where open UpperInterval 𝒢 H H-sg open GroupParachute 𝒢 H H-sg open IntervalIsoTools 𝒢 H H-sg ⊕ᵖ-Lattice iso open Ends ⊥ᵖ-isBottom ⊤ᵖ-isTop open OrderIso iso using ( to ; from ; to∘from ; from∘to ) open Lattice-Order ⊕ᵖ-Lattice renaming ( _≤_ to _≤ᴸ_ ; ≤-trans to ≤ᴸ-trans ; ≤-respˡ-≈ to ≤ᴸ-respˡ-≈ ; ≤-respʳ-≈ to ≤ᴸ-respʳ-≈ ; ∧-greatest to ∧ᴸ-greatest ; ∨-least to ∨ᴸ-least ) using ()
The i-th atom of the representation is the subgroup corresponding to the i-th
atom of the parachute, and its image is that atom back again.
-- The subgroup Kᵢ at the bottom of the i-th canopy. K : Fin (suc m) → Interval≈ K i = from (atom i) K-image : (i : Fin (suc m)) → atom i ≈ᵖ to (K i) K-image i = ≈ᵖ-sym (to∘from (atom i))
The three fields of the configuration, in turn.
Distinct atoms meet at the bottom: their intersection maps below atom i ∧ atom j,
which is the parachute's bottom. They join to the top: a member containing both maps
above atom i ∨ atom j, which is the parachute's top. And the covering property is
the parachute's own, transported.
atoms-meet′ : (i j : Fin (suc m)) → ¬ i ≡ j → set (K i) ∩ set (K j) ⊆ H atoms-meet′ i j i≢j = below-bot (K i ∧ᵢ K j) meet-below where meet-below : to (K i ∧ᵢ K j) ≤ᴸ ⊥ᵖ meet-below = ≤ᴸ-trans ( ∧ᴸ-greatest ( ≤ᴸ-respʳ-≈ (≈ᵖ-sym (K-image i)) (to-mono′ (K i ∧ᵢ K j) (K i) proj₁) ) ( ≤ᴸ-respʳ-≈ (≈ᵖ-sym (K-image j)) (to-mono′ (K i ∧ᵢ K j) (K j) proj₂) ) ) ( ≤ᵖ-sound (atoms-meet i j i≢j) ) atoms-join′ : (i j : Fin (suc m)) → ¬ i ≡ j → (C : Interval≈) → set (K i) ⊆ set C → set (K j) ⊆ set C → IsAll C atoms-join′ i j i≢j C Ki⊆C Kj⊆C = above-top C ( ≤ᴸ-trans ( ≤ᵖ-sound (atoms-join i j i≢j) ) ( ∨ᴸ-least ( ≤ᴸ-respˡ-≈ (≈ᵖ-sym (K-image i)) (to-mono′ (K i) C Ki⊆C)) ( ≤ᴸ-respˡ-≈ (≈ᵖ-sym (K-image j)) (to-mono′ (K j) C Kj⊆C)) ) ) covered′ : (M : Interval≈) → (set M ⊆ H) ⊎ Σ[ i ∈ Fin (suc m) ] (set (K i) ⊆ set M) covered′ M with covered (to M) ... | inj₁ below = inj₁ (below-bot M (≤ᵖ-sound below)) ... | inj₂ (i , le) = inj₂ (i , λ z → proj₁ (from∘to M) (from-mono′ (atom i) (to M) (≤ᵖ-sound le) z)) -- The parachute shape of [H , G], as the propagation theorem consumes it. config : ParachuteConfig (suc m) config = record { atom = K ; atoms-meet = atoms-meet′ ; atoms-join = atoms-join′ ; covered = covered′ } -- No atom subgroup collapses to `H` — the atoms of the parachute are not its -- bottom — so an atom is proper as soon as there is a second one to meet it. K-⊄H : (i : Fin (suc m)) → ¬ set (K i) ⊆ H K-⊄H i sub = atom-≢⊥ i (≤ᵖ-complete (≤ᴸ-respˡ-≈ (≈ᵖ-sym (K-image i)) (≤ᴸ-trans (to-mono′ (K i) Hᵢ sub) ≤-bot))) K-proper : (i j : Fin (suc m)) → ¬ i ≡ j → Proper (K i) K-proper i j i≢j all = K-⊄H j (λ {x} z → atoms-meet′ i j i≢j (all x , z)) -- Properness is decidable in a parachute: a member is everything exactly when -- its image is the parachute's top, and being the top is decidable there. -- (This is the datum Lemma 3.7 of [FLRP.Parachute][] needs.) IsAll? : (M : Interval≈) → Dec (IsAll M) IsAll? M with ⊤ᵖ≤? (to M) ... | yes le = yes (above-top M (≤ᵖ-sound le)) ... | no ¬le = no (λ all → ¬le (≤ᵖ-complete (≤ᴸ-trans top-≤ (to-mono′ Gᵢ M (λ {x} _ → all x)))))
The canopies are represented¶
[Kᵢ , G] ≅ Lᵢ. The maps are the parachute's own canopy retraction π i and its
section ↑ i (Classical.Structures.Lattice.Parachute), conjugated by the
interval isomorphism. The only bookkeeping is that a member of [Kᵢ , G] is also
a member of [H , G] (widen), since H ⊆ Kᵢ.
module Canopy (i : Fin (suc m)) where Kᵢ-sg : IsSubgroup 𝒢 (set (K i)) Kᵢ-sg = element-isSubgroup (K i) -- private module IK = UpperInterval 𝒢 (set (K i)) Kᵢ-sg open UpperInterval 𝒢 (set (K i)) Kᵢ-sg using () renaming ( Interval≈ to Interval≈ᴷ ; set to setᴷ ; mk to mkᴷ ; above to aboveᴷ ; _≈ᵢ_ to _≈ᵢᴷ_ ; _≤ᵢ_ to _≤ᵢᴷ_ ; element-isSubgroup to element-isSubgroupᴷ ) -- A subgroup above Kᵢ is a subgroup above H. widen : Interval≈ᴷ → Interval≈ widen M = mk (setᴷ M) (element-isSubgroupᴷ M) (aboveᴷ M ∘ above (K i)) -- The i-th canopy coordinate of a member of [Kᵢ , G] ... toᶜ : Interval≈ᴷ → 𝕌[ 𝑳s i .proj₁ ] toᶜ M = π i (to (widen M)) -- ... and the member of [Kᵢ , G] a canopy element names. fromᶜ : 𝕌[ 𝑳s i .proj₁ ] → Interval≈ᴷ fromᶜ x = mkᴷ (set (from (↑ i x))) (element-isSubgroup (from (↑ i x))) (from-mono′ (atom i) (↑ i x) (≤ᵖ-sound (atom-≤-↑ i x))) toᶜ-mono : (M N : Interval≈ᴷ) → M ≤ᵢᴷ N → [ i ] toᶜ M ≤ toᶜ N toᶜ-mono M N le = π-mono i (≤ᵖ-complete (to-mono′ (widen M) (widen N) le)) fromᶜ-mono : (x y : 𝕌[ 𝑳s i .proj₁ ]) → [ i ] x ≤ y → fromᶜ x ≤ᵢᴷ fromᶜ y fromᶜ-mono x y e = from-mono′ (↑ i x) (↑ i y) (≤ᵖ-sound (↑-mono i e)) -- Round trip through the canopy: π i undoes ↑ i. toᶜ∘fromᶜ : (x : 𝕌[ 𝑳s i .proj₁ ]) → [ i ] toᶜ (fromᶜ x) ≈ x toᶜ∘fromᶜ x = ≈trans i (π-cong i step) (π∘↑ i x) where step : to (widen (fromᶜ x)) ≈ᵖ ↑ i x step = ≈ᵖ-trans (to-≈ (widen (fromᶜ x))(from (↑ i x)) (id , id)) (to∘from (↑ i x)) -- Round trip through the interval: ↑ i undoes π i above the i-th atom. fromᶜ∘toᶜ : (M : Interval≈ᴷ) → fromᶜ (toᶜ M) ≈ᵢᴷ M fromᶜ∘toᶜ M = round where atom≤ : atom i ≤ᵖ to (widen M) atom≤ = ≤ᵖ-complete (≤ᴸ-respˡ-≈ (≈ᵖ-sym (K-image i)) (to-mono′ (K i) (widen M) (λ z → aboveᴷ M z))) round : from (↑ i (π i (to (widen M)))) ≈ᵢ widen M round = ≈ᵢ-trans { from (↑ i (π i (to (widen M)))) } { from (to (widen M)) } { widen M } (from-≈ (↑ i (π i (to (widen M)))) (to (widen M)) (↑∘π i (to (widen M)) atom≤)) (from∘to (widen M)) -- The canopy isomorphism [Kᵢ , G] ≅ Lᵢ. canopy-iso : IntervalIso 𝒢 (set (K i)) Kᵢ-sg (𝑳s i) canopy-iso = record { to = toᶜ ; from = fromᶜ ; to-mono = λ {M} {N} le → toᶜ-mono M N le ; from-mono = λ {x} {y} e → fromᶜ-mono x y e ; to∘from = toᶜ∘fromᶜ ; from∘to = fromᶜ∘toᶜ } canopyIso : (i : Fin (suc m)) → IntervalIso 𝒢 (set (K i)) (element-isSubgroup (K i)) (𝑳s i) canopyIso i = Canopy.canopy-iso i
Big canopies¶
"|Lᵢ| > 2" says Lᵢ has an element strictly between its bottom and its top.
Such an element names a member of [Kᵢ , G] strictly between Kᵢ and G, which
is precisely the BigCanopy datum of FLRP.Parachute.
bigCanopy : (i : Fin (suc m)) → BigCanopyᴸ i → BigCanopy (K i) bigCanopy i big = record { mid = from (↑ i elt) ; atom-⊆-mid = from-mono′ (atom i) (↑ i elt) (≤ᵖ-sound (atom-≤-↑ i elt)) ; mid-⊄-atom = not-below ; mid-proper = not-all } where open BigCanopyᴸ big -- The canopy coordinate of the member named by `elt` is `elt` again ... coordinate : [ i ] π i (to (from (↑ i elt))) ≈ elt coordinate = ≈trans i (π-cong i (to∘from (↑ i elt))) (π∘↑ i elt) -- ... and the canopy coordinate of the atom is the canopy's bottom. atom-coordinate : [ i ] π i (to (K i)) ≈ bot i atom-coordinate = ≈trans i (π-cong i (≈ᵖ-sym (K-image i))) (π-atom i) -- Were the middle element below the atom, its canopy coordinate would be -- below the canopy's bottom. not-below : ¬ (set (from (↑ i elt)) ⊆ set (K i)) not-below sub = elt-not-bot (≤trans i (≤reflexive i (≈sym i coordinate)) (≤trans i (π-mono i (≤ᵖ-complete (to-mono′ (from (↑ i elt)) (K i) sub))) (≤reflexive i atom-coordinate))) -- Were it everything, its canopy coordinate would be the canopy's top. not-all : Proper (from (↑ i elt)) not-all all = elt-not-top (≤antisym i (≤top i elt) (≤trans i (π-mono i (≤ᵖ-complete (≤ᴸ-trans top-≤ (to-mono′ Gᵢ (from (↑ i elt)) (λ {x} _ → all x))))) (≤reflexive i coordinate)))
The three outputs of this module — config, canopyIso,
and bigCanopy — are exactly the inputs of the parachute theorems
of FLRP.Parachute.Theorems.