Pullbacks of subsemigroups

Content created by Egbert Rijke.

Created on 2023-11-24.
Last modified on 2024-04-25.

module group-theory.pullbacks-subsemigroups where
Imports 
open import foundation.dependent-pair-types
open import foundation.function-types
open import foundation.identity-types
open import foundation.powersets
open import foundation.pullbacks-subtypes
open import foundation.universe-levels

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

open import order-theory.commuting-squares-of-order-preserving-maps-large-posets
open import order-theory.order-preserving-maps-large-posets
open import order-theory.order-preserving-maps-large-preorders
open import order-theory.similarity-of-order-preserving-maps-large-posets

Idea

Given a semigroup homomorphism f : G → H into a semigroup H equipped with a subsemigroup K ≤ H, the pullback pullback f K of K along f is defined by substituting f in K. In other words, it is the subsemigroup pullback f K of G consisting of the elements x : G such that f x ∈ K.

Definitions

The pullback of a subsemigroup along a semigroup homomorphism

module _
  {l1 l2 l3 : Level} (G : Semigroup l1) (H : Semigroup l2)
  (f : hom-Semigroup G H) (K : Subsemigroup l3 H)
  where

  subset-pullback-Subsemigroup : subset-Semigroup l3 G
  subset-pullback-Subsemigroup =
    subset-Subsemigroup H K ∘ map-hom-Semigroup G H f

  is-closed-under-multiplication-pullback-Subsemigroup :
    is-closed-under-multiplication-subset-Semigroup G
      subset-pullback-Subsemigroup
  is-closed-under-multiplication-pullback-Subsemigroup p q =
    is-closed-under-eq-Subsemigroup' H K
      ( is-closed-under-multiplication-Subsemigroup H K p q)
      ( preserves-mul-hom-Semigroup G H f)

  pullback-Subsemigroup : Subsemigroup l3 G
  pr1 pullback-Subsemigroup =
    subset-pullback-Subsemigroup
  pr2 pullback-Subsemigroup =
    is-closed-under-multiplication-pullback-Subsemigroup

  is-in-pullback-Subsemigroup : type-Semigroup G → UU l3
  is-in-pullback-Subsemigroup =
    is-in-Subsemigroup G pullback-Subsemigroup

  is-closed-under-eq-pullback-Subsemigroup :
    {x y : type-Semigroup G} →
    is-in-pullback-Subsemigroup x → x ＝ y → is-in-pullback-Subsemigroup y
  is-closed-under-eq-pullback-Subsemigroup =
    is-closed-under-eq-Subsemigroup G pullback-Subsemigroup

  is-closed-under-eq-pullback-Subsemigroup' :
    {x y : type-Semigroup G} →
    is-in-pullback-Subsemigroup y → x ＝ y → is-in-pullback-Subsemigroup x
  is-closed-under-eq-pullback-Subsemigroup' =
    is-closed-under-eq-Subsemigroup' G pullback-Subsemigroup

The order preserving operation `pullback-Subsemigroup

module _
  {l1 l2 : Level} (G : Semigroup l1) (H : Semigroup l2) (f : hom-Semigroup G H)
  where

  preserves-order-pullback-Subsemigroup :
    {l3 l4 : Level} (S : Subsemigroup l3 H) (T : Subsemigroup l4 H) →
    leq-Subsemigroup H S T →
    leq-Subsemigroup G
      ( pullback-Subsemigroup G H f S)
      ( pullback-Subsemigroup G H f T)
  preserves-order-pullback-Subsemigroup S T =
    preserves-order-pullback-subtype
      ( map-hom-Semigroup G H f)
      ( subset-Subsemigroup H S)
      ( subset-Subsemigroup H T)

  pullback-hom-large-poset-Subsemigroup :
    hom-Large-Poset
      ( λ l → l)
      ( Subsemigroup-Large-Poset H)
      ( Subsemigroup-Large-Poset G)
  map-hom-Large-Preorder pullback-hom-large-poset-Subsemigroup =
    pullback-Subsemigroup G H f
  preserves-order-hom-Large-Preorder pullback-hom-large-poset-Subsemigroup =
    preserves-order-pullback-Subsemigroup

Properties

The pullback operation commutes with the underlying subtype operation

The square

                       pullback f
    Subsemigroup H ----------------> Subsemigroup G
          |                                |
   K ↦ UK |                                | K ↦ UK
          |                                |
          ∨                                ∨
  subset-Semigroup H ------------> subset-Semigroup G
                      pullback f

of order preserving maps commutes by reflexivity.

module _
  {l1 l2 : Level} (G : Semigroup l1) (H : Semigroup l2) (f : hom-Semigroup G H)
  where

  coherence-square-pullback-subset-Subsemigroup :
    coherence-square-hom-Large-Poset
      ( Subsemigroup-Large-Poset H)
      ( powerset-Large-Poset (type-Semigroup H))
      ( Subsemigroup-Large-Poset G)
      ( powerset-Large-Poset (type-Semigroup G))
      ( pullback-hom-large-poset-Subsemigroup G H f)
      ( subset-subsemigroup-hom-large-poset-Semigroup H)
      ( subset-subsemigroup-hom-large-poset-Semigroup G)
      ( pullback-subtype-hom-Large-Poset (map-hom-Semigroup G H f))
  coherence-square-pullback-subset-Subsemigroup =
    refl-sim-hom-Large-Poset
      ( Subsemigroup-Large-Poset H)
      ( powerset-Large-Poset (type-Semigroup G))
      ( comp-hom-Large-Poset
        ( Subsemigroup-Large-Poset H)
        ( Subsemigroup-Large-Poset G)
        ( powerset-Large-Poset (type-Semigroup G))
        ( subset-subsemigroup-hom-large-poset-Semigroup G)
        ( pullback-hom-large-poset-Subsemigroup G H f))

Recent changes