# Subsets of groups

Content created by Egbert Rijke, Fredrik Bakke and Maša Žaucer.

Created on 2023-06-08.

module group-theory.subsets-groups where

Imports
open import foundation.large-locale-of-subtypes
open import foundation.sets
open import foundation.universe-levels

open import group-theory.groups

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


## Idea

A subset of a group G is a subtype of the underlying type of G. The large poset of all subsets of G is called the powerset of G.

## Definitions

### The large locale of subsets of a group

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

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


### The large poset of subsets of a group

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

powerset-large-poset-Group :
Large-Poset (λ l2 → l1 ⊔ lsuc l2) (λ l2 l3 → l1 ⊔ l2 ⊔ l3)
powerset-large-poset-Group =
large-poset-Large-Locale (powerset-large-locale-Group G)


### Subsets of groups

subset-Group :
(l : Level) {l1 : Level} (G : Group l1) → UU (lsuc l ⊔ l1)
subset-Group l G = type-Large-Locale (powerset-large-locale-Group G) l

is-set-subset-Group :
{l1 l2 : Level} (G : Group l1) → is-set (subset-Group l2 G)
is-set-subset-Group G =
is-set-type-Large-Locale (powerset-large-locale-Group G)