FLRP.Bridge¶
The Pálfy–Pudlák bridge (easy direction)¶
This is the FLRP.Bridge module of the Agda Universal Algebra Library.
For a group G and a subgroup H, the congruence lattice of
the transitive coset G-set G ↷ G/H is order-isomorphic to the interval [H , G]
in the subgroup lattice Sub G.
This module formalizes the easy (constructive) direction of the Pálfy–Pudlák correspondence.1
The correspondence has two mutually inverse, order-preserving maps.
-
θ ↦ K_θ(to). A congruenceθof the coset algebra — aG-invariant equivalence on cosets — maps to the subgroupK_θ = { g ∈ G : H·ε ∼_θ H·g }, theθ-class of the base coset viewed as a predicate on the carrier. We proveK_θis an equality-respecting subgroup containingH, i.e. an element of the respecting interval[H , G]. -
K ↦ θ_K(from). A subgroupKwithH ≤ K ≤ Gmaps to the relationθ_Kon cosets defined byH·x θ_K H·y ⟺ x ⁻¹ ∙ y ∈ K— which is exactly the coset relation ofKfrom Classical.Structures.Group.Cosets. We prove it is a congruence of the coset algebra (an equivalence, reflexive over∼_H, compatible with every unary translate).
The two maps are mutually inverse and monotone, giving the order isomorphism
bridge.
On the interval side we use the respecting UpperInterval of
FLRP.Enforceable, not the bare SubInterval.
This honors the WP-4 finding: the round trip to (from M) ≈ M moves
membership across the setoid equality ε ⁻¹ ∙ g ≈ g, which is sound only because
interval elements carry a Respects proof.
Over a redundant presentation the bare interval can be strictly larger than the respecting one, so the isomorphism is false at the bare level (see the counterexample in FLRP.Enforceable).
The core isomorphism bridge is the Layer S formulation: it relates
the semantic congruence lattice Con to the interval, proved
constructively with no classical or deferred hypotheses.
The Layer D statement required by issue #454 is proved here as well — directly,
not through the classical cross-layer bridge.2 The pivot is that both maps carry
their decision procedures with them: K_θ is the θ-class of the base coset, decided
by θ's own decision procedure at the pair (ε , g), and θ_K is the coset relation
of K, decided by one group multiplication once membership in K is
decidable. So the correspondence restricts to an order isomorphism
bridgeᵈ between the decidable congruence poset DecCon (𝒢 ↷ 𝒢/H) and
the decidably presented interval [H , 𝒢] (Intervalᵈ of
FLRP.Enforceable), with no classical assumption — the congruence-completeness
bridge of FLRP.Assumptions is not consumed.
The module ends with the corollaries: a finite coset algebra realizes the decidable
interval as its decidable congruence poset, and every group-representable lattice is
decidably representable (GroupRepresentable→Representableᵈ).
The bridge module¶
The development is parameterized by a group 𝒢 at level 0ℓ
and an equality-respecting subgroup H, matching the level discipline of
FLRP.Problem and FLRP.Enforceable (0ℓ suffices for every finite
instance and keeps the interval side lined up with UpperInterval).
module Bridge (𝒢 : Group 0ℓ 0ℓ) (H : Pred 𝕌[ proj₁ 𝒢 ] 0ℓ) (H-sg : IsSubgroup 𝒢 H) where 𝑮 : Algebra 0ℓ 0ℓ 𝑮 = proj₁ 𝒢 G : Type 0ℓ G = 𝕌[ 𝑮 ] open Setoid 𝔻[ 𝑮 ] renaming ( refl to ≈refl ; sym to ≈sym ; trans to ≈trans ) using ( _≈_ ) open Group-Op 𝒢 using ( _∙_ ; ε ; _⁻¹ ; ∙-cong ; idˡ-law ; idʳ-law ; invˡ-law ) open GroupProperties ⟨ 𝒢 ⟩ᵍᵖ using ( ε⁻¹≈ε ; \\-leftDividesˡ ) open IsSubgroup H-sg using ( respects ) open Coset 𝒢 H H-sg using ( _∼_ ; ≈⇒∼ ; ∼-dec ) open CosetAction 𝒢 H H-sg using ( cosetAlgebra ; cosetAlgebra-FiniteAlgebra ) open UpperInterval 𝒢 H H-sg
Elementary facts about a congruence of the coset algebra¶
The coset algebra's setoid equality is the coset relation _∼_ of
H (that is _≈_ of 𝔻[ cosetAlgebra ]), so a
congruence θ is reflexive over _∼_, and — being an
equivalence compatible with every operation symbol g — it is symmetric,
transitive, and invariant under left translation x ↦ g ∙ x (the
action). These four facts are the only structure of θ the
correspondence consumes.
module _ ((_θ_ , θcon) : Con cosetAlgebra 0ℓ) where -- A congruence relates ∼-equal (coset-equal) elements: reflexivity over ∼_H. θ-refl : {a b : G} → a ∼ b → a θ b θ-refl = reflexive θcon -- Symmetry of the congruence. θ-sym : {a b : G} → a θ b → b θ a θ-sym = IsEquivalence.sym (is-equivalence θcon) -- Transitivity of the congruence. θ-trans : {a b c : G} → a θ b → b θ c → a θ c θ-trans = IsEquivalence.trans (is-equivalence θcon) -- G-invariance: the congruence is preserved by left translation (the action of g). -- This is compatibility of θ with the unary operation symbol g of the coset algebra. θ-transl : (g : G) {a b : G} → a θ b → (g ∙ a) θ (g ∙ b) θ-transl g {a} {b} p = is-compatible θcon g {λ _ → a} {λ _ → b} (λ _ → p) -- A single group-arithmetic fact used for the interval-side round trip. ε⁻¹∙ : (a : G) → ε ⁻¹ ∙ a ≈ a ε⁻¹∙ a = ≈trans (∙-cong ε⁻¹≈ε ≈refl) (idˡ-law a)
The forward map θ ↦ K_θ¶
K_θ is the θ-class of the base coset, read as a predicate on the
group carrier: g ∈ K_θ exactly when the identity coset H·ε is θ-related to the
coset H·g (in the setoid presentation, ε θ g).
-- The forward map on predicates: K_θ g = H·ε ∼_θ H·g. Kθ : (θ : Con cosetAlgebra 0ℓ) → Pred G 0ℓ Kθ (_θ_ , _) g = ε θ g
K_θ is a subgroup. Each closure property is one short congruence
computation using the action laws: closure under _∙_ and
_⁻¹ translate the hypotheses by x and x ⁻¹
respectively, and re-anchor at ε through the unit and inverse laws;
containment of ε is reflexivity; and the respecting property is
transitivity against a ∼-step.
private -- ε ∈ K_θ (the identity coset is θ-related to itself). Kθ-ε : (θ : Con cosetAlgebra 0ℓ) → ε ∈ Kθ θ Kθ-ε (_ , θcon) = IsEquivalence.refl (is-equivalence θcon) -- K_θ is closed under the group multiplication. Kθ-∙ : (θ : Con cosetAlgebra 0ℓ) {x y : G} → x ∈ Kθ θ → y ∈ Kθ θ → x ∙ y ∈ Kθ θ Kθ-∙ θ {x} {y} εx εy = θ-trans θ εx (θ-trans θ (θ-refl θ (≈⇒∼ (≈sym (idʳ-law x)))) (θ-transl θ x εy)) -- K_θ is closed under inverses. Kθ-⁻¹ : (θ : Con cosetAlgebra 0ℓ) {x : G} → x ∈ Kθ θ → x ⁻¹ ∈ Kθ θ Kθ-⁻¹ θ {x} εx = θ-sym θ (θ-trans θ (θ-refl θ (≈⇒∼ (≈sym (idʳ-law (x ⁻¹))))) (θ-trans θ (θ-transl θ (x ⁻¹) εx) (θ-refl θ (≈⇒∼ (invˡ-law x))))) -- K_θ respects the setoid equality of the group. Kθ-resp : (θ : Con cosetAlgebra 0ℓ) → Kθ θ Respects _≈_ Kθ-resp θ x≈y εx = θ-trans θ εx (θ-refl θ (≈⇒∼ x≈y)) -- Well-definedness of the forward map (part 1): K_θ is a subgroup. Kθ-isSubgroup : (θ : Con cosetAlgebra 0ℓ) → IsSubgroup 𝒢 (Kθ θ) Kθ-isSubgroup θ = mkIsSubgroup 𝒢 (Kθ-resp θ) (Kθ-∙ θ) (Kθ-ε θ) (Kθ-⁻¹ θ) -- Well-definedness of the forward map (part 2): H ⊆ K_θ, so K_θ ∈ [H , 𝒢]. -- If h ∈ H then ε ∼_H h (as ε ⁻¹ ∙ h ≈ h ∈ H), hence H·ε ∼_θ H·h by reflexivity. H⊆Kθ : (θ : Con cosetAlgebra 0ℓ) → H ⊆ Kθ θ H⊆Kθ θ {h} h∈H = θ-refl θ (respects (≈sym (ε⁻¹∙ h)) h∈H) -- The forward map: a congruence goes to the respecting interval element [H , K_θ]. to : Con cosetAlgebra 0ℓ → Interval≈ to θ = mk (Kθ θ) (Kθ-isSubgroup θ) (H⊆Kθ θ)
The backward map K ↦ θ_K¶
For an interval element M with underlying subgroup K = pred M, the
relation θ_K is the coset relation of K: cosets H·x
and H·y are θ_K-related exactly when x ⁻¹ ∙ y ∈ K. We reuse the whole
Coset infrastructure at K, so its equivalence and left-
translation lemmas come for free.
-- The backward map's relation: the coset relation of K = pred M. θK-rel : (M : Interval≈) → BinaryRel G 0ℓ θK-rel M = Coset._∼_ 𝒢 (set M) (element-isSubgroup M)
θ_K is a congruence of the coset algebra of H.
Reflexivity over ∼_H is precisely H ⊆ K — this is
where the upper interval is needed: were K not above
H, θ_K would fail to relate ∼_H-equal cosets, so it
would not be a congruence. The equivalence and compatibility (with every left
translate) are the corresponding Coset lemmas at K.
-- Well-definedness of the backward map: θ_K is a congruence of the coset algebra. θK-isCongruence : (𝑴 : Interval≈) → IsCongruence cosetAlgebra (θK-rel 𝑴) θK-isCongruence 𝑴@(((M , _) , H≤M , _) , _) = mkcon reflx equivx compatx where Ksg : IsSubgroup 𝒢 M Ksg = element-isSubgroup 𝑴 -- Reflexivity over ∼_H: ∼_H ⊆ ∼_K pointwise, because H ⊆ K (above M). reflx : {a b : G} → a ∼ b → θK-rel 𝑴 a b reflx = H≤M -- θ_K is an equivalence (the Coset equivalence at K). equivx : IsEquivalence (θK-rel 𝑴) equivx = Coset.∼-isEquivalence 𝒢 M Ksg -- θ_K is compatible with every unary translate (left congruence at K). compatx : cosetAlgebra ∣≈ θK-rel 𝑴 compatx g h = Coset.∼-congˡ 𝒢 M Ksg g (h 0F) -- The backward map: an interval element goes to the coset congruence θ_K. from : Interval≈ → Con cosetAlgebra 0ℓ from M = θK-rel M , θK-isCongruence M
Monotonicity of both maps¶
Both maps act by (co)restriction of the underlying relations, so monotonicity is immediate: a containment of congruences forwards to a containment of the base-coset classes, and a containment of subgroups forwards to a containment of coset relations.
-- The forward map is monotone for the congruence containment order. to-mono : {θ φ : Con cosetAlgebra 0ℓ} → θ ⊑ φ → to θ ≤ᵢ to φ to-mono θ⊑φ p = θ⊑φ p -- The backward map is monotone for the interval order. from-mono : {M N : Interval≈} → M ≤ᵢ N → from M ⊑ from N from-mono M≤N p = M≤N p
Mutual inverseness¶
The two round trips close the correspondence.
On congruences, θ_{K_θ} ≑ θ: the relation θ_{K_θ} holds at (x , y) when
H·ε ∼_θ H·(x ⁻¹ ∙ y), and translating by x (resp. x ⁻¹)
re-expresses this as H·x ∼_θ H·y through the unit, inverse, and left-division laws.
-- Round trip on congruences: θ_{K_θ} ≑ θ (mutual containment). from∘to : (θ : Con cosetAlgebra 0ℓ) → from (to θ) ≑ θ from∘to θ = fwd , bwd where -- θ_{K_θ} ⊆ θ: from H·ε ∼_θ H·(x ⁻¹ ∙ y) derive H·x ∼_θ H·y. fwd : from (to θ) ⊑ θ fwd {x} {y} q = θ-trans θ (θ-refl θ (≈⇒∼ (≈sym (idʳ-law x)))) (θ-trans θ (θ-transl θ x q) (θ-refl θ (≈⇒∼ (\\-leftDividesˡ x y)))) -- θ ⊆ θ_{K_θ}: from H·x ∼_θ H·y derive H·ε ∼_θ H·(x ⁻¹ ∙ y). bwd : θ ⊑ from (to θ) bwd {x} {y} p = θ-trans θ (θ-refl θ (≈⇒∼ (≈sym (invˡ-law x)))) (θ-transl θ (x ⁻¹) p)
On the interval, K_{θ_K} ≈ K: an element g lies in K_{θ_K} when
ε ⁻¹ ∙ g ∈ K, and since ε ⁻¹ ∙ g ≈ g the respecting proof carried
by the interval element identifies this with g ∈ K. This is the step that
requires the respecting interval — the sole place the correspondence would break
over the bare SubInterval.
-- Round trip on the interval: K_{θ_K} ≈ K (needs the respecting field). to∘from : (M : Interval≈) → to (from M) ≈ᵢ M to∘from M = fwd , bwd where -- K_{θ_K} ⊆ K: ε ⁻¹ ∙ g ∈ K and ε ⁻¹ ∙ g ≈ g give g ∈ K. fwd : Kθ (from M) ⊆ set M fwd {g} p = set-respects M (ε⁻¹∙ g) p -- K ⊆ K_{θ_K}: g ∈ K and g ≈ ε ⁻¹ ∙ g give ε ⁻¹ ∙ g ∈ K. bwd : set M ⊆ Kθ (from M) bwd {g} p = set-respects M (≈sym (ε⁻¹∙ g)) p
The order isomorphism¶
Assembling the four facts (two maps, both monotone, mutually inverse) yields the
Pálfy–Pudlák bridge as an OrderIso between the congruence containment
order of the coset algebra and the respecting upper interval [H , 𝒢].
-- The order isomorphism Con (𝒢 ↷ 𝒢/H) ≅ [H , 𝒢]. BridgeIso : Type (lsuc 0ℓ) BridgeIso = OrderIso (_≑_ {𝑨 = cosetAlgebra} {ℓ = 0ℓ}) (_⊑_ {𝑨 = cosetAlgebra} {ℓ = 0ℓ}) _≈ᵢ_ _≤ᵢ_ bridge : BridgeIso bridge = record { to = to ; from = from ; to-mono = λ {θ} {φ} → to-mono {θ} {φ} ; from-mono = λ {M} {N} → from-mono {M} {N} ; to∘from = to∘from ; from∘to = from∘to }
Toward representability¶
The reverse isomorphism presents the interval [H , 𝒢] as the congruence lattice of
the coset algebra.
-- The interval [H , 𝒢], order-isomorphic to Con of the coset algebra 𝑨. RepIso : (𝑨 : Algebra {𝑆 = Sig-Unary G} 0ℓ 0ℓ) → Type (lsuc 0ℓ) RepIso 𝑨 = OrderIso _≈ᵢ_ _≤ᵢ_ (_≑_ {𝑨 = 𝑨} {ℓ = 0ℓ}) (_⊑_ {𝑨 = 𝑨} {ℓ = 0ℓ}) bridge⁻¹ : RepIso cosetAlgebra bridge⁻¹ = record { to = from ; from = to ; to-mono = λ {M} {N} → from-mono {M} {N} ; from-mono = λ {θ} {φ} → to-mono {θ} {φ} ; to∘from = from∘to ; from∘to = to∘from }
Corollary (toward representability). If the coset algebra is finite, then the
interval [H , 𝒢] is realized as the congruence lattice of a finite algebra — namely
the coset algebra itself. The roadmap's corollary "every interval in a finite
subgroup lattice is representable" is this statement with the finiteness witness
supplied.
Finiteness of the coset algebra enters as an explicit hypothesis rather than being
rederived here: cosetAlgebra-FiniteAlgebra of
Classical.Structures.Group.GSet discharges it constructively from finiteness of
𝒢 plus decidability of ∼_H — that is, of membership in
H, by ∼-dec of Classical.Structures.Group.Cosets.
The Layer-D development below meets Representableᵈ of the two-layer
discipline (ADR-008) through this same finiteness witness, with no classical
assumption.
-- Corollary: a finite coset algebra realizes the interval [H , 𝒢] as its Con. interval-Con-representable : FiniteAlgebra cosetAlgebra → Σ[ 𝑨 ∈ Algebra {𝑆 = Sig-Unary G} 0ℓ 0ℓ ] ( FiniteAlgebra 𝑨 × RepIso 𝑨 ) interval-Con-representable fin = cosetAlgebra , fin , bridge⁻¹
The Layer-D correspondence, directly and constructively¶
The updated acceptance criteria of issue #454 call for the correspondence at Layer
D: the same isomorphism with the decidable congruence poset DecCon
in place of the semantic Con. No classical assumption is needed,
because the two maps of the Layer-S bridge already carry decision procedures.
- Forward.
K_θis theθ-class of the base coset, so a decidable congruence decides membership in its own image: run its decision procedure at(ε , g). - Backward.
θ_Kis the coset relation ofK, so a membership decider forKdecidesθ_Kafter one group multiplication —∼-decof Classical.Structures.Group.Cosets, instantiated atK.
On the interval side the decidable layer quantifies over the decidably presented
interval Intervalᵈ of FLRP.Enforceable — interval elements
bundled with membership deciders — exactly as the congruence side quantifies over
DecCon rather than Con. This is a necessity, not a
convenience: over the bare interval the Layer-D isomorphism would be as
non-constructive as the Layer-S one, since an interval element can encode an arbitrary
proposition in its membership predicate and the round trip would decide it — the
oracle obstruction of the WP-1 no-go theorem, in interval clothing (see the footnote
to Intervalᵈ).
-- Forward decidability: a decidable congruence decides membership in K_θ by -- running its own decision procedure at the pair (ε , g). Kθ-dec : (d : DecCon cosetAlgebra 0ℓ) (g : G) → Dec (g ∈ Kθ (d .proj₁)) Kθ-dec d g = d .proj₂ ε g -- Backward decidability: θ_K is the coset relation of K = set M, so a membership -- decider for K decides it by a single group multiplication. θK-dec : (M : Interval≈) → (∀ x → Dec (x ∈ set M)) → ∀ x y → Dec (θK-rel M x y) θK-dec M = Coset.∼-dec 𝒢 (set M) (element-isSubgroup M)
The two maps of the decidable layer are the Layer-S maps, each paired with its decision procedure.
-- The forward map at Layer D: K_θ together with its decision procedure. toᵈ : DecCon cosetAlgebra 0ℓ → Intervalᵈ toᵈ d = to (d .proj₁) , Kθ-dec d -- The backward map at Layer D: θ_K together with its decision procedure. fromᵈ : Intervalᵈ → DecCon cosetAlgebra 0ℓ fromᵈ M = from (M .proj₁) , θK-dec (M .proj₁) (M .proj₂)
The Layer-D equivalences and orders on the two sides (≑ᵈ,
⊆ᵈ; ≈ᵢᵈ, ≤ᵢᵈ) compare the
underlying congruences and interval elements, so the monotonicity and round-trip
proofs of the Layer-S bridge transport verbatim — nothing is reproved. (The endpoint
implicits of the monotone maps are forwarded explicitly, per the non-injectivity
discipline of Setoid.Congruences.Lattice.)
-- The Layer-D order isomorphism DecCon (𝒢 ↷ 𝒢/H) ≅ [H , 𝒢]ᵈ — with no -- classical assumption. BridgeIsoᵈ : Type (lsuc 0ℓ) BridgeIsoᵈ = OrderIso (_≑ᵈ_ {𝑨 = cosetAlgebra} {ℓ = 0ℓ}) (_⊆ᵈ_ {𝑨 = cosetAlgebra} {ℓ = 0ℓ}) _≈ᵢᵈ_ _≤ᵢᵈ_ bridgeᵈ : BridgeIsoᵈ bridgeᵈ = record { to = toᵈ ; from = fromᵈ ; to-mono = λ {d} {e} → to-mono {d .proj₁} {e .proj₁} ; from-mono = λ {M} {N} → from-mono {M .proj₁} {N .proj₁} ; to∘from = λ M → to∘from (M .proj₁) ; from∘to = λ d → from∘to (d .proj₁) }
The reverse isomorphism presents the decidable interval as the decidable congruence
poset of the coset algebra — the Layer-D analogue of bridge⁻¹.
RepIsoᵈ : (𝑨 : Algebra {𝑆 = Sig-Unary G} 0ℓ 0ℓ) → Type (lsuc 0ℓ) RepIsoᵈ 𝑨 = OrderIso _≈ᵢᵈ_ _≤ᵢᵈ_ (_≑ᵈ_ {𝑨 = 𝑨} {ℓ = 0ℓ}) (_⊆ᵈ_ {𝑨 = 𝑨} {ℓ = 0ℓ}) bridgeᵈ⁻¹ : RepIsoᵈ cosetAlgebra bridgeᵈ⁻¹ = record { to = fromᵈ ; from = toᵈ ; to-mono = λ {M} {N} → from-mono {M .proj₁} {N .proj₁} ; from-mono = λ {d} {e} → to-mono {d .proj₁} {e .proj₁} ; to∘from = λ d → from∘to (d .proj₁) ; from∘to = λ M → to∘from (M .proj₁) }
Corollary (Layer D).3 A finite coset algebra realizes the decidable interval
[H , 𝒢]ᵈ as its decidable congruence poset — unconditionally. The finiteness
witness is itself discharged constructively by
cosetAlgebra-FiniteAlgebra whenever membership in H is
decidable.
interval-DecCon-representable : FiniteAlgebra cosetAlgebra → Σ[ 𝑨 ∈ Algebra {𝑆 = Sig-Unary G} 0ℓ 0ℓ ] ( FiniteAlgebra 𝑨 × RepIsoᵈ 𝑨 ) interval-DecCon-representable fin = cosetAlgebra , fin , bridgeᵈ⁻¹
Composing with an interval isomorphism¶
The representability corollary must turn an interval isomorphism [H , 𝒢] ≅ 𝑳 — an
IntervalIso of FLRP.Enforceable, stated over the bare respecting
interval — into a decidable-layer congruence isomorphism ConIsoᵈ cosetAlgebra 𝑳 of
FLRP.Representable. The composition follows compose-IntervalIso
of FLRP.Enforceable: the interval-equality round trip is pushed through the
lattice-valued map by the meet order's antisymmetry, and through the
congruence-valued map by monotonicity.
One datum is needed beyond the isomorphism itself: a membership decider for each
interval element in the image of the isomorphism's backward map, so that the
composite's backward map lands in DecCon. Per the discussion above
this is genuinely data — part of the Layer-D presentation of the representation, like
decidable membership in H itself — not derivable from finiteness.
IntervalIso→ConIsoᵈ : (𝑳 : Lattice) (iso : IntervalIso 𝒢 H H-sg 𝑳) → (∀ u x → Dec (x ∈ set (OrderIso.from iso u))) → ConIsoᵈ cosetAlgebra 𝑳 IntervalIso→ConIsoᵈ 𝑳 iso from-dec = record { to = to' ; from = from' ; to-mono = λ {d} {e} → I.to-mono ∘ to-mono {d .proj₁} {e .proj₁} ; from-mono = λ {u} {v} → from-mono {I.from u} {I.from v} ∘ I.from-mono {u} {v} ; to∘from = tf ; from∘to = ft } where module I = OrderIso iso open Setoid 𝔻[ proj₁ 𝑳 ] using () renaming ( _≈_ to _≈ᴸ_ ; trans to ≈ᴸ-trans ) open Lattice-Order 𝑳 using () renaming ( ≤-antisym to ≤ᴸ-antisym ) to' : DecCon cosetAlgebra 0ℓ → 𝕌[ proj₁ 𝑳 ] to' d = I.to (to (d .proj₁)) from' : 𝕌[ proj₁ 𝑳 ] → DecCon cosetAlgebra 0ℓ from' u = fromᵈ (I.from u , from-dec u) -- 𝑳 → DecCon → 𝑳: a bridge round trip pushed through I.to by antisymmetry, -- then an iso round trip. tf : ∀ u → to' (from' u) ≈ᴸ u tf u = ≈ᴸ-trans (≤ᴸ-antisym (I.to-mono (to∘from (I.from u) .proj₁)) (I.to-mono (to∘from (I.from u) .proj₂))) (I.to∘from u) -- DecCon → 𝑳 → DecCon: an iso round trip pushed through `from` by -- monotonicity, then a bridge round trip, composed on each ⇒-direction. ft : ∀ d → from' (to' d) ≑ᵈ d ft d = from∘to (d .proj₁) .proj₁ ∘ from-mono {I.from (to' d)} {to (d .proj₁)} (I.from∘to (to (d .proj₁)) .proj₁) , from-mono {to (d .proj₁)} {I.from (to' d)} (I.from∘to (to (d .proj₁)) .proj₂) ∘ from∘to (d .proj₁) .proj₂
From group representability to decidable representability¶
The headline corollary of issue #454: a lattice that occurs as an upper interval
[H , 𝒢] in a subgroup lattice (GroupRepresentable of
FLRP.Enforceable) is decidably representable (Representableᵈ of
FLRP.Representable), the representing finite algebra being the coset algebra
𝒢 ↷ 𝒢/H of the witnessing representation.
The hypotheses are exactly the Layer-D presentation data of the witness, per audit A2
(docs/notes/flrp-wp7-audits.md):
- carrier finiteness of the group, as a
FiniteAlgebrawitness; - finite-finitariness of the unary signature on the group's carrier — built from an
≡-surjective enumeration of the carrier bySig-Unary-FiniteSignatureof Classical.Signatures.Finite (surjectivity up to≈does not suffice for a signature; see the caveat there); - a membership decider for
H; - membership deciders for the interval elements in the image of the interval isomorphism's backward map.
None of these is classical, and all are inhabited by the concrete finite groups the FLRP program ranges over (Cayley-table groups with decidable subgroup predicates).
module _ (𝑳 : Lattice) (rep : GroupRepresentable 𝑳) where open GroupRepresentable rep -- grp , sub , isSubgroup , interval-iso private module B = Bridge grp sub isSubgroup module UI = UpperInterval grp sub isSubgroup module I = OrderIso interval-iso open CosetAction grp sub isSubgroup using ( cosetAlgebra ; cosetAlgebra-FiniteAlgebra ) open Coset grp sub isSubgroup using ( ∼-dec ) -- Every group-representable lattice is decidably representable, via the coset -- algebra of the witnessing representation. GroupRepresentable→Representableᵈ : FiniteAlgebra (grp .proj₁) → FiniteSignature (Sig-Unary 𝕌[ grp .proj₁ ]) → (∀ x → Dec (x ∈ sub)) → (∀ u x → Dec (x ∈ UI.set (I.from u))) → Representableᵈ 𝑳 GroupRepresentable→Representableᵈ fin finsig sub-dec from-dec = record { sigᵈ = Sig-Unary 𝕌[ grp .proj₁ ] ; algᵈ = cosetAlgebra ; finiteᵈ = cosetAlgebra-FiniteAlgebra fin (∼-dec sub-dec) ; finsigᵈ = finsig ; con-isoᵈ = B.IntervalIso→ConIsoᵈ 𝑳 interval-iso from-dec }
-
This is the main deliverable of work package WP-3; see
docs/notes/flrp-research-roadmap.md§ 7. Classical references include McKenzie–McNulty–Taylor Lemma 4.20, Dixon–Mortimer Theorem 1.5A, and the introduction of the research notedocs/papers/flrp/ieprops/IEProps-1205.1927v4.tex. ↩ -
An earlier revision of this module reached Layer D by composing
bridge⁻¹with the cross-layer isomorphismCon 𝑨 ≅ DecCon 𝑨of FLRP.LayerBridge, which consumes the registered classical assumptionCongruenceCompletenessof FLRP.Assumptions. The direct construction below supersedes that composition: stated over the decidably presented interval, the correspondence needs no assumption at all, which is what the acceptance criteria of Issue #454 require. The generic cross-layer transports remain available in FLRP.LayerBridge for results that genuinely live at Layer S. ↩ -
This Corollary, together with
GroupRepresentable→Representableᵈat the end of the module, closes Issue #454. ↩