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