Definition of a group

class MyAlgebra.MyGroup (G : Type u_1) extends Mul G, One G, Inv G : Type u_1

A type $G$ with $\cdot : G \times G \to G$, identity $1$, and inverse $(-)^{-1}$ satisfying associativity, left identity $1 \cdot a = a$, and left inverse $a^{-1} \cdot a = 1$. The right-handed duals follow as theorems.

• mul : G → G → G
• one : G
• inv : G → G
• mul_assoc (a b c : G) : a * b * c = a * (b * c)

  Associativity: $\forall a, b, c,\; (a \cdot b) \cdot c = a \cdot (b \cdot c)$.

• one_mul (a : G) : 1 * a = a

  Left identity: $\forall a,\; 1 \cdot a = a$.

• mul_left_inv (a : G) : a⁻¹ * a = 1

  Left inverse: $\forall a,\; a^{-1} \cdot a = 1$.

Examples of groups

@[implicit_reducible]

instance MyAlgebra.Unit_group : MyGroup Unit

The trivial group: \texttt{Unit} with its single element.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance MyAlgebra.Bool_group : MyGroup Bool

$\mathbb{Z}/2\mathbb{Z}$: \texttt{Bool} under XOR, identity \texttt{false}, every element self-inverse.

Equations

• One or more equations did not get rendered due to their size.

Basic theorems from the axioms

theorem MyAlgebra.mul_left_cancel {G : Type u_1} [MyGroup G] (a b c : G) (h : a * b = a * c) : b = c

$a \cdot b = a \cdot c \;\Longrightarrow\; b = c$.

theorem MyAlgebra.mul_right_inv {G : Type u_1} [MyGroup G] (a : G) : a * a⁻¹ = 1

$\forall a,\; a \cdot a^{-1} = 1$.

theorem MyAlgebra.mul_one {G : Type u_1} [MyGroup G] (a : G) : a * 1 = a

$\forall a,\; a \cdot 1 = a$.

theorem MyAlgebra.mul_right_cancel {G : Type u_1} [MyGroup G] (a b c : G) (h : b * a = c * a) : b = c

$b \cdot a = c \cdot a \;\Longrightarrow\; b = c$.

theorem MyAlgebra.mul_eq_self_iff_right_eq_one {G : Type u_1} [MyGroup G] (a b : G) : a * b = a ↔ b = 1

$a \cdot b = a \;\Longleftrightarrow\; b = 1$ (the second form of the cancellation law).

theorem MyAlgebra.self_eq_mul_iff_left_eq_one {G : Type u_1} [MyGroup G] (a b : G) : b * a = a ↔ b = 1

$b \cdot a = a \;\Longleftrightarrow\; b = 1$ (the dual cancellation statement on the left).

theorem MyAlgebra.one_unique {G : Type u_1} [MyGroup G] (e : G) (h : ∀ (a : G), e * a = a) : e = 1

$(\forall a,\; e \cdot a = a) \;\Longrightarrow\; e = 1$.

theorem MyAlgebra.left_inv_eq_right_inv {G : Type u_1} [MyGroup G] (a ℓ r : G) (hℓ : ℓ * a = 1) (hr : a * r = 1) : ℓ = r

A left inverse and a right inverse of the same element are equal: if $\ell \cdot a = 1$ and $a \cdot r = 1$, then $\ell = r$.

theorem MyAlgebra.inv_unique {G : Type u_1} [MyGroup G] (a b : G) (h : b * a = 1) : b = a⁻¹

$b \cdot a = 1 \;\Longrightarrow\; b = a^{-1}$.

theorem MyAlgebra.mul_eq_iff_eq_mul_inv {G : Type u_1} [MyGroup G] (a b c : G) : a * b = c ↔ a = c * b⁻¹

$a \cdot b = c \;\Longleftrightarrow\; a = c \cdot b^{-1}$ — the basic rearrangement move.

theorem MyAlgebra.inv_inv {G : Type u_1} [MyGroup G] (a : G) : a⁻¹⁻¹ = a

$(a^{-1})^{-1} = a$.

theorem MyAlgebra.one_inv {G : Type u_1} [MyGroup G] : 1⁻¹ = 1

The identity is its own inverse: $1^{-1} = 1$.

theorem MyAlgebra.inv_inj {G : Type u_1} [MyGroup G] (a b : G) (h : a⁻¹ = b⁻¹) : a = b

The inverse map is injective: $a^{-1} = b^{-1} \;\Longrightarrow\; a = b$.

theorem MyAlgebra.mul_inv_rev {G : Type u_1} [MyGroup G] (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹

$(a \cdot b)^{-1} = b^{-1} \cdot a^{-1}$.

theorem MyAlgebra.abelian_of_self_inv {G : Type u_1} [MyGroup G] (h : ∀ (x : G), x * x = 1) (a b : G) : a * b = b * a

$(\forall x,\; x \cdot x = 1) \;\Longrightarrow\; G$ abelian. (Equivalently: a group of exponent $2$ is commutative.)

Natural-number powers

def MyAlgebra.npow {G : Type u_1} [MyGroup G] (g : G) : ℕ → G

$g^n$: product of $n$ copies of $g$ on the right of $1$.

Equations

• MyAlgebra.npow g 0 = 1
• MyAlgebra.npow g n.succ = MyAlgebra.npow g n * g

@[implicit_reducible]

instance MyAlgebra.instHPowNat_abstractAlgebraInLean {G : Type u_1} [MyGroup G] : HPow G ℕ G

Equations

• MyAlgebra.instHPowNat_abstractAlgebraInLean = { hPow := MyAlgebra.npow }

theorem MyAlgebra.pow_zero {G : Type u_1} [MyGroup G] (g : G) : g ^ 0 = 1

$g^0 = 1$.

theorem MyAlgebra.pow_succ {G : Type u_1} [MyGroup G] (g : G) (n : ℕ) : g ^ (n + 1) = g ^ n * g

$g^{n+1} = g^n \cdot g$.

theorem MyAlgebra.pow_add {G : Type u_1} [MyGroup G] (g : G) (m n : ℕ) : g ^ (m + n) = g ^ m * g ^ n

$g^{m+n} = g^m \cdot g^n$.

theorem MyAlgebra.pow_mul {G : Type u_1} [MyGroup G] (g : G) (m n : ℕ) : (g ^ m) ^ n = g ^ (m * n)

$(g^m)^n = g^{m \cdot n}$.

Order of an element

def MyAlgebra.IsOrderOf {G : Type u_1} [MyGroup G] (g : G) (n : ℕ) : Prop

$n > 0 \;\wedge\; g^n = 1 \;\wedge\; (\forall k,\; 0 < k < n \Longrightarrow g^k \neq 1)$.

Equations

• MyAlgebra.IsOrderOf g n = (0 < n ∧ g ^ n = 1 ∧ ∀ (k : ℕ), 0 < k → k < n → g ^ k ≠ 1)

theorem MyAlgebra.isOrderOf_one {G : Type u_1} [MyGroup G] : IsOrderOf 1 1

$\mathrm{IsOrderOf}\, 1\, 1$.

theorem MyAlgebra.isOrderOf_unique {G : Type u_1} [MyGroup G] (g : G) (m n : ℕ) (hm : IsOrderOf g m) (hn : IsOrderOf g n) : m = n

$\mathrm{IsOrderOf}\, g\, m \;\wedge\; \mathrm{IsOrderOf}\, g\, n \;\Longrightarrow\; m = n$.

theorem MyAlgebra.pow_eq_one_iff_dvd_order {G : Type u_1} [MyGroup G] (g : G) {n : ℕ} (hn : IsOrderOf g n) (m : ℕ) : g ^ m = 1 ↔ n ∣ m

If $n$ is the order of $g$, then $g^m = 1 \;\Longleftrightarrow\; n \mid m$.

theorem MyAlgebra.pow_eq_pow_iff_dvd_order_sub {G : Type u_1} [MyGroup G] (g : G) {n : ℕ} (hn : IsOrderOf g n) {k ℓ : ℕ} (hkℓ : k ≤ ℓ) : g ^ k = g ^ ℓ ↔ n ∣ ℓ - k

Proposition 1.3.6(b) (Nat form): for $k \leq \ell$, $g^k = g^\ell \;\Longleftrightarrow\; \mathrm{ord}(g) \mid (\ell - k)$.

theorem MyAlgebra.isOrderOf_pow {G : Type u_1} [MyGroup G] (g : G) {n : ℕ} (hn : IsOrderOf g n) (k : ℕ) : IsOrderOf (g ^ k) (n / n.gcd k)

Proposition 1.3.11: if $\mathrm{ord}(g) = n$, then $\mathrm{ord}(g^k) = n / \gcd(n, k)$.

theorem MyAlgebra.isOrderOf_pow_iff_coprime {G : Type u_1} [MyGroup G] (g : G) {n : ℕ} (hn : IsOrderOf g n) (k : ℕ) : IsOrderOf (g ^ k) n ↔ n.gcd k = 1

Corollary 1.3.12: in $\langle g \rangle$ with $\mathrm{ord}(g) = n$, the power $g^k$ has the same order $n$ — i.e. generates the same cyclic subgroup — iff $\gcd(n, k) = 1$.

Permutations: the canonical non-abelian example

structure MyAlgebra.Perm (α : Type u_1) : Type u_1

A bijection $\alpha \to \alpha$: a forward function paired with a two-sided inverse.

• toFun : α → α
• invFun : α → α
• left_inv (x : α) : self.invFun (self.toFun x) = x
• right_inv (x : α) : self.toFun (self.invFun x) = x

@[implicit_reducible]

instance MyAlgebra.instMulPerm {α : Type u_1} : Mul (Perm α)

$\sigma \cdot \tau := \sigma \circ \tau$ on $\mathrm{Perm}\ \alpha$.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance MyAlgebra.instOnePerm {α : Type u_1} : One (Perm α)

$1 := \mathrm{id}$ on $\mathrm{Perm}\ \alpha$.

Equations

• MyAlgebra.instOnePerm = { one := { toFun := fun (x : α) => x, invFun := fun (x : α) => x, left_inv := ⋯, right_inv := ⋯ } }

@[implicit_reducible]

instance MyAlgebra.instInvPerm {α : Type u_1} : Inv (Perm α)

$\sigma^{-1}$: swap $\sigma.\mathrm{toFun}$ and $\sigma.\mathrm{invFun}$.

Equations

• MyAlgebra.instInvPerm = { inv := fun (σ : MyAlgebra.Perm α) => { toFun := σ.invFun, invFun := σ.toFun, left_inv := ⋯, right_inv := ⋯ } }

theorem MyAlgebra.Perm.ext_of_toFun {α : Type u_1} (σ τ : Perm α) (h : σ.toFun = τ.toFun) : σ = τ

$\sigma.\mathrm{toFun} = \tau.\mathrm{toFun} \;\Longrightarrow\; \sigma = \tau$.

@[implicit_reducible]

instance MyAlgebra.instMyGroupPerm {α : Type u_1} : MyGroup (Perm α)

$\mathrm{Perm}\,\alpha$ is a group under composition.

Equations

• MyAlgebra.instMyGroupPerm = { toMul := MyAlgebra.instMulPerm, toOne := MyAlgebra.instOnePerm, toInv := MyAlgebra.instInvPerm, mul_assoc := ⋯, one_mul := ⋯, mul_left_inv := ⋯ }

def MyAlgebra.swapBool : Perm Bool

The swap on \texttt{Bool}: a concrete permutation exchanging \texttt{true} and \texttt{false}.

Equations

• MyAlgebra.swapBool = { toFun := not, invFun := not, left_inv := MyAlgebra.swapBool._proof_1, right_inv := MyAlgebra.swapBool._proof_1 }

theorem MyAlgebra.swapBool_self_inv : swapBool * swapBool = 1

$\mathrm{swap} \cdot \mathrm{swap} = 1$.

Sign of a permutation

def MyAlgebra.Perm.sgnBool (σ : Perm Bool) : Bool

Sign of a permutation of \texttt{Bool}, valued in \texttt{Bool_group}: identity $\mapsto$ \texttt{false} ($+1$); swap $\mapsto$ \texttt{true} ($-1$).

Equations

• σ.sgnBool = !σ.toFun true

theorem MyAlgebra.Perm.sgnBool_one : sgnBool 1 = false

$\mathrm{sgn}(1) = +1$.

theorem MyAlgebra.Perm.sgnBool_swap : swapBool.sgnBool = true

$\mathrm{sgn}(\mathrm{swap}) = -1$.

theorem MyAlgebra.Perm.sgnBool_mul (σ τ : Perm Bool) : (σ * τ).sgnBool = σ.sgnBool * τ.sgnBool

Sign is a group homomorphism on $\mathrm{Perm}(\mathrm{Bool})$: $\mathrm{sgn}(\sigma \cdot \tau) = \mathrm{sgn}(\sigma) \cdot \mathrm{sgn}(\tau)$ (the right-hand multiplication is XOR in \texttt{Bool_group}).

Dihedral groups

class MyAlgebra.IsDihedral (G : Type u_1) [MyGroup G] (n : ℕ) : Type u_1

A dihedral presentation of degree $n$ on $G$: distinguished generators $r, s$ with $r^n = 1$, $s^2 = 1$, and $s \cdot r = r^{-1} \cdot s$.

• r : G

  Distinguished rotation $r \in G$.

• s : G

  Distinguished reflection $s \in G$.

• r_pow_n : r n ^ n = 1

  $r^n = 1$.

• s_sq : s n * s n = 1

  $s^2 = 1$.

• s_mul_r : s n * r n = (r n)⁻¹ * s n

  $s \cdot r = r^{-1} \cdot s$.

theorem MyAlgebra.IsDihedral.s_eq_inv {G : Type u_1} [MyGroup G] {n : ℕ} (D : IsDihedral G n) : s n = (s n)⁻¹

$s = s^{-1}$: the reflection is an involution.

Abelian groups

class MyAlgebra.MyCommGroup (G : Type u_1) extends MyAlgebra.MyGroup G : Type u_1

A group with $\forall a, b,\; a \cdot b = b \cdot a$.

• mul : G → G → G
• one : G
• inv : G → G
• mul_assoc (a b c : G) : a * b * c = a * (b * c)
• one_mul (a : G) : 1 * a = a
• mul_left_inv (a : G) : a⁻¹ * a = 1
• mul_comm (a b : G) : a * b = b * a

  Commutativity: $\forall a, b,\; a \cdot b = b \cdot a$.

@[implicit_reducible]

instance MyAlgebra.Bool_commGroup : MyCommGroup Bool

\texttt{Bool} is abelian (the smallest non-trivial abelian group, $\mathbb{Z}/2\mathbb{Z}$).

Equations

• MyAlgebra.Bool_commGroup = { toMyGroup := MyAlgebra.Bool_group, mul_comm := MyAlgebra.Bool_commGroup._proof_1 }

theorem MyAlgebra.comm_mul_inv {G : Type u_1} [MyCommGroup G] (a b : G) : (a * b)⁻¹ = a⁻¹ * b⁻¹

$(a \cdot b)^{-1} = a^{-1} \cdot b^{-1}$ in an abelian group.

theorem MyAlgebra.comm_conjugation_trivial {G : Type u_1} [MyCommGroup G] (g h : G) : g * h * g⁻¹ = h

$g \cdot h \cdot g^{-1} = h$ in an abelian group (conjugation is trivial).

theorem MyAlgebra.comm_mul_pow {G : Type u_1} [MyCommGroup G] (g h : G) (n : ℕ) : (g * h) ^ n = g ^ n * h ^ n

$(g \cdot h)^n = g^n \cdot h^n$ in an abelian group.

Subgroups

structure MyAlgebra.MySubgroup (G : Type u_1) [MyGroup G] : Type u_1

A predicate $H : G \to \mathrm{Prop}$ with $1 \in H$, closed under $\cdot$ and $(-)^{-1}$.

• carrier : G → Prop
• one_mem : self.carrier 1
• mul_mem {a b : G} : self.carrier a → self.carrier b → self.carrier (a * b)
• inv_mem {a : G} : self.carrier a → self.carrier a⁻¹

def MyAlgebra.MySubgroup.top {G : Type u_1} [MyGroup G] : MySubgroup G

$\top := G$ (the whole group as a subgroup of itself).

Equations

• MyAlgebra.MySubgroup.top = { carrier := fun (x : G) => True, one_mem := trivial, mul_mem := ⋯, inv_mem := ⋯ }

def MyAlgebra.MySubgroup.bot {G : Type u_1} [MyGroup G] : MySubgroup G

$\bot := \{1\}$ (the trivial subgroup).

Equations

• MyAlgebra.MySubgroup.bot = { carrier := fun (a : G) => a = 1, one_mem := ⋯, mul_mem := ⋯, inv_mem := ⋯ }

def MyAlgebra.MySubgroup.inter {G : Type u_1} [MyGroup G] (H K : MySubgroup G) : MySubgroup G

$H \cap K$ is a subgroup.

Equations

• H.inter K = { carrier := fun (a : G) => H.carrier a ∧ K.carrier a, one_mem := ⋯, mul_mem := ⋯, inv_mem := ⋯ }

theorem MyAlgebra.MySubgroup.criterion {G : Type u_2} [MyGroup G] (P : G → Prop) (hne : ∃ (x : G), P x) (hdiv : ∀ (a b : G), P a → P b → P (a * b⁻¹)) : P 1 ∧ (∀ (a : G), P a → P a⁻¹) ∧ ∀ (a b : G), P a → P b → P (a * b)

Subgroup criterion: a non-empty $P : G \to \mathrm{Prop}$ closed under $a, b \mapsto a \cdot b^{-1}$ is a subgroup. (One-shot test in place of checking $1 \in P$, closure under $\cdot$, closure under $(-)^{-1}$ separately.)

Subgroups generated by a subset

inductive MyAlgebra.MySubgroup.Closure {G : Type u_1} [MyGroup G] (U : G → Prop) : G → Prop

Closure of $U$ under $1$, $\cdot$ and $(-)^{-1}$ — the underlying predicate of $\langle U \rangle$.

• of {G : Type u_1} [MyGroup G] {U : G → Prop} {x : G} : U x → Closure U x
• one {G : Type u_1} [MyGroup G] {U : G → Prop} : Closure U 1
• mul {G : Type u_1} [MyGroup G] {U : G → Prop} {a b : G} : Closure U a → Closure U b → Closure U (a * b)
• inv {G : Type u_1} [MyGroup G] {U : G → Prop} {a : G} : Closure U a → Closure U a⁻¹

def MyAlgebra.MySubgroup.generatedBy {G : Type u_1} [MyGroup G] (U : G → Prop) : MySubgroup G

$\langle U \rangle$: the subgroup generated by $U \subseteq G$.

Equations

• MyAlgebra.MySubgroup.generatedBy U = { carrier := MyAlgebra.MySubgroup.Closure U, one_mem := ⋯, mul_mem := ⋯, inv_mem := ⋯ }

theorem MyAlgebra.MySubgroup.subset_generatedBy {G : Type u_1} [MyGroup G] (U : G → Prop) (x : G) (hx : U x) : (generatedBy U).carrier x

$U \subseteq \langle U \rangle$.

theorem MyAlgebra.MySubgroup.generatedBy_le {G : Type u_1} [MyGroup G] (U : G → Prop) (H : MySubgroup G) (hU : ∀ (x : G), U x → H.carrier x) (x : G) : (generatedBy U).carrier x → H.carrier x

$\langle U \rangle$ is the smallest subgroup containing $U$: $U \subseteq H \;\Longrightarrow\; \langle U \rangle \subseteq H$.

def MyAlgebra.MySubgroup.iInf {G : Type u_1} [MyGroup G] {ι : Type u_2} (H : ι → MySubgroup G) : MySubgroup G

The intersection of an arbitrary family of subgroups is a subgroup.

Equations

• MyAlgebra.MySubgroup.iInf H = { carrier := fun (x : G) => ∀ (i : ι), (H i).carrier x, one_mem := ⋯, mul_mem := ⋯, inv_mem := ⋯ }

Cyclic subgroups

inductive MyAlgebra.MySubgroup.Generated {G : Type u_1} [MyGroup G] (g : G) : G → Prop

The closure of $\{g\}$ under $1$, $\cdot$, and $(-)^{-1}$ — the underlying predicate of $\langle g \rangle$.

• gen {G : Type u_1} [MyGroup G] {g : G} : Generated g g
• one {G : Type u_1} [MyGroup G] {g : G} : Generated g 1
• mul {G : Type u_1} [MyGroup G] {g a b : G} : Generated g a → Generated g b → Generated g (a * b)
• inv {G : Type u_1} [MyGroup G] {g a : G} : Generated g a → Generated g a⁻¹

def MyAlgebra.MySubgroup.cyclic {G : Type u_1} [MyGroup G] (g : G) : MySubgroup G

$\langle g \rangle$: the cyclic subgroup generated by $g$.

Equations

• MyAlgebra.MySubgroup.cyclic g = { carrier := MyAlgebra.MySubgroup.Generated g, one_mem := ⋯, mul_mem := ⋯, inv_mem := ⋯ }

theorem MyAlgebra.MySubgroup.self_mem_cyclic {G : Type u_1} [MyGroup G] (g : G) : (cyclic g).carrier g

$g \in \langle g \rangle$.

theorem MyAlgebra.MySubgroup.npow_mem_cyclic {G : Type u_1} [MyGroup G] (g : G) (n : ℕ) : (cyclic g).carrier (g ^ n)

$\forall n : \mathbb{N},\; g^n \in \langle g \rangle$.

theorem MyAlgebra.MySubgroup.cyclic_le_of_mem {G : Type u_2} [MyGroup G] (g : G) (H : MySubgroup G) (hg : H.carrier g) (x : G) : (cyclic g).carrier x → H.carrier x

Proposition 1.3.3: $\langle g \rangle$ is the smallest subgroup containing $g$. Concretely: any subgroup $H$ containing $g$ also contains $\langle g \rangle$.

def MyAlgebra.IsCyclic (G : Type u_1) [MyGroup G] : Prop

$\exists g \in G,\; \forall x \in G,\; x \in \langle g \rangle$ (i.e. $G = \langle g \rangle$ for some $g$).

Equations

• MyAlgebra.IsCyclic G = ∃ (g : G), ∀ (x : G), (MyAlgebra.MySubgroup.cyclic g).carrier x

theorem MyAlgebra.subgroup_of_cyclic_isCyclic {G : Type u_1} [MyGroup G] (g : G) (H : MySubgroup G) (hH : ∀ (x : G), H.carrier x → (MySubgroup.cyclic g).carrier x) : ∃ (g' : G), H.carrier g' ∧ ∀ (x : G), H.carrier x ↔ (MySubgroup.cyclic g').carrier x

Proposition 1.3.14(a): every subgroup of a cyclic group is cyclic.

Stated for a subgroup $H \subseteq \langle g \rangle$ of an ambient cyclic-style subgroup: there exists $g' \in H$ such that $H = \langle g' \rangle$ — i.e. $H$ is itself cyclic, generated by some element of $H$.

Subgroups of the additive group of integers

structure MyAlgebra.IsAddSubgroupZ (S : ℤ → Prop) : Prop

$S \subseteq \mathbb{Z}$ is an additive subgroup of $(\mathbb{Z}, +)$: closed under $0$, $+$, and negation.

• zero_mem : S 0
• add_mem {a b : ℤ} : S a → S b → S (a + b)
• neg_mem {a : ℤ} : S a → S (-a)

def MyAlgebra.aZ (a : ℤ) : ℤ → Prop

$a\mathbb{Z} := \{\, ka : k \in \mathbb{Z} \,\}$.

Equations

• MyAlgebra.aZ a n = ∃ (k : ℤ), n = k * a

theorem MyAlgebra.aZ_isAddSubgroup (a : ℤ) : IsAddSubgroupZ (aZ a)

$a\mathbb{Z}$ is an additive subgroup of $(\mathbb{Z}, +)$.

theorem MyAlgebra.IsAddSubgroupZ.classification {S : ℤ → Prop} (hS : IsAddSubgroupZ S) : ∃ (a : ℤ), 0 ≤ a ∧ ∀ (n : ℤ), S n ↔ aZ a n

Classification of subgroups of $(\mathbb{Z}, +)$: every additive subgroup equals $a\mathbb{Z}$ for some $a \geq 0$.

Greatest common divisor and least common multiple

def MyAlgebra.addSpanZ (a b : ℤ) : ℤ → Prop

$a\mathbb{Z} + b\mathbb{Z} := \{\, ra + sb : r, s \in \mathbb{Z} \,\}$.

Equations

• MyAlgebra.addSpanZ a b n = ∃ (r : ℤ) (s : ℤ), n = r * a + s * b

theorem MyAlgebra.addSpanZ_isAddSubgroup (a b : ℤ) : IsAddSubgroupZ (addSpanZ a b)

$a\mathbb{Z} + b\mathbb{Z}$ is an additive subgroup of $(\mathbb{Z}, +)$.

theorem MyAlgebra.aZ_inter_isAddSubgroup (a b : ℤ) : IsAddSubgroupZ fun (n : ℤ) => aZ a n ∧ aZ b n

$a\mathbb{Z} \cap b\mathbb{Z}$ is an additive subgroup of $(\mathbb{Z}, +)$.

def MyAlgebra.IsGcd (a b d : ℤ) : Prop

$d$ is \emph{a $\gcd$} of $a, b$: $d \geq 0$ and $d\mathbb{Z} = a\mathbb{Z} + b\mathbb{Z}$.

Equations

• MyAlgebra.IsGcd a b d = (0 ≤ d ∧ ∀ (n : ℤ), MyAlgebra.aZ d n ↔ MyAlgebra.addSpanZ a b n)

def MyAlgebra.IsLcm (a b m : ℤ) : Prop

$m$ is \emph{an $\mathrm{lcm}$} of $a, b$: $m \geq 0$ and $m\mathbb{Z} = a\mathbb{Z} \cap b\mathbb{Z}$.

Equations

• MyAlgebra.IsLcm a b m = (0 ≤ m ∧ ∀ (n : ℤ), MyAlgebra.aZ m n ↔ MyAlgebra.aZ a n ∧ MyAlgebra.aZ b n)

theorem MyAlgebra.bezout {a b d : ℤ} (h : IsGcd a b d) : ∃ (r : ℤ) (s : ℤ), r * a + s * b = d

B'ezout: $d = \gcd(a, b) \;\Longrightarrow\; \exists r, s : ra + sb = d$.

theorem MyAlgebra.gcd_dvd {a b d : ℤ} (h : IsGcd a b d) : d ∣ a ∧ d ∣ b

$d = \gcd(a, b) \;\Longrightarrow\; d \mid a \;\wedge\; d \mid b$.

theorem MyAlgebra.dvd_gcd {a b d e : ℤ} (h : IsGcd a b d) (ha : e ∣ a) (hb : e ∣ b) : e ∣ d

Universality of $\gcd$: any common divisor of $a, b$ divides $\gcd(a, b)$.

def MyAlgebra.IsCoprime (a b : ℤ) : Prop

$a, b$ are \emph{coprime} if $\gcd(a, b) = 1$.

Equations

• MyAlgebra.IsCoprime a b = MyAlgebra.IsGcd a b 1

theorem MyAlgebra.isCoprime_iff_bezout (a b : ℤ) : IsCoprime a b ↔ ∃ (r : ℤ) (s : ℤ), r * a + s * b = 1

$a, b$ coprime $\;\Longleftrightarrow\; \exists r, s : ra + sb = 1$.

theorem MyAlgebra.euclid_lemma {p a b : ℤ} (hp : Prime p) (hpab : p ∣ a * b) : p ∣ a ∨ p ∣ b

Euclid's lemma: $p$ prime, $p \mid ab \;\Longrightarrow\; p \mid a \;\vee\; p \mid b$.

theorem MyAlgebra.dvd_lcm {a b m : ℤ} (h : IsLcm a b m) : a ∣ m ∧ b ∣ m

If $m = \mathrm{lcm}(a, b)$, then both $a$ and $b$ divide $m$ (Proposition 1.2.7(a)).

theorem MyAlgebra.lcm_dvd {a b m n : ℤ} (h : IsLcm a b m) (ha : a ∣ n) (hb : b ∣ n) : m ∣ n

Universality of $\mathrm{lcm}$: if $a \mid n$ and $b \mid n$, then $\mathrm{lcm}(a, b) \mid n$ (Proposition 1.2.7(b)).

theorem MyAlgebra.gcd_mul_lcm {a b d m : ℤ} (ha : a ≠ 0) (hb : b ≠ 0) (hd : IsGcd a b d) (hm : IsLcm a b m) : d * m = |a * b|

$\gcd(a, b) \cdot \mathrm{lcm}(a, b) = |a \cdot b|$ for $a, b$ both nonzero (Corollary 1.2.8).

Group homomorphisms

structure MyAlgebra.MyHom (G : Type u_1) (G' : Type u_2) [MyGroup G] [MyGroup G'] : Type (max u_1 u_2)

A group homomorphism $\varphi : G \to G'$.

• toFun : G → G'

  Underlying function $G \to G'$.

• mul_map (a b : G) : self.toFun (a * b) = self.toFun a * self.toFun b

  Multiplicativity: $\forall a, b,\; \varphi(a \cdot b) = \varphi(a) \cdot \varphi(b)$.

theorem MyAlgebra.MyHom.one_map {G : Type u_1} {G' : Type u_2} [MyGroup G] [MyGroup G'] (ϕ : MyHom G G') : ϕ.toFun 1 = 1

$\varphi(1) = 1$: homomorphisms preserve the identity.

theorem MyAlgebra.MyHom.inv_map {G : Type u_1} {G' : Type u_2} [MyGroup G] [MyGroup G'] (ϕ : MyHom G G') (a : G) : ϕ.toFun a⁻¹ = (ϕ.toFun a)⁻¹

$\varphi(a^{-1}) = \varphi(a)^{-1}$: homomorphisms preserve inverses.

theorem MyAlgebra.MyHom.pow_map {G : Type u_1} {G' : Type u_2} [MyGroup G] [MyGroup G'] (ϕ : MyHom G G') (a : G) (n : ℕ) : ϕ.toFun (a ^ n) = ϕ.toFun a ^ n

$\varphi(a^n) = \varphi(a)^n$ for $n : \mathbb{N}$: homomorphisms preserve natural-number powers.

def MyAlgebra.MyHom.trivial (G : Type u_3) (G' : Type u_4) [MyGroup G] [MyGroup G'] : MyHom G G'

The trivial homomorphism $\tau : G \to G',\; x \mapsto 1$.

Equations

• MyAlgebra.MyHom.trivial G G' = { toFun := fun (x : G) => 1, mul_map := ⋯ }

def MyAlgebra.MyHom.identity (G : Type u_3) [MyGroup G] : MyHom G G

The identity homomorphism $\mathrm{id}_G : G \to G$.

Equations

• MyAlgebra.MyHom.identity G = { toFun := fun (x : G) => x, mul_map := ⋯ }

Image, kernel, and the kernel test

def MyAlgebra.MyHom.image {G : Type u_1} {G' : Type u_2} [MyGroup G] [MyGroup G'] (ϕ : MyHom G G') : MySubgroup G'

$\mathrm{im}\,\varphi$ as a subgroup of $G'$.

Equations

• ϕ.image = { carrier := fun (y : G') => ∃ (x : G), ϕ.toFun x = y, one_mem := ⋯, mul_mem := ⋯, inv_mem := ⋯ }

def MyAlgebra.MyHom.kernel {G : Type u_1} {G' : Type u_2} [MyGroup G] [MyGroup G'] (ϕ : MyHom G G') : MySubgroup G

$\ker \varphi$ as a subgroup of $G$.

Equations

• ϕ.kernel = { carrier := fun (x : G) => ϕ.toFun x = 1, one_mem := ⋯, mul_mem := ⋯, inv_mem := ⋯ }

theorem MyAlgebra.MyHom.kernel_test {G : Type u_1} {G' : Type u_2} [MyGroup G] [MyGroup G'] (ϕ : MyHom G G') (a b : G) : ϕ.toFun a = ϕ.toFun b ↔ ϕ.kernel.carrier (a⁻¹ * b)

Kernel test: $\varphi(a) = \varphi(b) \;\Longleftrightarrow\; a^{-1} \cdot b \in \ker \varphi$.

theorem MyAlgebra.MyHom.injective_iff_kernel_trivial {G : Type u_1} {G' : Type u_2} [MyGroup G] [MyGroup G'] (ϕ : MyHom G G') : (∀ (a b : G), ϕ.toFun a = ϕ.toFun b → a = b) ↔ ∀ (a : G), ϕ.kernel.carrier a → a = 1

$\varphi$ injective $\;\Longleftrightarrow\; \ker \varphi = \{1\}$.

def MyAlgebra.MyHom.comp {G : Type u_3} {G' : Type u_4} {G'' : Type u_5} [MyGroup G] [MyGroup G'] [MyGroup G''] (ψ : MyHom G' G'') (ϕ : MyHom G G') : MyHom G G''

Composition of homomorphisms is a homomorphism: $(\psi \circ \varphi)(a) := \psi(\varphi(a))$.

Equations

• ψ.comp ϕ = { toFun := fun (x : G) => ψ.toFun (ϕ.toFun x), mul_map := ⋯ }

def MyAlgebra.MyHom.imageOf {G : Type u_1} {G' : Type u_2} [MyGroup G] [MyGroup G'] (ϕ : MyHom G G') (H : MySubgroup G) : MySubgroup G'

Image of a subgroup $H \leq G$ under $\varphi$: $\varphi(H) := \{\, \varphi(h) : h \in H \,\} \leq G'$. Specializes to \cref{MyAlgebra.MyHom.image} at $H = \top$.

Equations

• ϕ.imageOf H = { carrier := fun (y : G') => ∃ (x : G), H.carrier x ∧ ϕ.toFun x = y, one_mem := ⋯, mul_mem := ⋯, inv_mem := ⋯ }

def MyAlgebra.MyHom.preimage {G : Type u_1} {G' : Type u_2} [MyGroup G] [MyGroup G'] (ϕ : MyHom G G') (K : MySubgroup G') : MySubgroup G

Preimage of a subgroup $K \leq G'$ under $\varphi$: $\varphi^{-1}(K) := \{\, x \in G : \varphi(x) \in K \,\} \leq G$. Specializes to \cref{MyAlgebra.MyHom.kernel} at $K = \bot$.

Equations

• ϕ.preimage K = { carrier := fun (x : G) => K.carrier (ϕ.toFun x), one_mem := ⋯, mul_mem := ⋯, inv_mem := ⋯ }

Isomorphisms

structure MyAlgebra.MyIso (G : Type u_1) (G' : Type u_2) [MyGroup G] [MyGroup G'] extends MyAlgebra.MyHom G G' : Type (max u_1 u_2)

A group isomorphism: a homomorphism bundled with a two-sided inverse function.

• toFun : G → G'
• mul_map (a b : G) : self.toFun (a * b) = self.toFun a * self.toFun b
• invFun : G' → G

  Two-sided inverse function $G' \to G$.

• left_inv (x : G) : self.invFun (self.toFun x) = x

  Left inverse: $\forall x,\; \mathrm{invFun}(\mathrm{toFun}\, x) = x$.

• right_inv (y : G') : self.toFun (self.invFun y) = y

  Right inverse: $\forall y,\; \mathrm{toFun}(\mathrm{invFun}\, y) = y$.

def MyAlgebra.MyIso.identity (G : Type u_1) [MyGroup G] : MyIso G G

The identity isomorphism $\mathrm{id}_G : G \xrightarrow{\sim} G$.

Equations

• MyAlgebra.MyIso.identity G = { toFun := fun (x : G) => x, mul_map := ⋯, invFun := fun (x : G) => x, left_inv := ⋯, right_inv := ⋯ }

def MyAlgebra.MyIso.symm {G : Type u_1} {G' : Type u_2} [MyGroup G] [MyGroup G'] (e : MyIso G G') : MyIso G' G

The inverse isomorphism $e^{-1} : G' \xrightarrow{\sim} G$.

Equations

• e.symm = { toFun := e.invFun, mul_map := ⋯, invFun := e.toFun, left_inv := ⋯, right_inv := ⋯ }

def MyAlgebra.MyIso.comp {G : Type u_1} {G' : Type u_2} {G'' : Type u_3} [MyGroup G] [MyGroup G'] [MyGroup G''] (f : MyIso G' G'') (e : MyIso G G') : MyIso G G''

Composition of isomorphisms is an isomorphism.

Equations

• f.comp e = { toFun := fun (x : G) => f.toFun (e.toFun x), mul_map := ⋯, invFun := fun (z : G'') => e.invFun (f.invFun z), left_inv := ⋯, right_inv := ⋯ }

Normal subgroups

def MyAlgebra.IsNormal {G : Type u_1} [MyGroup G] (H : MySubgroup G) : Prop

$H \triangleleft G$: $\forall g \in G,\, h \in H,\; g \cdot h \cdot g^{-1} \in H$.

Equations

• MyAlgebra.IsNormal H = ∀ (g h : G), H.carrier h → H.carrier (g * h * g⁻¹)

theorem MyAlgebra.normal_of_comm {G : Type u_1} [MyCommGroup G] (H : MySubgroup G) : IsNormal H

In an abelian group, every subgroup is normal.

theorem MyAlgebra.MyHom.kernel_normal {G : Type u_1} {G' : Type u_2} [MyGroup G] [MyGroup G'] (ϕ : MyHom G G') : IsNormal ϕ.kernel

Kernels are normal: $\ker \varphi \triangleleft G$.

theorem MyAlgebra.MyHom.preimage_normal {G : Type u_1} {G' : Type u_2} [MyGroup G] [MyGroup G'] (ϕ : MyHom G G') {K : MySubgroup G'} (hK : IsNormal K) : IsNormal (ϕ.preimage K)

Preimage of a normal subgroup under a homomorphism is normal: $K \triangleleft G' \;\Longrightarrow\; \varphi^{-1}(K) \triangleleft G$.

theorem MyAlgebra.bot_isNormal {G : Type u_1} [MyGroup G] : IsNormal MySubgroup.bot

The trivial subgroup is normal.

theorem MyAlgebra.top_isNormal {G : Type u_1} [MyGroup G] : IsNormal MySubgroup.top

The whole group is normal in itself.

theorem MyAlgebra.IsNormal.inter {G : Type u_1} [MyGroup G] {H K : MySubgroup G} (hH : IsNormal H) (hK : IsNormal K) : IsNormal (H.inter K)

Intersection of two normal subgroups is normal.

The center

def MyAlgebra.center (G : Type u_1) [MyGroup G] : MySubgroup G

$Z(G) := \{\, z : \forall x,\; z \cdot x = x \cdot z \,\}$, the center of $G$, as a subgroup.

Equations

• MyAlgebra.center G = { carrier := fun (z : G) => ∀ (x : G), z * x = x * z, one_mem := ⋯, mul_mem := ⋯, inv_mem := ⋯ }

theorem MyAlgebra.center_eq_top_iff_commutes (G : Type u_1) [MyGroup G] : (∀ (z : G), (center G).carrier z) ↔ ∀ (a b : G), a * b = b * a

$G$ is abelian $\;\Longleftrightarrow\; Z(G) = G$.

theorem MyAlgebra.center_normal (G : Type u_1) [MyGroup G] : IsNormal (center G)

The center is a normal subgroup: $Z(G) \triangleleft G$.

Centralizer, normalizer, and inner automorphisms

def MyAlgebra.centralizer {G : Type u_1} [MyGroup G] (a : G) : MySubgroup G

$C_G(a) := \{\, g \in G : g \cdot a = a \cdot g \,\}$, the centralizer of $a$, as a subgroup of $G$.

Equations

• MyAlgebra.centralizer a = { carrier := fun (g : G) => g * a = a * g, one_mem := ⋯, mul_mem := ⋯, inv_mem := ⋯ }

def MyAlgebra.conjugationHom {G : Type u_1} [MyGroup G] (g : G) : MyHom G G

For each $g \in G$, conjugation by $g$, $\mathrm{conj}_g : G \to G,\; x \mapsto g \cdot x \cdot g^{-1}$, is a group homomorphism (an \emph{inner automorphism} of $G$).

Equations

• MyAlgebra.conjugationHom g = { toFun := fun (x : G) => g * x * g⁻¹, mul_map := ⋯ }

def MyAlgebra.normalizer {G : Type u_1} [MyGroup G] (H : MySubgroup G) : MySubgroup G

$N_G(H) := \{\, g : \forall h,\; h \in H \iff g h g^{-1} \in H \,\}$, the normalizer of $H$ in $G$, as a subgroup.

Equations

• MyAlgebra.normalizer H = { carrier := fun (g : G) => ∀ (h : G), H.carrier h ↔ H.carrier (g * h * g⁻¹), one_mem := ⋯, mul_mem := ⋯, inv_mem := ⋯ }

theorem MyAlgebra.subset_normalizer {G : Type u_1} [MyGroup G] (H : MySubgroup G) (h : G) (hh : H.carrier h) : (normalizer H).carrier h

Every subgroup is contained in its own normalizer: $H \subseteq N_G(H)$.

theorem MyAlgebra.normal_iff_normalizer_eq_top {G : Type u_1} [MyGroup G] (H : MySubgroup G) : IsNormal H ↔ ∀ (g : G), (normalizer H).carrier g

$H$ is normal in $G$ iff its normalizer is all of $G$: $H \triangleleft G \;\Longleftrightarrow\; \forall g \in G,\; g \in N_G(H)$.

A note on finite groups

In a finite group every element has finite order: the powers $g^0, g^1, g^2, \ldots$ cannot all be distinct, so $g^i = g^j$ for some $i < j$, giving $g^{j-i} = 1$. Formalizing "finite" needs Fintype, which lives in mathlib — the next chapter imports it and proves Lagrange's theorem: the order of every element of a finite group divides the order of the group.