Nuclei on large locales
module order-theory.nuclei-large-locales where
Imports
open import foundation.dependent-pair-types open import foundation.functions open import foundation.identity-types open import foundation.logical-equivalences open import foundation.propositions open import foundation.sets open import foundation.subtypes open import foundation.universe-levels open import order-theory.homomorphisms-large-meet-semilattices open import order-theory.large-frames open import order-theory.large-locales open import order-theory.large-meet-semilattices open import order-theory.large-meet-subsemilattices open import order-theory.large-posets open import order-theory.large-subposets open import order-theory.large-subpreorders open import order-theory.large-suplattices open import order-theory.least-upper-bounds-large-posets
Idea
A nucleus on a large locale L is an order
preserving map j : hom-Large-Poset id L L such that j preserves meets and is
idempotent.
Definitions
Nuclei on large locales
module _ {α : Level → Level} {β : Level → Level → Level} (L : Large-Locale α β) where record nucleus-Large-Locale : UUω where field hom-large-meet-semilattice-nucleus-Large-Locale : hom-Large-Meet-Semilattice ( large-meet-semilattice-Large-Locale L) ( large-meet-semilattice-Large-Locale L) is-increasing-nucleus-Large-Locale : {l1 : Level} (x : type-Large-Locale L l1) → leq-Large-Locale L x ( map-hom-Large-Meet-Semilattice ( large-meet-semilattice-Large-Locale L) ( large-meet-semilattice-Large-Locale L) ( hom-large-meet-semilattice-nucleus-Large-Locale) ( x)) is-idempotent-nucleus-Large-Locale : {l1 : Level} (x : type-Large-Locale L l1) → map-hom-Large-Meet-Semilattice ( large-meet-semilattice-Large-Locale L) ( large-meet-semilattice-Large-Locale L) ( hom-large-meet-semilattice-nucleus-Large-Locale) ( map-hom-Large-Meet-Semilattice ( large-meet-semilattice-Large-Locale L) ( large-meet-semilattice-Large-Locale L) ( hom-large-meet-semilattice-nucleus-Large-Locale) ( x)) ＝ map-hom-Large-Meet-Semilattice ( large-meet-semilattice-Large-Locale L) ( large-meet-semilattice-Large-Locale L) ( hom-large-meet-semilattice-nucleus-Large-Locale) ( x) open nucleus-Large-Locale public module _ (j : nucleus-Large-Locale) where map-nucleus-Large-Locale : {l1 : Level} → type-Large-Locale L l1 → type-Large-Locale L l1 map-nucleus-Large-Locale = map-hom-Large-Meet-Semilattice ( large-meet-semilattice-Large-Locale L) ( large-meet-semilattice-Large-Locale L) ( hom-large-meet-semilattice-nucleus-Large-Locale j) preserves-order-nucleus-Large-Locale : {l1 l2 : Level} (x : type-Large-Locale L l1) (y : type-Large-Locale L l2) → leq-Large-Locale L x y → leq-Large-Locale L ( map-nucleus-Large-Locale x) ( map-nucleus-Large-Locale y) preserves-order-nucleus-Large-Locale = preserves-order-hom-Large-Meet-Semilattice ( large-meet-semilattice-Large-Locale L) ( large-meet-semilattice-Large-Locale L) ( hom-large-meet-semilattice-nucleus-Large-Locale j) preserves-meets-nucleus-Large-Locale : {l1 l2 : Level} (x : type-Large-Locale L l1) (y : type-Large-Locale L l2) → map-nucleus-Large-Locale (meet-Large-Locale L x y) ＝ meet-Large-Locale L ( map-nucleus-Large-Locale x) ( map-nucleus-Large-Locale y) preserves-meets-nucleus-Large-Locale = preserves-meets-hom-Large-Meet-Semilattice ( hom-large-meet-semilattice-nucleus-Large-Locale j) preserves-top-nucleus-Large-Locale : map-nucleus-Large-Locale (top-Large-Locale L) ＝ top-Large-Locale L preserves-top-nucleus-Large-Locale = preserves-top-hom-Large-Meet-Semilattice ( hom-large-meet-semilattice-nucleus-Large-Locale j)
The large locale of j-closed elements of a nucleus
module _ {α : Level → Level} {β : Level → Level → Level} (L : Large-Locale α β) (j : nucleus-Large-Locale L) where large-subpreorder-nucleus-Large-Locale : Large-Subpreorder α (large-preorder-Large-Locale L) large-subpreorder-nucleus-Large-Locale {l1} x = Id-Prop (set-Large-Locale L l1) (map-nucleus-Large-Locale L j x) x is-closed-element-nucleus-Large-Locale : {l1 : Level} → type-Large-Locale L l1 → UU (α l1) is-closed-element-nucleus-Large-Locale = is-in-Large-Subpreorder ( large-preorder-Large-Locale L) ( large-subpreorder-nucleus-Large-Locale) is-prop-is-closed-element-nucleus-Large-Locale : {l1 : Level} (x : type-Large-Locale L l1) → is-prop (is-closed-element-nucleus-Large-Locale x) is-prop-is-closed-element-nucleus-Large-Locale = is-prop-is-in-Large-Subpreorder ( large-preorder-Large-Locale L) ( large-subpreorder-nucleus-Large-Locale) is-closed-element-leq-nucleus-Large-Locale : {l1 : Level} (x : type-Large-Locale L l1) → leq-Large-Locale L (map-nucleus-Large-Locale L j x) x → is-closed-element-nucleus-Large-Locale x is-closed-element-leq-nucleus-Large-Locale x H = antisymmetric-leq-Large-Locale L ( map-nucleus-Large-Locale L j x) ( x) ( H) (is-increasing-nucleus-Large-Locale j x) closed-element-nucleus-Large-Locale : (l1 : Level) → UU (α l1) closed-element-nucleus-Large-Locale = type-Large-Subpreorder ( large-preorder-Large-Locale L) ( large-subpreorder-nucleus-Large-Locale) is-closed-under-sim-nucleus-Large-Locale : {l1 l2 : Level} (x : type-Large-Locale L l1) (y : type-Large-Locale L l2) → leq-Large-Locale L x y → leq-Large-Locale L y x → is-closed-element-nucleus-Large-Locale x → is-closed-element-nucleus-Large-Locale y is-closed-under-sim-nucleus-Large-Locale x y H K c = is-closed-element-leq-nucleus-Large-Locale y ( transitive-leq-Large-Locale L ( map-nucleus-Large-Locale L j y) ( map-nucleus-Large-Locale L j x) ( y) ( transitive-leq-Large-Locale L ( map-nucleus-Large-Locale L j x) ( x) ( y) ( H) ( leq-eq-Large-Locale L c)) ( preserves-order-nucleus-Large-Locale L j y x K)) large-subposet-nucleus-Large-Locale : Large-Subposet α (large-poset-Large-Locale L) large-subpreorder-Large-Subposet large-subposet-nucleus-Large-Locale = large-subpreorder-nucleus-Large-Locale is-closed-under-sim-Large-Subposet large-subposet-nucleus-Large-Locale = is-closed-under-sim-nucleus-Large-Locale large-poset-nucleus-Large-Locale : Large-Poset (λ l → α l ⊔ α l) β large-poset-nucleus-Large-Locale = large-poset-Large-Subposet ( large-poset-Large-Locale L) ( large-subposet-nucleus-Large-Locale) leq-closed-element-nucleus-Large-Locale-Prop : {l1 l2 : Level} (x : closed-element-nucleus-Large-Locale l1) (y : closed-element-nucleus-Large-Locale l2) → Prop (β l1 l2) leq-closed-element-nucleus-Large-Locale-Prop = leq-Large-Subposet-Prop ( large-poset-Large-Locale L) ( large-subposet-nucleus-Large-Locale) leq-closed-element-nucleus-Large-Locale : {l1 l2 : Level} (x : closed-element-nucleus-Large-Locale l1) (y : closed-element-nucleus-Large-Locale l2) → UU (β l1 l2) leq-closed-element-nucleus-Large-Locale = leq-Large-Subposet ( large-poset-Large-Locale L) ( large-subposet-nucleus-Large-Locale) is-prop-leq-closed-element-nucleus-Large-Locale : {l1 l2 : Level} (x : closed-element-nucleus-Large-Locale l1) (y : closed-element-nucleus-Large-Locale l2) → is-prop (leq-closed-element-nucleus-Large-Locale x y) is-prop-leq-closed-element-nucleus-Large-Locale = is-prop-leq-Large-Subposet ( large-poset-Large-Locale L) ( large-subposet-nucleus-Large-Locale) refl-leq-closed-element-nucleus-Large-Locale : {l1 : Level} (x : closed-element-nucleus-Large-Locale l1) → leq-closed-element-nucleus-Large-Locale x x refl-leq-closed-element-nucleus-Large-Locale = refl-leq-Large-Subposet ( large-poset-Large-Locale L) ( large-subposet-nucleus-Large-Locale) antisymmetric-leq-closed-element-nucleus-Large-Locale : {l1 : Level} (x y : closed-element-nucleus-Large-Locale l1) → leq-closed-element-nucleus-Large-Locale x y → leq-closed-element-nucleus-Large-Locale y x → x ＝ y antisymmetric-leq-closed-element-nucleus-Large-Locale = antisymmetric-leq-Large-Subposet ( large-poset-Large-Locale L) ( large-subposet-nucleus-Large-Locale) transitive-leq-closed-element-nucleus-Large-Locale : {l1 l2 l3 : Level} (x : closed-element-nucleus-Large-Locale l1) (y : closed-element-nucleus-Large-Locale l2) (z : closed-element-nucleus-Large-Locale l3) → leq-closed-element-nucleus-Large-Locale y z → leq-closed-element-nucleus-Large-Locale x y → leq-closed-element-nucleus-Large-Locale x z transitive-leq-closed-element-nucleus-Large-Locale = transitive-leq-Large-Subposet ( large-poset-Large-Locale L) ( large-subposet-nucleus-Large-Locale) is-closed-under-meets-large-subposet-nucleus-Large-Locale : is-closed-under-meets-Large-Subposet ( large-meet-semilattice-Large-Locale L) ( large-subposet-nucleus-Large-Locale) is-closed-under-meets-large-subposet-nucleus-Large-Locale x y p q = ( preserves-meets-nucleus-Large-Locale L j x y) ∙ ( ap-meet-Large-Locale L p q) contains-top-large-subposet-nucleus-Large-Locale : contains-top-Large-Subposet ( large-meet-semilattice-Large-Locale L) ( large-subposet-nucleus-Large-Locale) contains-top-large-subposet-nucleus-Large-Locale = is-closed-element-leq-nucleus-Large-Locale ( top-Large-Locale L) ( is-top-element-top-Large-Locale L ( map-nucleus-Large-Locale L j (top-Large-Locale L))) large-meet-subsemilattice-nucleus-Large-Locale : Large-Meet-Subsemilattice α (large-meet-semilattice-Large-Locale L) large-subposet-Large-Meet-Subsemilattice large-meet-subsemilattice-nucleus-Large-Locale = large-subposet-nucleus-Large-Locale is-closed-under-meets-Large-Meet-Subsemilattice large-meet-subsemilattice-nucleus-Large-Locale = is-closed-under-meets-large-subposet-nucleus-Large-Locale contains-top-Large-Meet-Subsemilattice large-meet-subsemilattice-nucleus-Large-Locale = contains-top-large-subposet-nucleus-Large-Locale is-large-meet-semilattice-nucleus-Large-Locale : is-large-meet-semilattice-Large-Poset ( large-poset-nucleus-Large-Locale) is-large-meet-semilattice-nucleus-Large-Locale = is-large-meet-semilattice-Large-Meet-Subsemilattice ( large-meet-semilattice-Large-Locale L) ( large-meet-subsemilattice-nucleus-Large-Locale) large-meet-semilattice-nucleus-Large-Locale : Large-Meet-Semilattice (λ l → α l ⊔ α l) β large-meet-semilattice-nucleus-Large-Locale = large-meet-semilattice-Large-Meet-Subsemilattice ( large-meet-semilattice-Large-Locale L) ( large-meet-subsemilattice-nucleus-Large-Locale) meet-closed-element-nucleus-Large-Locale : {l1 l2 : Level} → closed-element-nucleus-Large-Locale l1 → closed-element-nucleus-Large-Locale l2 → closed-element-nucleus-Large-Locale (l1 ⊔ l2) meet-closed-element-nucleus-Large-Locale = meet-Large-Meet-Semilattice large-meet-semilattice-nucleus-Large-Locale forward-implication-adjoint-relation-nucleus-Large-Locale : {l1 l2 : Level} {x : type-Large-Locale L l1} {y : type-Large-Locale L l2} → is-closed-element-nucleus-Large-Locale y → leq-Large-Locale L x y → leq-Large-Locale L (map-nucleus-Large-Locale L j x) y forward-implication-adjoint-relation-nucleus-Large-Locale {x = x} {y} H K = transitive-leq-Large-Locale L ( map-nucleus-Large-Locale L j x) ( map-nucleus-Large-Locale L j y) ( y) ( leq-eq-Large-Locale L H) ( preserves-order-nucleus-Large-Locale L j ( x) ( y) ( K)) backward-implication-adjoint-relation-nucleus-Large-Locale : {l1 l2 : Level} {x : type-Large-Locale L l1} {y : type-Large-Locale L l2} → leq-Large-Locale L (map-nucleus-Large-Locale L j x) y → leq-Large-Locale L x y backward-implication-adjoint-relation-nucleus-Large-Locale {x = x} {y} H = transitive-leq-Large-Locale L ( x) ( map-nucleus-Large-Locale L j x) ( y) ( H) ( is-increasing-nucleus-Large-Locale j x) adjoint-relation-nucleus-Large-Locale : {l1 l2 : Level} (x : type-Large-Locale L l1) (y : type-Large-Locale L l2) → is-closed-element-nucleus-Large-Locale y → leq-Large-Locale L x y ↔ leq-Large-Locale L (map-nucleus-Large-Locale L j x) y pr1 (adjoint-relation-nucleus-Large-Locale x y H) = forward-implication-adjoint-relation-nucleus-Large-Locale H pr2 (adjoint-relation-nucleus-Large-Locale x y H) = backward-implication-adjoint-relation-nucleus-Large-Locale sup-closed-element-nucleus-Large-Locale : {l1 l2 : Level} {I : UU l1} (x : I → closed-element-nucleus-Large-Locale l2) → closed-element-nucleus-Large-Locale (l1 ⊔ l2) pr1 (sup-closed-element-nucleus-Large-Locale x) = map-nucleus-Large-Locale L j (sup-Large-Locale L (pr1 ∘ x)) pr2 (sup-closed-element-nucleus-Large-Locale x) = is-idempotent-nucleus-Large-Locale j (sup-Large-Locale L (pr1 ∘ x)) is-least-upper-bound-sup-closed-element-nucleus-Large-Locale : {l1 l2 : Level} {I : UU l1} (x : I → closed-element-nucleus-Large-Locale l2) → is-least-upper-bound-family-of-elements-Large-Poset ( large-poset-nucleus-Large-Locale) ( x) ( sup-closed-element-nucleus-Large-Locale x) pr1 (is-least-upper-bound-sup-closed-element-nucleus-Large-Locale x y) H = forward-implication-adjoint-relation-nucleus-Large-Locale ( pr2 y) ( forward-implication ( is-least-upper-bound-sup-Large-Locale L (pr1 ∘ x) (pr1 y)) ( H)) pr2 (is-least-upper-bound-sup-closed-element-nucleus-Large-Locale x y) H = backward-implication ( is-least-upper-bound-sup-Large-Locale L (pr1 ∘ x) (pr1 y)) ( backward-implication-adjoint-relation-nucleus-Large-Locale H) is-large-suplattice-large-poset-nucleus-Large-Locale : is-large-suplattice-Large-Poset ( large-poset-nucleus-Large-Locale) sup-has-least-upper-bound-family-of-elements-Large-Poset ( is-large-suplattice-large-poset-nucleus-Large-Locale x) = sup-closed-element-nucleus-Large-Locale x is-least-upper-bound-sup-has-least-upper-bound-family-of-elements-Large-Poset ( is-large-suplattice-large-poset-nucleus-Large-Locale x) = is-least-upper-bound-sup-closed-element-nucleus-Large-Locale x large-suplattice-nucleus-Large-Locale : Large-Suplattice (λ l → α l ⊔ α l) β large-poset-Large-Suplattice large-suplattice-nucleus-Large-Locale = large-poset-nucleus-Large-Locale is-large-suplattice-Large-Suplattice large-suplattice-nucleus-Large-Locale = is-large-suplattice-large-poset-nucleus-Large-Locale distributive-meet-sup-nucleus-Large-Locale : {l1 l2 l3 : Level} (x : closed-element-nucleus-Large-Locale l1) {I : UU l2} (y : I → closed-element-nucleus-Large-Locale l3) → meet-closed-element-nucleus-Large-Locale x ( sup-closed-element-nucleus-Large-Locale y) ＝ sup-closed-element-nucleus-Large-Locale ( λ i → meet-closed-element-nucleus-Large-Locale x (y i)) distributive-meet-sup-nucleus-Large-Locale (x , p) y = eq-type-subtype ( large-subpreorder-nucleus-Large-Locale) ( ( ap (λ u → meet-Large-Locale L u _) (inv p)) ∙ ( ( inv ( preserves-meets-nucleus-Large-Locale L j x _)) ∙ ( ap ( map-nucleus-Large-Locale L j) ( distributive-meet-sup-Large-Locale L x (pr1 ∘ y))))) large-frame-nucleus-Large-Locale : Large-Frame (λ l → α l ⊔ α l) β large-poset-Large-Frame large-frame-nucleus-Large-Locale = large-poset-nucleus-Large-Locale is-large-meet-semilattice-Large-Frame large-frame-nucleus-Large-Locale = is-large-meet-semilattice-nucleus-Large-Locale is-large-suplattice-Large-Frame large-frame-nucleus-Large-Locale = is-large-suplattice-large-poset-nucleus-Large-Locale distributive-meet-sup-Large-Frame large-frame-nucleus-Large-Locale = distributive-meet-sup-nucleus-Large-Locale large-locale-nucleus-Large-Locale : Large-Locale (λ l → α l ⊔ α l) β large-locale-nucleus-Large-Locale = large-frame-nucleus-Large-Locale