Large meet-subsemilattices

Content created by Egbert Rijke, Fredrik Bakke, Julian KG, fernabnor, Gregor Perčič and louismntnu.

Created on 2023-05-12.
Last modified on 2024-04-11.

module order-theory.large-meet-subsemilattices where
Imports 
open import foundation.dependent-pair-types
open import foundation.large-binary-relations
open import foundation.universe-levels

open import order-theory.greatest-lower-bounds-large-posets
open import order-theory.large-meet-semilattices
open import order-theory.large-posets
open import order-theory.large-preorders
open import order-theory.large-subposets
open import order-theory.top-elements-large-posets

Idea

A large meet-subsemilattice of a large meet-semilattice L is a large subposet S of L that is closed under meets and contains the top element.

Definitions

The predicate that a large subposet is closed under meets

module _
  {α : Level → Level} {β : Level → Level → Level} {γ : Level → Level}
  (L : Large-Meet-Semilattice α β)
  (S : Large-Subposet γ (large-poset-Large-Meet-Semilattice L))
  where

  is-closed-under-meets-Large-Subposet : UUω
  is-closed-under-meets-Large-Subposet =
    {l1 l2 : Level}
    (x : type-Large-Meet-Semilattice L l1)
    (y : type-Large-Meet-Semilattice L l2) →
    is-in-Large-Subposet (large-poset-Large-Meet-Semilattice L) S x →
    is-in-Large-Subposet (large-poset-Large-Meet-Semilattice L) S y →
    is-in-Large-Subposet
      ( large-poset-Large-Meet-Semilattice L)
      ( S)
      ( meet-Large-Meet-Semilattice L x y)

The predicate that a large subposet contains the top element

module _
  {α : Level → Level} {β : Level → Level → Level} {γ : Level → Level}
  (L : Large-Meet-Semilattice α β)
  (S : Large-Subposet γ (large-poset-Large-Meet-Semilattice L))
  where

  contains-top-Large-Subposet : UU (γ lzero)
  contains-top-Large-Subposet =
    is-in-Large-Subposet
      ( large-poset-Large-Meet-Semilattice L)
      ( S)
      ( top-Large-Meet-Semilattice L)

The predicate that a large subposet is a large meet-subsemilattice

module _
  {α : Level → Level} {β : Level → Level → Level} {γ : Level → Level}
  (L : Large-Meet-Semilattice α β)
  (S : Large-Subposet γ (large-poset-Large-Meet-Semilattice L))
  where

  record
    is-large-meet-subsemilattice-Large-Subposet : UUω
    where
    field
      is-closed-under-meets-is-large-meet-subsemilattice-Large-Subposet :
        is-closed-under-meets-Large-Subposet L S
      contains-top-is-large-meet-subsemilattice-Large-Poset :
        contains-top-Large-Subposet L S

  open is-large-meet-subsemilattice-Large-Subposet public

Large meet-subsemilattices

module _
  {α : Level → Level} {β : Level → Level → Level} (γ : Level → Level)
  (L : Large-Meet-Semilattice α β)
  where

  record
    Large-Meet-Subsemilattice : UUω
    where
    field
      large-subposet-Large-Meet-Subsemilattice :
        Large-Subposet γ (large-poset-Large-Meet-Semilattice L)
      is-closed-under-meets-Large-Meet-Subsemilattice :
        is-closed-under-meets-Large-Subposet L
          ( large-subposet-Large-Meet-Subsemilattice)
      contains-top-Large-Meet-Subsemilattice :
        contains-top-Large-Subposet L
          ( large-subposet-Large-Meet-Subsemilattice)

  open Large-Meet-Subsemilattice public

module _
  {α : Level → Level} {β : Level → Level → Level} {γ : Level → Level}
  (L : Large-Meet-Semilattice α β)
  (S : Large-Meet-Subsemilattice γ L)
  where

  large-poset-Large-Meet-Subsemilattice :
    Large-Poset (λ l → α l ⊔ γ l) β
  large-poset-Large-Meet-Subsemilattice =
    large-poset-Large-Subposet
      ( large-poset-Large-Meet-Semilattice L)
      ( large-subposet-Large-Meet-Subsemilattice S)

  large-preorder-Large-Meet-Subsemilattice :
    Large-Preorder (λ l → α l ⊔ γ l) (λ l1 l2 → β l1 l2)
  large-preorder-Large-Meet-Subsemilattice =
    large-preorder-Large-Subposet
      ( large-poset-Large-Meet-Semilattice L)
      ( large-subposet-Large-Meet-Subsemilattice S)

  is-in-Large-Meet-Subsemilattice :
    {l1 : Level} → type-Large-Meet-Semilattice L l1 → UU (γ l1)
  is-in-Large-Meet-Subsemilattice =
    is-in-Large-Subposet
      ( large-poset-Large-Meet-Semilattice L)
      ( large-subposet-Large-Meet-Subsemilattice S)

  type-Large-Meet-Subsemilattice : (l1 : Level) → UU (α l1 ⊔ γ l1)
  type-Large-Meet-Subsemilattice =
    type-Large-Subposet
      ( large-poset-Large-Meet-Semilattice L)
      ( large-subposet-Large-Meet-Subsemilattice S)

  leq-prop-Large-Meet-Subsemilattice :
    Large-Relation-Prop β type-Large-Meet-Subsemilattice
  leq-prop-Large-Meet-Subsemilattice =
    leq-prop-Large-Subposet
      ( large-poset-Large-Meet-Semilattice L)
      ( large-subposet-Large-Meet-Subsemilattice S)

  leq-Large-Meet-Subsemilattice :
    Large-Relation β type-Large-Meet-Subsemilattice
  leq-Large-Meet-Subsemilattice =
    leq-Large-Subposet
      ( large-poset-Large-Meet-Semilattice L)
      ( large-subposet-Large-Meet-Subsemilattice S)

  is-prop-leq-Large-Meet-Subsemilattice :
    is-prop-Large-Relation
      ( type-Large-Meet-Subsemilattice)
      ( leq-Large-Meet-Subsemilattice)
  is-prop-leq-Large-Meet-Subsemilattice =
    is-prop-leq-Large-Subposet
      ( large-poset-Large-Meet-Semilattice L)
      ( large-subposet-Large-Meet-Subsemilattice S)

  refl-leq-Large-Meet-Subsemilattice :
    is-reflexive-Large-Relation
      ( type-Large-Meet-Subsemilattice)
      ( leq-Large-Meet-Subsemilattice)
  refl-leq-Large-Meet-Subsemilattice =
    refl-leq-Large-Subposet
      ( large-poset-Large-Meet-Semilattice L)
      ( large-subposet-Large-Meet-Subsemilattice S)

  transitive-leq-Large-Meet-Subsemilattice :
    is-transitive-Large-Relation
      ( type-Large-Meet-Subsemilattice)
      ( leq-Large-Meet-Subsemilattice)
  transitive-leq-Large-Meet-Subsemilattice =
    transitive-leq-Large-Subposet
      ( large-poset-Large-Meet-Semilattice L)
      ( large-subposet-Large-Meet-Subsemilattice S)

  antisymmetric-leq-Large-Meet-Subsemilattice :
    is-antisymmetric-Large-Relation
      ( type-Large-Meet-Subsemilattice)
      ( leq-Large-Meet-Subsemilattice)
  antisymmetric-leq-Large-Meet-Subsemilattice =
    antisymmetric-leq-Large-Subposet
      ( large-poset-Large-Meet-Semilattice L)
      ( large-subposet-Large-Meet-Subsemilattice S)

  is-closed-under-sim-Large-Meet-Subsemilattice :
    {l1 l2 : Level}
    (x : type-Large-Meet-Semilattice L l1)
    (y : type-Large-Meet-Semilattice L l2) →
    leq-Large-Meet-Semilattice L x y →
    leq-Large-Meet-Semilattice L y x →
    is-in-Large-Meet-Subsemilattice x →
    is-in-Large-Meet-Subsemilattice y
  is-closed-under-sim-Large-Meet-Subsemilattice =
    is-closed-under-sim-Large-Subposet
      ( large-subposet-Large-Meet-Subsemilattice S)

  meet-Large-Meet-Subsemilattice :
    {l1 l2 : Level}
    (x : type-Large-Meet-Subsemilattice l1)
    (y : type-Large-Meet-Subsemilattice l2) →
    type-Large-Meet-Subsemilattice (l1 ⊔ l2)
  pr1 (meet-Large-Meet-Subsemilattice (x , p) (y , q)) =
    meet-Large-Meet-Semilattice L x y
  pr2 (meet-Large-Meet-Subsemilattice (x , p) (y , q)) =
    is-closed-under-meets-Large-Meet-Subsemilattice S x y p q

  is-greatest-binary-lower-bound-meet-Large-Meet-Subsemilattice :
    {l1 l2 : Level}
    (x : type-Large-Meet-Subsemilattice l1)
    (y : type-Large-Meet-Subsemilattice l2) →
    is-greatest-binary-lower-bound-Large-Poset
      ( large-poset-Large-Meet-Subsemilattice)
      ( x)
      ( y)
      ( meet-Large-Meet-Subsemilattice x y)
  is-greatest-binary-lower-bound-meet-Large-Meet-Subsemilattice
    (x , p) (y , q) (z , r) =
    is-greatest-binary-lower-bound-meet-Large-Meet-Semilattice L x y z

  has-meets-Large-Meet-Subsemilattice :
    has-meets-Large-Poset
      ( large-poset-Large-Meet-Subsemilattice)
  meet-has-meets-Large-Poset
    has-meets-Large-Meet-Subsemilattice =
    meet-Large-Meet-Subsemilattice
  is-greatest-binary-lower-bound-meet-has-meets-Large-Poset
    has-meets-Large-Meet-Subsemilattice =
    is-greatest-binary-lower-bound-meet-Large-Meet-Subsemilattice

  top-Large-Meet-Subsemilattice :
    type-Large-Meet-Subsemilattice lzero
  pr1 top-Large-Meet-Subsemilattice = top-Large-Meet-Semilattice L
  pr2 top-Large-Meet-Subsemilattice = contains-top-Large-Meet-Subsemilattice S

  is-top-element-top-Large-Meet-Subsemilattice :
    {l1 : Level} (x : type-Large-Meet-Subsemilattice l1) →
    leq-Large-Meet-Subsemilattice x top-Large-Meet-Subsemilattice
  is-top-element-top-Large-Meet-Subsemilattice (x , p) =
    is-top-element-top-Large-Meet-Semilattice L x

  has-top-element-Large-Meet-Subsemilattice :
    has-top-element-Large-Poset
      ( large-poset-Large-Meet-Subsemilattice)
  top-has-top-element-Large-Poset
    has-top-element-Large-Meet-Subsemilattice =
    top-Large-Meet-Subsemilattice
  is-top-element-top-has-top-element-Large-Poset
    has-top-element-Large-Meet-Subsemilattice =
    is-top-element-top-Large-Meet-Subsemilattice

  is-large-meet-semilattice-Large-Meet-Subsemilattice :
    is-large-meet-semilattice-Large-Poset
      ( large-poset-Large-Meet-Subsemilattice)
  has-meets-is-large-meet-semilattice-Large-Poset
    is-large-meet-semilattice-Large-Meet-Subsemilattice =
    has-meets-Large-Meet-Subsemilattice
  has-top-element-is-large-meet-semilattice-Large-Poset
    is-large-meet-semilattice-Large-Meet-Subsemilattice =
    has-top-element-Large-Meet-Subsemilattice

  large-meet-semilattice-Large-Meet-Subsemilattice :
    Large-Meet-Semilattice (λ l → α l ⊔ γ l) β
  large-poset-Large-Meet-Semilattice
    large-meet-semilattice-Large-Meet-Subsemilattice =
    large-poset-Large-Meet-Subsemilattice
  is-large-meet-semilattice-Large-Meet-Semilattice
    large-meet-semilattice-Large-Meet-Subsemilattice =
    is-large-meet-semilattice-Large-Meet-Subsemilattice

Recent changes