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
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


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



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 =
    ( 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)

  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-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 =
      ( 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 =
      ( 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 =
      ( 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) =
  pr2 (pr1 hom-inclusion-Submonoid) {x} {y} =
    preserves-mul-inclusion-Submonoid {x} {y}
  pr2 hom-inclusion-Submonoid = preserves-unit-inclusion-Submonoid


Extensionality of the type of all submonoids

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

  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 =
      ( is-submonoid-prop-subset-Monoid M)
      ( is-submonoid-Submonoid M N)
      ( λ x  pair id id)
      ( extensionality-subtype (subset-Submonoid M N))

Recent changes