Subsets of semigroups

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-11-24.
Last modified on 2026-05-02.

module group-theory.subsets-semigroups where
Imports 
open import foundation.dependent-products-propositions
open import foundation.identity-types
open import foundation.large-locale-of-subtypes
open import foundation.powersets
open import foundation.propositions
open import foundation.sets
open import foundation.subtypes
open import foundation.universe-levels

open import group-theory.semigroups

open import order-theory.large-locales
open import order-theory.large-posets

Idea

A subset of a semigroup G is a subtype of the underlying type of the semigroup G. The powerset of a semigroup is the large poset of all subsets of G, i.e., it is the powerset of the underlying set of G.

Definitions

The large locale of subsets of a semigroup

module _
  {l1 : Level} (G : Semigroup l1)
  where

  powerset-large-locale-Semigroup :
    Large-Locale (λ l2 → l1 ⊔ lsuc l2) (λ l2 l3 → l1 ⊔ l2 ⊔ l3) lzero
  powerset-large-locale-Semigroup =
    powerset-Large-Locale (type-Semigroup G)

The large poset of subsets of a semigroup

module _
  {l1 : Level} (G : Semigroup l1)
  where

  powerset-large-poset-Semigroup :
    Large-Poset (λ l → l1 ⊔ lsuc l) (λ l2 l3 → l1 ⊔ l2 ⊔ l3)
  powerset-large-poset-Semigroup = powerset-Large-Poset (type-Semigroup G)

Subsets of semigroups

subset-Semigroup :
  {l1 : Level} (l2 : Level) (G : Semigroup l1) → UU (l1 ⊔ lsuc l2)
subset-Semigroup l2 G = subtype l2 (type-Semigroup G)

module _
  {l1 l2 : Level} (G : Semigroup l1) (P : subset-Semigroup l2 G)
  where

  is-in-subset-Semigroup : type-Semigroup G → UU l2
  is-in-subset-Semigroup = is-in-subtype P

  is-closed-under-eq-subset-Semigroup :
    {x y : type-Semigroup G} →
    is-in-subset-Semigroup x → (x ＝ y) → is-in-subset-Semigroup y
  is-closed-under-eq-subset-Semigroup =
    is-closed-under-eq-subtype P

  is-closed-under-eq-subset-Semigroup' :
    {x y : type-Semigroup G} →
    is-in-subset-Semigroup y → (x ＝ y) → is-in-subset-Semigroup x
  is-closed-under-eq-subset-Semigroup' =
    is-closed-under-eq-subtype' P

  is-prop-is-in-subset-Semigroup :
    (x : type-Semigroup G) → is-prop (is-in-subset-Semigroup x)
  is-prop-is-in-subset-Semigroup = is-prop-is-in-subtype P

  type-subset-Semigroup : UU (l1 ⊔ l2)
  type-subset-Semigroup = type-subtype P

  is-set-type-subset-Semigroup : is-set type-subset-Semigroup
  is-set-type-subset-Semigroup =
    is-set-type-subtype P (is-set-type-Semigroup G)

  set-subset-Semigroup : Set (l1 ⊔ l2)
  set-subset-Semigroup = set-subset (set-Semigroup G) P

  inclusion-subset-Semigroup : type-subset-Semigroup → type-Semigroup G
  inclusion-subset-Semigroup = inclusion-subtype P

  ap-inclusion-subset-Semigroup :
    (x y : type-subset-Semigroup) →
    x ＝ y → (inclusion-subset-Semigroup x ＝ inclusion-subset-Semigroup y)
  ap-inclusion-subset-Semigroup = ap-inclusion-subtype P

  is-in-subset-inclusion-subset-Semigroup :
    (x : type-subset-Semigroup) →
    is-in-subset-Semigroup (inclusion-subset-Semigroup x)
  is-in-subset-inclusion-subset-Semigroup =
    is-in-subtype-inclusion-subtype P

Recent changes