Intersections of subgroups of groups

Content created by Egbert Rijke, Fredrik Bakke, Maša Žaucer and Gregor Perčič.

Created on 2023-06-08.
Last modified on 2023-11-24.

module group-theory.intersections-subgroups-groups where
Imports 
open import foundation.dependent-pair-types
open import foundation.intersections-subtypes
open import foundation.subtypes
open import foundation.universe-levels

open import group-theory.groups
open import group-theory.subgroups
open import group-theory.subsets-groups

open import order-theory.greatest-lower-bounds-large-posets

Idea

The intersection of two subgroups H, K ≤ G is again closed under the group operations, and is therefore a subgroup of G.

Definitions

The intersection of two subgroups

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

  subset-intersection-Subgroup :
    subset-Group (l2 ⊔ l3) G
  subset-intersection-Subgroup =
    intersection-subtype (subset-Subgroup G H) (subset-Subgroup G K)

  is-in-intersection-Subgroup :
    type-Group G → UU (l2 ⊔ l3)
  is-in-intersection-Subgroup =
    is-in-subtype subset-intersection-Subgroup

  contains-unit-intersection-Subgroup :
    is-in-intersection-Subgroup (unit-Group G)
  pr1 contains-unit-intersection-Subgroup = contains-unit-Subgroup G H
  pr2 contains-unit-intersection-Subgroup = contains-unit-Subgroup G K

  is-closed-under-multiplication-intersection-Subgroup :
    {x y : type-Group G} →
    is-in-intersection-Subgroup x →
    is-in-intersection-Subgroup y →
    is-in-intersection-Subgroup (mul-Group G x y)
  pr1
    ( is-closed-under-multiplication-intersection-Subgroup
      ( pH , pK)
      ( qH , qK)) =
    is-closed-under-multiplication-Subgroup G H pH qH
  pr2
    ( is-closed-under-multiplication-intersection-Subgroup
      ( pH , pK)
      ( qH , qK)) =
    is-closed-under-multiplication-Subgroup G K pK qK

  is-closed-under-inverses-intersection-Subgroup :
    {x : type-Group G} →
    is-in-intersection-Subgroup x → is-in-intersection-Subgroup (inv-Group G x)
  pr1 (is-closed-under-inverses-intersection-Subgroup (pH , pK)) =
    is-closed-under-inverses-Subgroup G H pH
  pr2 (is-closed-under-inverses-intersection-Subgroup (pH , pK)) =
    is-closed-under-inverses-Subgroup G K pK

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

  intersection-Subgroup : Subgroup (l2 ⊔ l3) G
  pr1 intersection-Subgroup = subset-intersection-Subgroup
  pr2 intersection-Subgroup = is-subgroup-intersection-Subgroup

The intersection of a family of subgroups

module _
  {l1 l2 l3 : Level} (G : Group l1) {I : UU l2} (H : I → Subgroup l3 G)
  where

  subset-intersection-family-of-subgroups-Group : subset-Group (l2 ⊔ l3) G
  subset-intersection-family-of-subgroups-Group =
    intersection-family-of-subtypes (λ i → subset-Subgroup G (H i))

  is-in-intersection-family-of-subgroups-Group : type-Group G → UU (l2 ⊔ l3)
  is-in-intersection-family-of-subgroups-Group =
    is-in-subtype subset-intersection-family-of-subgroups-Group

  contains-unit-intersection-family-of-subgroups-Group :
    contains-unit-subset-Group G subset-intersection-family-of-subgroups-Group
  contains-unit-intersection-family-of-subgroups-Group i =
    contains-unit-Subgroup G (H i)

  is-closed-under-multiplication-intersection-family-of-subgroups-Group :
    is-closed-under-multiplication-subset-Group G
      subset-intersection-family-of-subgroups-Group
  is-closed-under-multiplication-intersection-family-of-subgroups-Group p q i =
    is-closed-under-multiplication-Subgroup G (H i) (p i) (q i)

  is-closed-under-inverses-intersection-family-of-subgroups-Group :
    is-closed-under-inverses-subset-Group G
      subset-intersection-family-of-subgroups-Group
  is-closed-under-inverses-intersection-family-of-subgroups-Group p i =
    is-closed-under-inverses-Subgroup G (H i) (p i)

  is-subgroup-intersection-family-of-subgroups-Group :
    is-subgroup-subset-Group G subset-intersection-family-of-subgroups-Group
  pr1 is-subgroup-intersection-family-of-subgroups-Group =
    contains-unit-intersection-family-of-subgroups-Group
  pr1 (pr2 is-subgroup-intersection-family-of-subgroups-Group) =
    is-closed-under-multiplication-intersection-family-of-subgroups-Group
  pr2 (pr2 is-subgroup-intersection-family-of-subgroups-Group) =
    is-closed-under-inverses-intersection-family-of-subgroups-Group

  intersection-family-of-subgroups-Group : Subgroup (l2 ⊔ l3) G
  pr1 intersection-family-of-subgroups-Group =
    subset-intersection-family-of-subgroups-Group
  pr2 intersection-family-of-subgroups-Group =
    is-subgroup-intersection-family-of-subgroups-Group

Properties

The intersection of H and K is the greatest binary lower bound of H and K in the poset of subgroups of G

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

  is-greatest-binary-lower-bound-intersection-Subgroup :
    is-greatest-binary-lower-bound-Large-Poset
      ( Subgroup-Large-Poset G)
      ( H)
      ( K)
      ( intersection-Subgroup G H K)
  is-greatest-binary-lower-bound-intersection-Subgroup L =
    is-greatest-binary-lower-bound-intersection-subtype
      ( subset-Subgroup G H)
      ( subset-Subgroup G K)
      ( subset-Subgroup G L)

Recent changes