# Centralizer subgroups

Content created by Egbert Rijke and Gregor Perčič.

Created on 2023-08-07.

module group-theory.centralizer-subgroups where
Imports
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.propositions
open import foundation.sets
open import foundation.subtypes
open import foundation.universe-levels

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

## Idea

Consider a subset S of a group G. The centralizer subgroup Cᴳ(S) of S is the subgroup of elements g : G such that gs=sg for every s ∈ S. In other words, it consists of the elements of G that commute with all the elements of S.

The definition of the centralizer is similar, but not identical to the definition of the normalizer. There is an inclusion of the centralizer into the normalizer, but not the other way around. The centralizer should also not be confused with the center of a group.

## Definitions

module _
{l1 l2 : Level} (G : Group l1) (S : subset-Group l2 G)
where

subset-centralizer-subset-Group : subset-Group (l1  l2) G
subset-centralizer-subset-Group x =
Π-Prop
( type-Group G)
( λ y
hom-Prop (S y) (Id-Prop (set-Group G) (conjugation-Group G x y) y))

is-in-centralizer-subset-Group : type-Group G  UU (l1  l2)
is-in-centralizer-subset-Group =
is-in-subtype subset-centralizer-subset-Group

contains-unit-centralizer-subset-Group :
contains-unit-subset-Group G subset-centralizer-subset-Group
contains-unit-centralizer-subset-Group y s =
compute-conjugation-unit-Group G y

is-closed-under-multiplication-centralizer-subset-Group :
is-closed-under-multiplication-subset-Group G
subset-centralizer-subset-Group
is-closed-under-multiplication-centralizer-subset-Group {x} {y} u v z s =
( compute-conjugation-mul-Group G x y z)
( ap (conjugation-Group G x) (v z s))
( u z s)

is-closed-under-inverses-centralizer-subset-Group :
is-closed-under-inverses-subset-Group G subset-centralizer-subset-Group
is-closed-under-inverses-centralizer-subset-Group {x} u y s =
transpose-eq-conjugation-inv-Group G (inv (u y s))

centralizer-subset-Group : Subgroup (l1  l2) G
pr1 centralizer-subset-Group =
subset-centralizer-subset-Group
pr1 (pr2 centralizer-subset-Group) =
contains-unit-centralizer-subset-Group
pr1 (pr2 (pr2 centralizer-subset-Group)) =
is-closed-under-multiplication-centralizer-subset-Group
pr2 (pr2 (pr2 centralizer-subset-Group)) =
is-closed-under-inverses-centralizer-subset-Group