Closure operators on large posets

Content created by Egbert Rijke, Fredrik Bakke, Julian KG, Maša Žaucer, fernabnor, Gregor Perčič and louismntnu.

Created on 2023-06-08.
Last modified on 2024-04-11.

module order-theory.closure-operators-large-posets where
Imports 
open import foundation.identity-types
open import foundation.large-binary-relations
open import foundation.propositions
open import foundation.sets
open import foundation.universe-levels

open import order-theory.large-posets
open import order-theory.large-subposets
open import order-theory.large-subpreorders
open import order-theory.order-preserving-maps-large-posets

Idea

A closure operator on a large poset P consists of an order preserving map cl : P → P such that

  1. cl is increasing, i.e., x ≤ cl x for each x : P, and
  2. cl is idempotent, i.e., cl (cl x) ＝ cl x for each x : P.

In other words, closure operators are idempotent monads on (large) posets.

Definitions

Closure operators on large posets

module _
  {α : Level → Level} {β : Level → Level → Level}
  (P : Large-Poset α β)
  where

  record
    closure-operator-Large-Poset : UUω
    where
    field
      hom-closure-operator-Large-Poset :
        hom-Large-Poset (λ l → l) P P
      is-inflationary-closure-operator-Large-Poset :
        {l1 : Level} (x : type-Large-Poset P l1) →
        leq-Large-Poset P x
          ( map-hom-Large-Poset P P hom-closure-operator-Large-Poset x)
      is-idempotent-closure-operator-Large-Poset :
        {l1 : Level} (x : type-Large-Poset P l1) →
        map-hom-Large-Poset P P hom-closure-operator-Large-Poset
          ( map-hom-Large-Poset P P hom-closure-operator-Large-Poset x) ＝
        map-hom-Large-Poset P P hom-closure-operator-Large-Poset x

  open closure-operator-Large-Poset public

  module _
    (cl : closure-operator-Large-Poset)
    where

    map-closure-operator-Large-Poset :
      {l1 : Level} → type-Large-Poset P l1 → type-Large-Poset P l1
    map-closure-operator-Large-Poset =
      map-hom-Large-Poset P P (hom-closure-operator-Large-Poset cl)

    preserves-order-closure-operator-Large-Poset :
      {l1 l2 : Level}
      (x : type-Large-Poset P l1) (y : type-Large-Poset P l2) →
      leq-Large-Poset P x y →
      leq-Large-Poset P
        ( map-closure-operator-Large-Poset x)
        ( map-closure-operator-Large-Poset y)
    preserves-order-closure-operator-Large-Poset =
      preserves-order-hom-Large-Poset P P (hom-closure-operator-Large-Poset cl)

The large subposet of closed elements of a closure operator

module _
  {α : Level → Level} {β : Level → Level → Level}
  (P : Large-Poset α β) (cl : closure-operator-Large-Poset P)
  where

  large-subpreorder-closure-operator-Large-Poset :
    Large-Subpreorder α (large-preorder-Large-Poset P)
  large-subpreorder-closure-operator-Large-Poset {l1} x =
    Id-Prop (set-Large-Poset P l1) (map-closure-operator-Large-Poset P cl x) x

  is-closed-element-closure-operator-Large-Poset :
    {l1 : Level} → type-Large-Poset P l1 → UU (α l1)
  is-closed-element-closure-operator-Large-Poset =
    is-in-Large-Subpreorder
      ( large-preorder-Large-Poset P)
      ( large-subpreorder-closure-operator-Large-Poset)

  is-prop-is-closed-element-closure-operator-Large-Poset :
    {l1 : Level} (x : type-Large-Poset P l1) →
    is-prop (is-closed-element-closure-operator-Large-Poset x)
  is-prop-is-closed-element-closure-operator-Large-Poset =
    is-prop-is-in-Large-Subpreorder
      ( large-preorder-Large-Poset P)
      ( large-subpreorder-closure-operator-Large-Poset)

  is-closed-element-leq-closure-operator-Large-Poset :
    {l1 : Level} (x : type-Large-Poset P l1) →
    leq-Large-Poset P (map-closure-operator-Large-Poset P cl x) x →
    is-closed-element-closure-operator-Large-Poset x
  is-closed-element-leq-closure-operator-Large-Poset x H =
    antisymmetric-leq-Large-Poset P
      ( map-closure-operator-Large-Poset P cl x)
      ( x)
      ( H)
      ( is-inflationary-closure-operator-Large-Poset cl x)

  closed-element-closure-operator-Large-Poset :
    (l1 : Level) → UU (α l1)
  closed-element-closure-operator-Large-Poset =
    type-Large-Subpreorder
      ( large-preorder-Large-Poset P)
      ( large-subpreorder-closure-operator-Large-Poset)

  is-closed-under-sim-closure-operator-Large-Poset :
    {l1 l2 : Level}
    (x : type-Large-Poset P l1)
    (y : type-Large-Poset P l2) →
    leq-Large-Poset P x y → leq-Large-Poset P y x →
    is-closed-element-closure-operator-Large-Poset x →
    is-closed-element-closure-operator-Large-Poset y
  is-closed-under-sim-closure-operator-Large-Poset x y H K c =
    is-closed-element-leq-closure-operator-Large-Poset y
      ( transitive-leq-Large-Poset P
        ( map-closure-operator-Large-Poset P cl y)
        ( map-closure-operator-Large-Poset P cl x)
        ( y)
        ( transitive-leq-Large-Poset P
          ( map-closure-operator-Large-Poset P cl x)
          ( x)
          ( y)
          ( H)
          ( leq-eq-Large-Poset P c))
        ( preserves-order-closure-operator-Large-Poset P cl y x K))

  large-subposet-closure-operator-Large-Poset :
    Large-Subposet α P
  large-subpreorder-Large-Subposet
    large-subposet-closure-operator-Large-Poset =
    large-subpreorder-closure-operator-Large-Poset
  is-closed-under-sim-Large-Subposet
    large-subposet-closure-operator-Large-Poset =
    is-closed-under-sim-closure-operator-Large-Poset

  large-poset-closure-operator-Large-Poset :
    Large-Poset α β
  large-poset-closure-operator-Large-Poset =
    large-poset-Large-Subposet P
      ( large-subposet-closure-operator-Large-Poset)

  leq-prop-closed-element-closure-operator-Large-Poset :
    Large-Relation-Prop β closed-element-closure-operator-Large-Poset
  leq-prop-closed-element-closure-operator-Large-Poset =
    leq-prop-Large-Subposet P
      ( large-subposet-closure-operator-Large-Poset)

  leq-closed-element-closure-operator-Large-Poset :
    Large-Relation β closed-element-closure-operator-Large-Poset
  leq-closed-element-closure-operator-Large-Poset =
    leq-Large-Subposet P
      ( large-subposet-closure-operator-Large-Poset)

  is-prop-leq-closed-element-closure-operator-Large-Poset :
    is-prop-Large-Relation
      ( closed-element-closure-operator-Large-Poset)
      ( leq-closed-element-closure-operator-Large-Poset)
  is-prop-leq-closed-element-closure-operator-Large-Poset =
    is-prop-leq-Large-Subposet P
      ( large-subposet-closure-operator-Large-Poset)

  refl-leq-closed-element-closure-operator-Large-Poset :
    is-reflexive-Large-Relation
      ( closed-element-closure-operator-Large-Poset)
      ( leq-closed-element-closure-operator-Large-Poset)
  refl-leq-closed-element-closure-operator-Large-Poset =
    refl-leq-Large-Subposet P
      ( large-subposet-closure-operator-Large-Poset)

  antisymmetric-leq-closed-element-closure-operator-Large-Poset :
    is-antisymmetric-Large-Relation
      ( closed-element-closure-operator-Large-Poset)
      ( leq-closed-element-closure-operator-Large-Poset)
  antisymmetric-leq-closed-element-closure-operator-Large-Poset =
    antisymmetric-leq-Large-Subposet P
      ( large-subposet-closure-operator-Large-Poset)

  transitive-leq-closed-element-closure-operator-Large-Poset :
    is-transitive-Large-Relation
      ( closed-element-closure-operator-Large-Poset)
      ( leq-closed-element-closure-operator-Large-Poset)
  transitive-leq-closed-element-closure-operator-Large-Poset =
    transitive-leq-Large-Subposet P
      ( large-subposet-closure-operator-Large-Poset)

Recent changes