# Large subposets

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

Created on 2023-05-12.

module order-theory.large-subposets where

Imports
open import foundation.dependent-pair-types
open import foundation.large-binary-relations
open import foundation.logical-equivalences
open import foundation.subtypes
open import foundation.universe-levels

open import order-theory.large-posets
open import order-theory.large-preorders
open import order-theory.large-subpreorders


## Idea

A large subposet of a large poset P consists of a subtype S : type-Large-Poset P l1 → Prop (γ l1) for each universe level l1 such that the implication

  ((x ≤ y) ∧ (y ≤ x)) → (x ∈ S → y ∈ S)


holds for every x y : P. Note that for elements of the same universe level, this is automatic by antisymmetry.

## Definition

### The predicate of being closed under similarity

module _
{α γ : Level → Level} {β : Level → Level → Level}
(P : Large-Poset α β) (S : Large-Subpreorder γ (large-preorder-Large-Poset P))
where

is-closed-under-sim-Large-Subpreorder : UUω
is-closed-under-sim-Large-Subpreorder =
{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-in-Large-Subpreorder (large-preorder-Large-Poset P) S x →
is-in-Large-Subpreorder (large-preorder-Large-Poset P) S y


### Large subposets

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

record
Large-Subposet : UUω
where
field
large-subpreorder-Large-Subposet :
Large-Subpreorder γ (large-preorder-Large-Poset P)
is-closed-under-sim-Large-Subposet :
is-closed-under-sim-Large-Subpreorder P large-subpreorder-Large-Subposet

open Large-Subposet public

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

large-preorder-Large-Subposet :
Large-Preorder (λ l → α l ⊔ γ l) (λ l1 l2 → β l1 l2)
large-preorder-Large-Subposet =
large-preorder-Large-Subpreorder
( large-preorder-Large-Poset P)
( large-subpreorder-Large-Subposet S)

is-in-Large-Subposet :
{l1 : Level} → type-Large-Poset P l1 → UU (γ l1)
is-in-Large-Subposet =
is-in-Large-Subpreorder
( large-preorder-Large-Poset P)
( large-subpreorder-Large-Subposet S)

type-Large-Subposet : (l1 : Level) → UU (α l1 ⊔ γ l1)
type-Large-Subposet =
type-Large-Subpreorder
( large-preorder-Large-Poset P)
( large-subpreorder-Large-Subposet S)

leq-prop-Large-Subposet :
Large-Relation-Prop β type-Large-Subposet
leq-prop-Large-Subposet =
leq-prop-Large-Subpreorder
( large-preorder-Large-Poset P)
( large-subpreorder-Large-Subposet S)

leq-Large-Subposet :
Large-Relation β type-Large-Subposet
leq-Large-Subposet =
leq-Large-Subpreorder
( large-preorder-Large-Poset P)
( large-subpreorder-Large-Subposet S)

is-prop-leq-Large-Subposet :
is-prop-Large-Relation type-Large-Subposet leq-Large-Subposet
is-prop-leq-Large-Subposet =
is-prop-leq-Large-Subpreorder
( large-preorder-Large-Poset P)
( large-subpreorder-Large-Subposet S)

refl-leq-Large-Subposet :
is-reflexive-Large-Relation type-Large-Subposet leq-Large-Subposet
refl-leq-Large-Subposet =
refl-leq-Large-Subpreorder
( large-preorder-Large-Poset P)
( large-subpreorder-Large-Subposet S)

transitive-leq-Large-Subposet :
is-transitive-Large-Relation type-Large-Subposet leq-Large-Subposet
transitive-leq-Large-Subposet =
transitive-leq-Large-Subpreorder
( large-preorder-Large-Poset P)
( large-subpreorder-Large-Subposet S)

antisymmetric-leq-Large-Subposet :
is-antisymmetric-Large-Relation type-Large-Subposet leq-Large-Subposet
antisymmetric-leq-Large-Subposet {l1} (x , p) (y , q) H K =
eq-type-subtype
( large-subpreorder-Large-Subposet S {l1})
( antisymmetric-leq-Large-Poset P x y H K)

large-poset-Large-Subposet : Large-Poset (λ l → α l ⊔ γ l) β
large-preorder-Large-Poset
large-poset-Large-Subposet =
large-preorder-Large-Subposet
antisymmetric-leq-Large-Poset
large-poset-Large-Subposet =
antisymmetric-leq-Large-Subposet


### The predicate of having the same elements

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

has-same-elements-Large-Subposet : UUω
has-same-elements-Large-Subposet =
{l : Level} (x : type-Large-Poset P l) →
is-in-Large-Subposet P S x ↔ is-in-Large-Subposet P T x