def AlgebraInLean.Kernel {G : Type u_1} {G' : Type u_2} [AlgebraInLean.Group G] [AlgebraInLean.Group G'] (φ : G → G') (h : AlgebraInLean.Homomorphism φ) : AlgebraInLean.Subgroup G

This naturally leads to the idea of the kernel of a homomorphism. Generally, when a group G acts on a set S, the kernel of the action is defined as {g ∈ G | g ⬝ s = s ∀ s ∈ S}. For a homomorphism φ : G → G', the kernel of φ (kerφ) is defined by {g ∈ G | φ (g) = 𝕖}. Try proving that the kernel of a homomorphism is a subgroup of G.

Equations

• AlgebraInLean.Kernel φ h = { carrier := {g : G | φ g = AlgebraInLean.𝕖}, has_id := ⋯, mul_closure := ⋯, inv_closure := ⋯ }

def AlgebraInLean.Image {G : Type u_1} {G' : Type u_2} [AlgebraInLean.Group G] [AlgebraInLean.Group G'] (φ : G → G') (h : AlgebraInLean.Homomorphism φ) : AlgebraInLean.Subgroup G'

The image of a homomorphism φ is a subgroup of G' (not G as the kernel was) that contains all elements which φ maps to. That is, all elements g' ∈ G' such that there is some element g ∈ G where φ(g) = g'.

Try proving that the image of a homomorphism is a subgroup of G'.

Equations

• AlgebraInLean.Image φ h = { carrier := {x : G' | ∃ (g : G), φ g = x}, has_id := ⋯, mul_closure := ⋯, inv_closure := ⋯ }

@[simp]

theorem AlgebraInLean.conjugate_by_id {G : Type u_1} [AlgebraInLean.Group G] : AlgebraInLean.conjugate AlgebraInLean.𝕖 = id

@[simp]

theorem AlgebraInLean.conjugate_id {G : Type u_1} [AlgebraInLean.Group G] (g : G) : AlgebraInLean.conjugate g AlgebraInLean.𝕖 = AlgebraInLean.𝕖

Secondly, conjugating 𝕖 by any element yields the identity. This uses the op_inv property.

@[simp]

theorem AlgebraInLean.conjugate_op {G : Type u_1} [AlgebraInLean.Group G] (a : G) (b : G) : AlgebraInLean.conjugate (AlgebraInLean.μ a b) = AlgebraInLean.conjugate a ∘ AlgebraInLean.conjugate b

Thirdly, the conjugate of a · b is just conjugate of a composed with conjugate of b.

Can you figure out how g · (a · b) · g⁻¹ = (g · a · g⁻¹) · (g · b · g⁻¹)?

def AlgebraInLean.Conjugate {G : Type u_1} [AlgebraInLean.Group G] (g : G) (S : Set G) : Set G

We'll use capital Conjugate to define conjugating a set by an element g. This notation is equivalent to the set {g · s · g⁻¹ | s ∈ S}, that is {conjugate s | s : S}.

Equations

• AlgebraInLean.Conjugate g S = AlgebraInLean.conjugate g '' S

def AlgebraInLean.normal {G : Type u_1} [AlgebraInLean.Group G] (H : AlgebraInLean.Subgroup G) : Prop

We define a subgroup to be normal if the subgroup is closed under conjugation with any element of G.

Equations

• AlgebraInLean.normal H = ∀ (g h : G), h ∈ H → AlgebraInLean.conjugate g h ∈ H

theorem AlgebraInLean.Minimal_normal {G : Type u_1} [AlgebraInLean.Group G] : AlgebraInLean.normal (AlgebraInLean.Minimal G)

theorem AlgebraInLean.Maximal_normal {G : Type u_1} [AlgebraInLean.Group G] : AlgebraInLean.normal (AlgebraInLean.Maximal G)

theorem AlgebraInLean.Kernel_normal {G : Type u_1} {G' : Type u_2} [AlgebraInLean.Group G] [AlgebraInLean.Group G'] (φ : G → G') (h : AlgebraInLean.Homomorphism φ) : AlgebraInLean.normal (AlgebraInLean.Kernel φ h)

def AlgebraInLean.Normalizer {G : Type u_1} [AlgebraInLean.Group G] (S : Set G) : AlgebraInLean.Subgroup G

The normalizer of a set S (of a group G) is the set of all elements in G that when conjugated with S return S. The normalizer will never be empty since 𝕖 conjugates in such a way. Now show that this subset of G is a subgroup of G.

Equations

• AlgebraInLean.Normalizer S = { carrier := {g : G | ∀ s ∈ S, AlgebraInLean.Conjugate g S = S}, has_id := ⋯, mul_closure := ⋯, inv_closure := ⋯ }

def AlgebraInLean.Centralizer {G : Type u_1} [AlgebraInLean.Group G] (S : Set G) : AlgebraInLean.Subgroup G

The centralizer of a set S (of a group G) is the set of all elements in G that commute with all elements of S. This can be thought of a measure of how close a group is to being abelian.

Equations

• AlgebraInLean.Centralizer S = { carrier := {g : G | ∀ s ∈ S, AlgebraInLean.μ g s = AlgebraInLean.μ s g}, has_id := ⋯, mul_closure := ⋯, inv_closure := ⋯ }

theorem AlgebraInLean.Centralizer_def {G : Type u_1} [AlgebraInLean.Group G] {S : Set G} {a : G} : a ∈ AlgebraInLean.Centralizer S ↔ ∀ s ∈ S, AlgebraInLean.μ a s = AlgebraInLean.μ s a

def AlgebraInLean.Center {G : Type u_1} [AlgebraInLean.Group G] : AlgebraInLean.Subgroup G

Equations

• AlgebraInLean.Center = AlgebraInLean.Centralizer Set.univ

def AlgebraInLean.Abelian {G : Type u_1} [AlgebraInLean.Group G] (H : AlgebraInLean.Subgroup G) : Prop

We have the AbelianGroup type class that we defined in chapter 1, but here we codify a subgroup being abelian into a Prop. This lends itself to nice proofs like the one below.

Equations

• AlgebraInLean.Abelian H = ∀ (x y : G), x ∈ H → y ∈ H → AlgebraInLean.μ x y = AlgebraInLean.μ y x

theorem AlgebraInLean.subgroup_abelian_iff_centralizer_self {G : Type u_1} [AlgebraInLean.Group G] (H : AlgebraInLean.Subgroup G) : H ≤ AlgebraInLean.Centralizer ↑H ↔ AlgebraInLean.Abelian H

theorem AlgebraInLean.homomorphism_inj_iff_kernel_trivial {G : Type u_1} {G' : Type u_2} [AlgebraInLean.Group G] [AlgebraInLean.Group G'] (φ : G → G') (h : AlgebraInLean.Homomorphism φ) : Function.Injective φ ↔ AlgebraInLean.Kernel φ h = AlgebraInLean.Minimal G

theorem AlgebraInLean.homomorphism_surj_iff_image_complete {G : Type u_1} {G' : Type u_2} [AlgebraInLean.Group G] [AlgebraInLean.Group G'] (φ : G → G') (h : AlgebraInLean.Homomorphism φ) : Function.Surjective φ ↔ AlgebraInLean.Image φ h = AlgebraInLean.Maximal G'

theorem AlgebraInLean.subgroup_normalizer_self {G : Type u_1} [AlgebraInLean.Group G] (H : AlgebraInLean.Subgroup G) : H ≤ AlgebraInLean.Normalizer ↑H