Pullbacks of subgroups

Content created by Egbert Rijke.

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

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

open import group-theory.conjugation
open import group-theory.groups
open import group-theory.homomorphisms-groups
open import group-theory.normal-subgroups
open import group-theory.pullbacks-subsemigroups
open import group-theory.subgroups
open import group-theory.subsemigroups
open import group-theory.subsets-groups

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 group homomorphism f : G → H into a group H equipped with a subgroup K ≤ H, the pullback pullback f K of K along f is defined by substituting f in K. In other words, it is the subgroup pullback f K of G consisting of the elements x : G such that f x ∈ K.

Definitions

Pullbacks of subgroups

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

  subsemigroup-pullback-Subgroup : Subsemigroup l3 (semigroup-Group G)
  subsemigroup-pullback-Subgroup =
    pullback-Subsemigroup
      ( semigroup-Group G)
      ( semigroup-Group H)
      ( f)
      ( subsemigroup-Subgroup H K)

  subset-pullback-Subgroup : subset-Group l3 G
  subset-pullback-Subgroup =
    subset-pullback-Subsemigroup
      ( semigroup-Group G)
      ( semigroup-Group H)
      ( f)
      ( subsemigroup-Subgroup H K)

  is-in-pullback-Subgroup : type-Group G → UU l3
  is-in-pullback-Subgroup =
    is-in-pullback-Subsemigroup
      ( semigroup-Group G)
      ( semigroup-Group H)
      ( f)
      ( subsemigroup-Subgroup H K)

  is-closed-under-eq-pullback-Subgroup :
    {x y : type-Group G} →
    is-in-pullback-Subgroup x → x ＝ y → is-in-pullback-Subgroup y
  is-closed-under-eq-pullback-Subgroup =
    is-closed-under-eq-pullback-Subsemigroup
      ( semigroup-Group G)
      ( semigroup-Group H)
      ( f)
      ( subsemigroup-Subgroup H K)

  is-closed-under-eq-pullback-Subgroup' :
    {x y : type-Group G} →
    is-in-pullback-Subgroup y → x ＝ y → is-in-pullback-Subgroup x
  is-closed-under-eq-pullback-Subgroup' =
    is-closed-under-eq-pullback-Subsemigroup'
      ( semigroup-Group G)
      ( semigroup-Group H)
      ( f)
      ( subsemigroup-Subgroup H K)

  contains-unit-pullback-Subgroup :
    contains-unit-subset-Group G subset-pullback-Subgroup
  contains-unit-pullback-Subgroup =
    is-closed-under-eq-Subgroup' H K
      ( contains-unit-Subgroup H K)
      ( preserves-unit-hom-Group G H f)

  is-closed-under-multiplication-pullback-Subgroup :
    is-closed-under-multiplication-subset-Group G subset-pullback-Subgroup
  is-closed-under-multiplication-pullback-Subgroup =
    is-closed-under-multiplication-pullback-Subsemigroup
      ( semigroup-Group G)
      ( semigroup-Group H)
      ( f)
      ( subsemigroup-Subgroup H K)

  is-closed-under-inverses-pullback-Subgroup :
    is-closed-under-inverses-subset-Group G subset-pullback-Subgroup
  is-closed-under-inverses-pullback-Subgroup p =
    is-closed-under-eq-Subgroup' H K
      ( is-closed-under-inverses-Subgroup H K p)
      ( preserves-inv-hom-Group G H f)

  is-subgroup-pullback-Subgroup :
    is-subgroup-subset-Group G subset-pullback-Subgroup
  pr1 is-subgroup-pullback-Subgroup =
    contains-unit-pullback-Subgroup
  pr1 (pr2 is-subgroup-pullback-Subgroup) =
    is-closed-under-multiplication-pullback-Subgroup
  pr2 (pr2 is-subgroup-pullback-Subgroup) =
    is-closed-under-inverses-pullback-Subgroup

  pullback-Subgroup : Subgroup l3 G
  pr1 pullback-Subgroup = subset-pullback-Subgroup
  pr2 pullback-Subgroup = is-subgroup-pullback-Subgroup

The order preserving map pullback-Subgroup

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

  preserves-order-pullback-Subgroup :
    {l3 l4 : Level} (S : Subgroup l3 H) (T : Subgroup l4 H) →
    leq-Subgroup H S T →
    leq-Subgroup G (pullback-Subgroup G H f S) (pullback-Subgroup G H f T)
  preserves-order-pullback-Subgroup S T =
    preserves-order-pullback-Subsemigroup
      ( semigroup-Group G)
      ( semigroup-Group H)
      ( f)
      ( subsemigroup-Subgroup H S)
      ( subsemigroup-Subgroup H T)

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

Properties

The pullback operation commutes with the underlying subtype operation

The square

                   pullback f
     Subgroup H ----------------> Subgroup G
         |                            |
  K ↦ UK |                            | K ↦ UK
         |                            |
         ∨                            ∨
   subset-Group H ------------> subset-Group G
                   pullback f

of order preserving maps commutes by reflexivity.

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

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

Pullbacks of normal subgroups are normal

module _
  {l1 l2 l3 : Level} (G : Group l1) (H : Group l2) (f : hom-Group G H)
  (N : Normal-Subgroup l3 H)
  where

  subgroup-pullback-Normal-Subgroup : Subgroup l3 G
  subgroup-pullback-Normal-Subgroup =
    pullback-Subgroup G H f (subgroup-Normal-Subgroup H N)

  is-normal-pullback-Normal-Subgroup :
    is-normal-Subgroup G subgroup-pullback-Normal-Subgroup
  is-normal-pullback-Normal-Subgroup x (y , n) =
    is-closed-under-eq-Normal-Subgroup' H N
      ( is-normal-Normal-Subgroup H N
        ( map-hom-Group G H f x)
        ( map-hom-Group G H f y)
        ( n))
      ( preserves-conjugation-hom-Group G H f)

  pullback-Normal-Subgroup : Normal-Subgroup l3 G
  pr1 pullback-Normal-Subgroup = subgroup-pullback-Normal-Subgroup
  pr2 pullback-Normal-Subgroup = is-normal-pullback-Normal-Subgroup

Recent changes