structure AlgebraInLean.Subgroup (G : Type u_1) [AlgebraInLean.Group G] : Type u_1

If G is a group, then a subgroup H of G is a subset of G along with G's operation satisfying three properties:

1. The identity in G is the identity in H (H is therefore nonempty)
2. ∀ a, b ∈ H then μ a b ∈ H
3. ∀ a ∈ H, then ι a ∈ H

If H is a subgroup of G, we write H ≤ G (we will explore why this notation is used in Sheet 4). We encode a subgroup as a Lean structure, notably not as a type class, to emphasize that subgroups are simply subsets of groups satisfying specific properties.

• carrier : Set G

  We represent the subgroup's underlying set using Mathlib's Set type. Upon viewing the Mathlib documentation for the set (if you are viewing this file in Visual Studio Code, you may Ctrl-Click on the keyword to consult its definiton), we see that it is merely a wrapper for G → Prop, meaning it is a function that determines what is and is not in the set.

• has_id : AlgebraInLean.𝕖 ∈ ↑self

  This proposition asserts that the subgroup contains the identity of G. This also asserts that the subgroup is not the empty set.

• mul_closure : ∀ {a b : G}, a ∈ ↑self → b ∈ ↑self → AlgebraInLean.μ a b ∈ ↑self

  The below propositions assert that the subgroup is closed under the group operation μ and the inverse function ι.

• inv_closure : ∀ {a : G}, a ∈ ↑self → AlgebraInLean.ι a ∈ ↑self

theorem AlgebraInLean.Subgroup.has_id {G : Type u_1} [AlgebraInLean.Group G] (self : AlgebraInLean.Subgroup G) : AlgebraInLean.𝕖 ∈ ↑self

This proposition asserts that the subgroup contains the identity of G. This also asserts that the subgroup is not the empty set.

theorem AlgebraInLean.Subgroup.mul_closure {G : Type u_1} [AlgebraInLean.Group G] (self : AlgebraInLean.Subgroup G) {a : G} {b : G} : a ∈ ↑self → b ∈ ↑self → AlgebraInLean.μ a b ∈ ↑self

The below propositions assert that the subgroup is closed under the group operation μ and the inverse function ι.

theorem AlgebraInLean.Subgroup.inv_closure {G : Type u_1} [AlgebraInLean.Group G] (self : AlgebraInLean.Subgroup G) {a : G} : a ∈ ↑self → AlgebraInLean.ι a ∈ ↑self

instance AlgebraInLean.instCoeSubgroupSet {G : Type u_1} [AlgebraInLean.Group G] : Coe (AlgebraInLean.Subgroup G) (Set G)

This instance coerces Subgroup G to Set G by extracting the underlying set.

Equations

• AlgebraInLean.instCoeSubgroupSet = { coe := fun (H : AlgebraInLean.Subgroup G) => ↑H }

instance AlgebraInLean.instCoeSortSubgroupType {G : Type u_1} [AlgebraInLean.Group G] : CoeSort (AlgebraInLean.Subgroup G) (Type u_1)

Equations

• AlgebraInLean.instCoeSortSubgroupType = { coe := fun (H : AlgebraInLean.Subgroup G) => ↑↑H }

instance AlgebraInLean.instMembershipSubgroup {G : Type u_1} [AlgebraInLean.Group G] : Membership G (AlgebraInLean.Subgroup G)

This notation allows us to use the element-of symbol (∈) for subgroups.

Equations

• AlgebraInLean.instMembershipSubgroup = { mem := fun (g : G) (H : AlgebraInLean.Subgroup G) => g ∈ ↑H }

instance AlgebraInLean.instGroupElemCarrier {G : Type u_1} [AlgebraInLean.Group G] {H : AlgebraInLean.Subgroup G} : AlgebraInLean.Group ↑↑H

The instances above allow us to assert that H : Subgroup G is itself a group. We do this by implementing our Group interface on all H. As you complete the proofs yourself, you will notice that many of the properties are inherited from the parent group's structure, so the mere assertion of closure of H under μ and ι are sufficient to prove that H is a group!

Equations

• AlgebraInLean.instGroupElemCarrier = AlgebraInLean.Group.mk (fun (x : ↑↑H) => match x with | ⟨a, ha⟩ => ⟨AlgebraInLean.ι a, ⋯⟩) ⋯

def AlgebraInLean.Maximal (G : Type u_2) [AlgebraInLean.Group G] : AlgebraInLean.Subgroup G

The largest possible subgroup of G contains every element of G. We call this subgroup the Maximal subgroup.

Equations

• AlgebraInLean.Maximal G = { carrier := Set.univ, has_id := trivial, mul_closure := ⋯, inv_closure := ⋯ }

def AlgebraInLean.Minimal (G : Type u_2) [AlgebraInLean.Group G] : AlgebraInLean.Subgroup G

The smallest possible subgroup of G is called the Minimal subgroup. Consider what this smallest subgroup would be, and then complete the proof that the set you choose is a subgroup.

Equations

• AlgebraInLean.Minimal G = { carrier := {AlgebraInLean.𝕖}, has_id := ⋯, mul_closure := ⋯, inv_closure := ⋯ }

theorem AlgebraInLean.ext {G : Type u_1} [AlgebraInLean.Group G] (H : AlgebraInLean.Subgroup G) (K : AlgebraInLean.Subgroup G) (h : ↑H = ↑K) : H = K

This theorem here is an extensionality theorem, which enables us to use the ext tactic on equality of subgroups.

def AlgebraInLean.Subgroup_Criterion {G : Type u_1} [AlgebraInLean.Group G] (S : Set G) (he : ∃ (s : G), s ∈ S) (hc : ∀ (x y : G), x ∈ S → y ∈ S → AlgebraInLean.μ x (AlgebraInLean.ι y) ∈ S) : AlgebraInLean.Subgroup G

We have defined a subgroup to be a subset of a group that is closed under each of the group operations and contains the group identity. Here, we show that we can derive these three properties from the two properties below.

1. H ≠ ∅
2. for all x, y ∈ H, μ x (ι y) ∈ H

Equations

• AlgebraInLean.Subgroup_Criterion S he hc = { carrier := S, has_id := ⋯, mul_closure := ⋯, inv_closure := ⋯ }