Table of Contents

• C09 S01 — Groups: Summary Notes
  • Monoids
  • Homomorphisms of Monoids and Groups
    • Monoid homomorphisms
    • Groups and the group/abel tactics
    • Group homomorphisms
  • Group Isomorphisms
  • Subgroups
    • Closure properties
    • Example: ℤ as an additive subgroup of ℚ
    • A subgroup is itself a group
    • Lattice operations on subgroups
    • Conjugate subgroups
  • Homomorphisms Acting on Subgroups
    • Image (map) and preimage (comap)
    • Kernel and range membership
    • Monotonicity of map and comap
    • map/comap along a composition
  • Counting: Lagrange and Sylow
    • Lagrange's theorem
    • Sylow's theorem
    • Triviality via cardinality
  • Quotient Groups
    • Normal subgroups and the quotient group
    • Universal properties: lift, map, and friends
  • A Chinese-Remainder-Style Finale
    • Auxiliary cardinality lemma
    • First isomorphism: K ≃* G ⧸ H
    • Second isomorphism: G ≃* (G ⧸ K) × (G ⧸ H)
    • Final isomorphism: G ≃* H × K

C09 S01 — Groups: Summary Notes

Summary generated from the comments in C09-S01.lean.

Monoids

Class	Definition	Key lemma
Monoid	a Semigroup with identity 1 such that x * 1 = x and 1 * x = x	mul_one, one_mul
AddCommMonoid	an AddMonoid with commutative addition	add_comm

example {M : Type*} [Monoid M] (x : M) : x * 1 = x := mul_one x
example {M : Type*} [AddCommMonoid M] (x y : M) : x + y = y + x := add_comm x y

Homomorphisms of Monoids and Groups

Monoid homomorphisms

A homomorphism of (multiplicative) monoids, written f : M →* N, preserves multiplication and the identity; additive monoid homomorphisms are written f : M →+ N:

example {M N : Type*} [Monoid M] [Monoid N] (x y : M) (f : M →* N) : f (x * y) = f x * f y :=
  f.map_mul x y
example {M N : Type*} [AddMonoid M] [AddMonoid N] (f : M →+ N) : f 0 = 0 :=
  f.map_zero

Composition of (additive) monoid homomorphisms is given by g.comp f:

example {M N P : Type*} [AddMonoid M] [AddMonoid N] [AddMonoid P]
    (f : M →+ N) (g : N →+ P) : M →+ P := g.comp f

Groups and the group/abel tactics

A Group is a monoid with inverses; an AddCommGroup is the additive, commutative counterpart.

Tactic	Scope
group	proves identities true in any group (free-group normalization)
abel	proves identities true in any abelian (additive commutative) group

example {G : Type*} [Group G] (x : G) : x * x⁻¹ = 1 := mul_inv_cancel x
example {G : Type*} [Group G] (x y z : G) : x * (y * z) * (x * z)⁻¹ * (x * y * x⁻¹)⁻¹ = 1 := by
  group
example {G : Type*} [AddCommGroup G] (x y z : G) : z + x + (y - z - x) = y := by
  abel

TIP

group and abel are huge time-savers for "obvious" rearrangements — use them instead of hand-chaining associativity/inverse lemmas.

Group homomorphisms

Homomorphisms of (multiplicative) groups are monoid homomorphisms; they automatically preserve inverses:

Lemma	Statement
f.map_mul	f (x * y) = f x * f y
f.map_inv	f (x⁻¹) = (f x)⁻¹

Conversely, a bare function that preserves multiplication between groups is enough to build a homomorphism — preservation of 1 and ⁻¹ comes for free:

example {G H : Type*} [Group G] [Group H] (f : G → H) (h : ∀ x y, f (x * y) = f x * f y) :
    G →* H :=
  MonoidHom.mk' f h

Group Isomorphisms

A group isomorphism f : G ≃* H is a bijective homomorphism bundled with its inverse (MulEquiv).

• Composing with the symmetric gives the identity isomorphism:

  example {G H : Type*} [Group G] [Group H] (f : G ≃* H) :
      f.trans f.symm = MulEquiv.refl G :=
    f.self_trans_symm

• A bijective homomorphism upgrades to an isomorphism:

  noncomputable example {G H : Type*} [Group G] [Group H]
      (f : G →* H) (h : Function.Bijective f) : G ≃* H :=
    MulEquiv.ofBijective f h

Subgroups

Closure properties

A subgroup H : Subgroup G is closed under the group operations:

Closure	Lemma	Statement
multiplication	H.mul_mem	x ∈ H → y ∈ H → x * y ∈ H
inverses	H.inv_mem	x ∈ H → x⁻¹ ∈ H

Example: ℤ as an additive subgroup of ℚ

example : AddSubgroup ℚ where
  carrier := Set.range ((↑) : ℤ → ℚ)
  add_mem' := by
    rintro _ _ ⟨n, rfl⟩ ⟨m, rfl⟩
    use n + m
    simp
  zero_mem' := by
    use 0
    simp
  neg_mem' := by
    rintro _ ⟨n, rfl⟩
    use -n
    simp

Field	Role	Proof idea
carrier	the underlying set: Set.range ((↑) : ℤ → ℚ), the image of the coercion ℤ → ℚ	the coercion is an enforced conversion — since the ambient group is ℚ, the carrier must be a subset of ℚ
add_mem'	closure under +	destruct as ↑n, ↑m; witness ↑(n + m); simp since (↑) preserves addition
zero_mem'	0 ∈ carrier	witness 0 = ↑0
neg_mem'	closure under negation	witness -(↑n) = ↑(-n)

A subgroup is itself a group

example {G : Type*} [Group G] (H : Subgroup G) : Group H := inferInstance
example {G : Type*} [Group G] (H : Subgroup G) : Group {x : G // x ∈ H} := inferInstance

H (as a Subgroup G) and the subtype {x : G // x ∈ H} carry the same Group instance.

Lattice operations on subgroups

• Infimum is literal intersection of the underlying sets:

  example {G : Type*} [Group G] (H H' : Subgroup G) :
      ((H ⊓ H' : Subgroup G) : Set G) = (H : Set G) ∩ (H' : Set G) := rfl

• Supremum is the subgroup generated by the union of the underlying sets:

  example {G : Type*} [Group G] (H H' : Subgroup G) :
      ((H ⊔ H' : Subgroup G) : Set G) = Subgroup.closure ((H : Set G) ∪ (H' : Set G)) := by
    rw [Subgroup.sup_eq_closure]

• Top and bottom: x ∈ (⊤ : Subgroup G) holds trivially for every x; x ∈ (⊥ : Subgroup G) ↔ x = 1 (Subgroup.mem_bot).

WARNING

Just as for submodules, the set-theoretic union of two subgroups is generally not a subgroup — ⊔ closes it up via Subgroup.closure.

Conjugate subgroups

The conjugate of a subgroup H by an element x is the subgroup x H x⁻¹:

Full definition and proof walkthrough (click to expand)

def conjugate {G : Type*} [Group G] (x : G) (H : Subgroup G) : Subgroup G where
  carrier := {a : G | ∃ h, h ∈ H ∧ a = x * h * x⁻¹}
  one_mem' := by
    dsimp
    use 1
    constructor
    exact H.one_mem
    group
  inv_mem' := by
    dsimp
    rintro - ⟨h, h_in, rfl⟩
    use h⁻¹, H.inv_mem h_in
    group
  mul_mem' := by
    dsimp
    rintro - - ⟨h, h_in, rfl⟩ ⟨k, k_in, rfl⟩
    use h*k, H.mul_mem h_in k_in
    group

Each obligation follows the same pattern: unfold the carrier with dsimp, destruct the existential to expose an element of H, supply the corresponding element of H as witness (1, h⁻¹, h * k), and let the group tactic discharge the pure group identity — e.g. x * 1 * x⁻¹ = 1, (x * h * x⁻¹)⁻¹ = x * h⁻¹ * x⁻¹, and (x * h * x⁻¹) * (x * k * x⁻¹) = x * (h * k) * x⁻¹.

Homomorphisms Acting on Subgroups

Let f : G →* H be a group homomorphism.

Image (map) and preimage (comap)

example {G H : Type*} [Group G] [Group H] (G' : Subgroup G) (f : G →* H) : Subgroup H :=
  Subgroup.map f G'
example {G H : Type*} [Group G] [Group H] (H' : Subgroup H) (f : G →* H) : Subgroup G :=
  Subgroup.comap f H'

• Subgroup.map f G' — the image of a subgroup of the source, a subgroup of the target.
• Subgroup.comap f H' — the preimage of a subgroup of the target, a subgroup of the source.

Kernel and range membership

Lemma	Statement
f.mem_ker	g ∈ MonoidHom.ker f ↔ f g = 1
f.mem_range	h ∈ MonoidHom.range f ↔ ∃ g : G, f g = h

Monotonicity of map and comap

Both operations are monotone:

example (φ : G →* H) (S T : Subgroup H) (hST : S ≤ T) : comap φ S ≤ comap φ T := by
  intro x hx
  rw [mem_comap] at * -- Lean does not need this line
  exact hST hx

example (φ : G →* H) (S T : Subgroup G) (hST : S ≤ T) : map φ S ≤ map φ T := by
  intro x hx
  rw [mem_map] at * -- Lean does not need this line
  rcases hx with ⟨y, hy, rfl⟩
  use y, hST hy

The rw [mem_comap]/rw [mem_map] lines are only for readability — membership in comap/map is already definitional, so Lean does not need them.

map/comap along a composition

Pullback is contravariant, pushforward is covariant:

$$\mathrm{comap}(\psi \circ \phi )=\mathrm{comap}\phi \circ \mathrm{comap}\psi ,\mathrm{map}(\psi \circ \phi )=\mathrm{map}\psi \circ \mathrm{map}\phi$$

Proofs (click to expand)

example (φ : G →* H) (ψ : H →* K) (U : Subgroup K) :
    comap (ψ.comp φ) U = comap φ (comap ψ U) := by
  ext x
  simp only [mem_comap]
  rfl

example (φ : G →* H) (ψ : H →* K) (S : Subgroup G) :
    map (ψ.comp φ) S = map ψ (S.map φ) := by
  ext x
  simp only [mem_map]
  constructor
  · rintro ⟨y, y_in, hy⟩
    exact ⟨φ y, ⟨y, y_in, rfl⟩, hy⟩
  · rintro ⟨y, ⟨z, z_in, hz⟩, hy⟩
    use z, z_in
    calc ψ.comp φ z = ψ (φ z) := rfl
    _               = ψ y := by congr
    _               = x := hy

• The comap identity is true by definition — ext + simp only [mem_comap] + rfl (the whole proof could be a single rfl).
• For map, both directions chase the existentials: the forward direction maps the witness through φ; the backward direction unpacks the nested witness and finishes with a calc chain, using congr to rewrite with hz : φ z = y inside ψ.

Counting: Lagrange and Sylow

Lagrange's theorem

The cardinality of a subgroup divides the cardinality of the whole group:

$$|G^{\prime }|||G|,\text{i.e. }\mathrm{\exists }k,|G|=|G^{\prime }|\cdot k$$

where the witness k is the index G'.index of the subgroup:

example {G : Type*} [Group G] (G' : Subgroup G) : Nat.card G' ∣ Nat.card G :=
  ⟨G'.index, mul_comm G'.index _ ▸ G'.index_mul_card.symm⟩

The anonymous constructor provides the existential witness G'.index; h ▸ e rewrites e using the equality h, here commuting the product in G'.index_mul_card : G'.index * Nat.card G' = Nat.card G.

Sylow's theorem

For a finite group G and a prime p, if p ^ n ∣ Nat.card G then there is a subgroup of order p ^ n:

example {G : Type*} [Group G] [Finite G] (p : ℕ) {n : ℕ} [Fact p.Prime]
    (hdvd : p ^ n ∣ Nat.card G) : ∃ K : Subgroup G, Nat.card K = p ^ n :=
  Sylow.exists_subgroup_card_pow_prime p hdvd

Triviality via cardinality

A subgroup is trivial iff its cardinality is 1:

$$H=\mathrm{\perp }⟺|H|=1$$

Proof of `eq_bot_iff_card` (click to expand)

lemma eq_bot_iff_card {G : Type*} [Group G] {H : Subgroup G} :
    H = ⊥ ↔ Nat.card H = 1 := by
  suffices (∀ x ∈ H, x = 1) ↔ ∃ x ∈ H, ∀ a ∈ H, a = x by
    simpa [eq_bot_iff_forall, Nat.card_eq_one_iff_exists]
  constructor
  · intro h
    use 1, H.one_mem
  · rintro ⟨y, -, hy'⟩ x hx
    calc x = y := hy' x hx
    _      = 1 := (hy' 1 H.one_mem).symm

The suffices rephrases both sides as "all elements equal 1" ↔ "all elements equal some common element"; simpa bridges with eq_bot_iff_forall and Nat.card_eq_one_iff_exists. The forward direction uses 1 as the common element; the backward direction shows every x equals the common y, which itself equals 1 (since 1 ∈ H).

Two corollaries of Lagrange-style reasoning:

Lemma	Statement
card_dvd_of_le	if H ≤ K then Nat.card H ∣ Nat.card K
inf_bot_of_coprime (below)	coprime cardinalities force trivial intersection

lemma inf_bot_of_coprime {G : Type*} [Group G] (H K : Subgroup G)
    (h : (Nat.card H).Coprime (Nat.card K)) : H ⊓ K = ⊥ := by
  have D₁ : Nat.card (H ⊓ K : Subgroup G) ∣ Nat.card H := card_dvd_of_le inf_le_left
  have D₂ : Nat.card (H ⊓ K : Subgroup G) ∣ Nat.card K := card_dvd_of_le inf_le_right
  exact eq_bot_iff_card.2 (Nat.eq_one_of_dvd_coprimes h D₁ D₂)

Since H ⊓ K ≤ H and H ⊓ K ≤ K, its cardinality divides both |H| and |K|; coprimality forces that divisor to be 1, and eq_bot_iff_card finishes.

Quotient Groups

Normal subgroups and the quotient group

H.Normal marks a subgroup that is invariant under conjugation by all group elements — exactly the condition for the quotient to carry a group structure:

example {G : Type*} [Group G] (H : Subgroup G) [H.Normal] : Group (G ⧸ H) := inferInstance

QuotientGroup.mk' is the canonical projection G →* G ⧸ H:

example {G : Type*} [Group G] (H : Subgroup G) [H.Normal] : G →* G ⧸ H :=
  QuotientGroup.mk' H

Universal properties: lift, map, and friends

Construction	Type	Requirement
QuotientGroup.lift N φ h	G ⧸ N →* M	h : N ≤ MonoidHom.ker φ — φ kills N
QuotientGroup.quotientKerEquivRange φ	G ⧸ ker φ →* MonoidHom.range φ	— (first isomorphism theorem)
QuotientGroup.map N N' φ h	G ⧸ N →* G' ⧸ N'	h : N ≤ Subgroup.comap φ N' — φ maps N into N'
QuotientGroup.quotientMulEquivOfEq h	G ⧸ M ≃* G ⧸ N	h : M = N

The first isomorphism theorem for groups:

$$G/\ker \phi \cong \mathrm{range}\phi$$

A Chinese-Remainder-Style Finale

Setup. H K : Subgroup G are both normal, G is a Fintype, and:

variable [H.Normal] [K.Normal] [Fintype G] (h : Disjoint H K)
  (h' : Nat.card G = Nat.card H * Nat.card K)

That is, H and K are disjoint and their orders multiply to the order of G. The goal: decompose G as the product H × K.

Auxiliary cardinality lemma

Under Nat.card G = Nat.card H * Nat.card K, the quotient has the complementary cardinality:

lemma aux_card_eq [Finite G] (h' : Nat.card G = Nat.card H * Nat.card K) :
    Nat.card (G ⧸ H) = Nat.card K := by
  have := calc
    Nat.card (G ⧸ H) * Nat.card H = Nat.card G := by rw [← H.index_eq_card, H.index_mul_card]
    _                             = Nat.card K * Nat.card H := by rw [h', mul_comm]
  exact Nat.eq_of_mul_eq_mul_right Nat.card_pos this

Key facts used:

Lemma	Statement
Subgroup.index_eq_card	the index of H equals the cardinality of G ⧸ H
Subgroup.index_mul_card	index H * Nat.card H = Nat.card G
Nat.eq_of_mul_eq_mul_right	cancel a positive right factor (Nat.card_pos supplies positivity)

First isomorphism: K ≃* G ⧸ H

Proof walkthrough (click to expand)

def iso₁ : K ≃* G ⧸ H := by
  apply MulEquiv.ofBijective ((QuotientGroup.mk' H).restrict K)
  rw [Nat.bijective_iff_injective_and_card]
  constructor
  · rw [← ker_eq_bot_iff, (QuotientGroup.mk' H).ker_restrict K]
    simp [h]
  · symm
    exact aux_card_eq h'

1. Candidate map. Restrict the canonical projection QuotientGroup.mk' H : G →* G ⧸ H to the subgroup K (restrict K).
2. Bijectivity by injectivity + cardinality (Nat.bijective_iff_injective_and_card): a map between finite types of equal cardinality is bijective iff injective.
3. Injectivity. ← ker_eq_bot_iff turns it into triviality of the kernel; ker_restrict rewrites the kernel of the restriction as ker (mk' H) viewed as a subgroup of K (subgroupOf), and simp [h] collapses it to ⊥ using disjointness of H and K.
4. Cardinality. aux_card_eq h' gives Nat.card (G ⧸ H) = Nat.card K, symmetrized to match the goal.

Second isomorphism: G ≃* (G ⧸ K) × (G ⧸ H)

Proof walkthrough (click to expand)

def iso₂ : G ≃* (G ⧸ K) × (G ⧸ H) := by
  apply MulEquiv.ofBijective <| (QuotientGroup.mk' K).prod (QuotientGroup.mk' H)
  rw [Nat.bijective_iff_injective_and_card]
  constructor
  · rw [← ker_eq_bot_iff, ker_prod]
    simp [h.symm.eq_bot]
  · rw [Nat.card_prod]
    rw [aux_card_eq h', aux_card_eq (mul_comm (Nat.card H) _▸ h'), h']

1. Candidate map. The product of the two projections, g ↦ (gK, gH), via MonoidHom.prod.
2. Injectivity. The kernel of a product map is the intersection of the kernels (ker_prod): ker (mk' K) ⊓ ker (mk' H) = K ⊓ H = ⊥ by disjointness (h.symm.eq_bot).
3. Cardinality. Nat.card_prod splits the product cardinality; both quotient cardinalities evaluate via aux_card_eq — the second applied to h' with the factors commuted — and h' itself closes the equation.

Final isomorphism: G ≃* H × K

Compose iso₂ with the (symmetric of the) product of the two iso₁ isomorphisms — one per factor — using MulEquiv.prodCongr to work componentwise:

def finalIso : G ≃* H × K :=
  (iso₂ h h').trans ((iso₁ h.symm (mul_comm (Nat.card H) _ ▸ h')).prodCongr (iso₁ h h')).symm

$$G\stackrel{\sim }{\to }(G/K)\times (G/H)\stackrel{\sim }{\to }H\times K$$

NOTE

The symmetry bookkeeping: iso₁ h h' : K ≃* G ⧸ H, while iso₁ h.symm (mul_comm .. ▸ h') : H ≃* G ⧸ K. Their prodCongr gives H × K ≃* (G ⧸ K) × (G ⧸ H), and .symm orients it correctly for trans after iso₂.