Submonoids

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides and Maša Žaucer.

Created on 2022-08-16.
Last modified on 2024-02-06.

module group-theory.submonoids where
Imports 
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.function-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.subtype-identity-principle
open import foundation.subtypes
open import foundation.universe-levels

open import group-theory.homomorphisms-monoids
open import group-theory.monoids
open import group-theory.semigroups
open import group-theory.subsets-monoids

Idea

A submonoid of a monoid M is a subset of M that contains the unit of M and is closed under multiplication.

Definitions

Submonoids

is-submonoid-prop-subset-Monoid :
  {l1 l2 : Level} (M : Monoid l1) (P : subset-Monoid l2 M) →
  Prop (l1 ⊔ l2)
is-submonoid-prop-subset-Monoid M P =
  product-Prop
    ( contains-unit-prop-subset-Monoid M P)
    ( is-closed-under-multiplication-prop-subset-Monoid M P)

is-submonoid-subset-Monoid :
  {l1 l2 : Level} (M : Monoid l1) (P : subset-Monoid l2 M) → UU (l1 ⊔ l2)
is-submonoid-subset-Monoid M P =
  type-Prop (is-submonoid-prop-subset-Monoid M P)

Submonoid :
  {l1 : Level} (l2 : Level) (M : Monoid l1) → UU (l1 ⊔ lsuc l2)
Submonoid l2 M =
  type-subtype (is-submonoid-prop-subset-Monoid {l2 = l2} M)

module _
  {l1 l2 : Level} (M : Monoid l1) (P : Submonoid l2 M)
  where

  subset-Submonoid : subtype l2 (type-Monoid M)
  subset-Submonoid =
    inclusion-subtype (is-submonoid-prop-subset-Monoid M) P

  is-submonoid-Submonoid : is-submonoid-subset-Monoid M subset-Submonoid
  is-submonoid-Submonoid = pr2 P

  is-in-Submonoid : type-Monoid M → UU l2
  is-in-Submonoid = is-in-subtype subset-Submonoid

  is-prop-is-in-Submonoid :
    (x : type-Monoid M) → is-prop (is-in-Submonoid x)
  is-prop-is-in-Submonoid =
    is-prop-is-in-subtype subset-Submonoid

  is-closed-under-eq-Submonoid :
    {x y : type-Monoid M} → is-in-Submonoid x → (x ＝ y) → is-in-Submonoid y
  is-closed-under-eq-Submonoid = is-closed-under-eq-subtype subset-Submonoid

  is-closed-under-eq-Submonoid' :
    {x y : type-Monoid M} → is-in-Submonoid y → (x ＝ y) → is-in-Submonoid x
  is-closed-under-eq-Submonoid' = is-closed-under-eq-subtype' subset-Submonoid

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

  is-set-type-Submonoid : is-set type-Submonoid
  is-set-type-Submonoid =
    is-set-type-subset-Monoid M subset-Submonoid

  set-Submonoid : Set (l1 ⊔ l2)
  set-Submonoid =
    set-subset-Monoid M subset-Submonoid

  inclusion-Submonoid :
    type-Submonoid → type-Monoid M
  inclusion-Submonoid =
    inclusion-subtype subset-Submonoid

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

  is-in-submonoid-inclusion-Submonoid :
    (x : type-Submonoid) →
    is-in-Submonoid (inclusion-Submonoid x)
  is-in-submonoid-inclusion-Submonoid =
    is-in-subtype-inclusion-subtype subset-Submonoid

  contains-unit-Submonoid : is-in-Submonoid (unit-Monoid M)
  contains-unit-Submonoid = pr1 (pr2 P)

  unit-Submonoid : type-Submonoid
  pr1 unit-Submonoid = unit-Monoid M
  pr2 unit-Submonoid = contains-unit-Submonoid

  is-closed-under-multiplication-Submonoid :
    {x y : type-Monoid M} →
    is-in-Submonoid x → is-in-Submonoid y →
    is-in-Submonoid (mul-Monoid M x y)
  is-closed-under-multiplication-Submonoid {x} {y} = pr2 (pr2 P) x y

  mul-Submonoid : (x y : type-Submonoid) → type-Submonoid
  pr1 (mul-Submonoid x y) =
    mul-Monoid M (inclusion-Submonoid x) (inclusion-Submonoid y)
  pr2 (mul-Submonoid x y) =
    is-closed-under-multiplication-Submonoid
      ( is-in-submonoid-inclusion-Submonoid x)
      ( is-in-submonoid-inclusion-Submonoid y)

  associative-mul-Submonoid :
    (x y z : type-Submonoid) →
    (mul-Submonoid (mul-Submonoid x y) z) ＝
    (mul-Submonoid x (mul-Submonoid y z))
  associative-mul-Submonoid x y z =
    eq-type-subtype
      ( subset-Submonoid)
      ( associative-mul-Monoid M
        ( inclusion-Submonoid x)
        ( inclusion-Submonoid y)
        ( inclusion-Submonoid z))

  semigroup-Submonoid : Semigroup (l1 ⊔ l2)
  pr1 semigroup-Submonoid = set-Submonoid
  pr1 (pr2 semigroup-Submonoid) = mul-Submonoid
  pr2 (pr2 semigroup-Submonoid) = associative-mul-Submonoid

  left-unit-law-mul-Submonoid :
    (x : type-Submonoid) → mul-Submonoid unit-Submonoid x ＝ x
  left-unit-law-mul-Submonoid x =
    eq-type-subtype
      ( subset-Submonoid)
      ( left-unit-law-mul-Monoid M (inclusion-Submonoid x))

  right-unit-law-mul-Submonoid :
    (x : type-Submonoid) → mul-Submonoid x unit-Submonoid ＝ x
  right-unit-law-mul-Submonoid x =
    eq-type-subtype
      ( subset-Submonoid)
      ( right-unit-law-mul-Monoid M (inclusion-Submonoid x))

  monoid-Submonoid : Monoid (l1 ⊔ l2)
  pr1 monoid-Submonoid = semigroup-Submonoid
  pr1 (pr2 monoid-Submonoid) = unit-Submonoid
  pr1 (pr2 (pr2 monoid-Submonoid)) = left-unit-law-mul-Submonoid
  pr2 (pr2 (pr2 monoid-Submonoid)) = right-unit-law-mul-Submonoid

  preserves-unit-inclusion-Submonoid :
    inclusion-Submonoid unit-Submonoid ＝ unit-Monoid M
  preserves-unit-inclusion-Submonoid = refl

  preserves-mul-inclusion-Submonoid :
    {x y : type-Submonoid} →
    inclusion-Submonoid (mul-Submonoid x y) ＝
    mul-Monoid M (inclusion-Submonoid x) (inclusion-Submonoid y)
  preserves-mul-inclusion-Submonoid = refl

  hom-inclusion-Submonoid :
    hom-Monoid monoid-Submonoid M
  pr1 (pr1 hom-inclusion-Submonoid) =
    inclusion-Submonoid
  pr2 (pr1 hom-inclusion-Submonoid) {x} {y} =
    preserves-mul-inclusion-Submonoid {x} {y}
  pr2 hom-inclusion-Submonoid = preserves-unit-inclusion-Submonoid

Properties

Extensionality of the type of all submonoids

module _
  {l1 l2 : Level} (M : Monoid l1) (N : Submonoid l2 M)
  where

  has-same-elements-Submonoid :
    {l3 : Level} → Submonoid l3 M → UU (l1 ⊔ l2 ⊔ l3)
  has-same-elements-Submonoid K =
    has-same-elements-subtype (subset-Submonoid M N) (subset-Submonoid M K)

  extensionality-Submonoid :
    (K : Submonoid l2 M) → (N ＝ K) ≃ has-same-elements-Submonoid K
  extensionality-Submonoid =
    extensionality-type-subtype
      ( is-submonoid-prop-subset-Monoid M)
      ( is-submonoid-Submonoid M N)
      ( λ x → pair id id)
      ( extensionality-subtype (subset-Submonoid M N))

Recent changes