9. Grup dan Gelanggang

Dalam Bab 2.2, kita telah melihat cara menalar tentang operasi pada grup dan gelanggang. Kemudian, dalam Bab 7.2, kita melihat cara mendefinisikan struktur aljabar abstrak, seperti struktur grup, beserta instans konkret seperti struktur gelanggang pada bilangan bulat Gauss. Bab 8 menjelaskan cara hierarki struktur abstrak ditangani dalam Mathlib.

Dalam bab ini, kita akan mempelajari grup dan gelanggang secara lebih terperinci. Kita tidak akan dapat membahas setiap aspek penanganan topik-topik tersebut dalam Mathlib, terlebih karena Mathlib terus berkembang. Namun, kita akan menyediakan titik masuk ke pustaka dan menunjukkan cara menggunakan konsep-konsep esensial. Ada sedikit tumpang tindih dengan pembahasan dalam Bab 8, tetapi di sini kita akan berfokus pada cara menggunakan Mathlib, bukan pada keputusan desain yang mendasari penanganan topik-topik tersebut. Karena itu, memahami sebagian contoh mungkin memerlukan peninjauan kembali latar belakang dari Bab 8.

9.1. Monoid dan Grup

9.1.1. Monoid dan morfismenya

Kuliah aljabar abstrak sering dimulai dengan grup, lalu berlanjut ke gelanggang, medan, dan ruang vektor. Hal ini menuntut beberapa penyesuaian ketika membahas perkalian pada gelanggang, sebab operasi perkalian tersebut tidak berasal dari struktur grup, tetapi banyak buktinya dapat dipindahkan kata demi kata dari teori grup ke konteks baru ini. Solusi yang paling lazim ketika mengerjakan matematika dengan pena dan kertas adalah menyerahkan bukti tersebut sebagai latihan. Cara yang kurang efisien, tetapi lebih aman dan lebih ramah formalisasi, adalah menggunakan monoid. Struktur monoid pada tipe M merupakan hukum komposisi internal yang asosiatif dan memiliki elemen netral.

Monoid terutama digunakan untuk mencakup grup sekaligus struktur multiplikatif gelanggang. Namun, ada pula sejumlah contoh alami; misalnya, himpunan bilangan asli yang dilengkapi penjumlahan membentuk monoid.

Dari sudut pandang praktis, Anda dapat mengabaikan monoid hampir sepenuhnya ketika menggunakan Mathlib. Namun, Anda perlu mengetahui keberadaannya ketika mencari lemma dengan menelusuri berkas Mathlib. Jika tidak, Anda mungkin mencari suatu pernyataan dalam berkas teori grup, padahal pernyataan tersebut terdapat pada bagian monoid karena tidak memerlukan elemen yang dapat dibalik.

Tipe struktur monoid pada tipe M ditulis Monoid M. Monoid merupakan kelas tipe, sehingga hampir selalu muncul sebagai argumen instans implisit (dengan kata lain, di dalam tanda kurung siku). Secara baku, Monoid menggunakan notasi multiplikatif bagi operasinya; untuk notasi aditif, gunakan AddMonoid. Versi komutatif struktur tersebut menambahkan prefiks Comm sebelum Monoid.

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

Perhatikan bahwa meskipun AddMonoid tersedia di pustaka, penggunaan notasi aditif untuk operasi nonkomutatif umumnya membingungkan.

Tipe morfisme di antara monoid M dan N disebut MonoidHom M N dan ditulis M →* N. Lean secara otomatis memandang morfisme semacam itu sebagai fungsi dari M ke N ketika kita menerapkannya pada elemen M. Versi aditifnya disebut AddMonoidHom dan ditulis 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

Morfisme tersebut merupakan pemetaan terbundel, yakni mengemas sebuah pemetaan beserta beberapa sifatnya. Ingat bahwa Bab 8.2 menjelaskan pemetaan terbundel. Di sini, kita hanya mencatat konsekuensi yang sedikit disayangkan: komposisi fungsi biasa tidak dapat digunakan untuk mengomposisikan pemetaan ini. Sebagai gantinya, kita perlu menggunakan MonoidHom.comp dan AddMonoidHom.comp.

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

9.1.2. Grup dan morfismenya

Kita akan membahas grup jauh lebih banyak. Grup merupakan monoid dengan sifat tambahan bahwa setiap elemennya memiliki invers.

example {G : Type*} [Group G] (x : G) : x * x⁻¹ = 1 := mul_inv_cancel x

Serupa dengan taktik ring yang telah kita lihat, terdapat taktik group yang membuktikan setiap identitas yang berlaku dalam sembarang grup. (Secara ekuivalen, taktik ini membuktikan identitas yang berlaku dalam grup bebas.)

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

Terdapat pula taktik bernama abel untuk identitas dalam grup aditif komutatif.

example {G : Type*} [AddCommGroup G] (x y z : G) : z + x + (y - z - x) = y := by
  abel

Menariknya, morfisme grup tidak lebih dari morfisme monoid di antara grup. Karena itu, kita dapat menyalin salah satu contoh terdahulu dan mengganti Monoid dengan Group.

example {G H : Type*} [Group G] [Group H] (x y : G) (f : G →* H) : f (x * y) = f x * f y :=
  f.map_mul x y

Tentu saja, kita memperoleh beberapa sifat baru, seperti berikut:

example {G H : Type*} [Group G] [Group H] (x : G) (f : G →* H) : f (x⁻¹) = (f x)⁻¹ :=
  f.map_inv x

Anda mungkin khawatir bahwa pembangunan morfisme grup mengharuskan kita melakukan pekerjaan yang tidak perlu. Definisi morfisme monoid mewajibkan elemen netral dipetakan ke elemen netral, padahal hal tersebut berlaku otomatis bagi morfisme grup. Dalam praktiknya pekerjaan tambahan ini tidak sulit, tetapi untuk menghindarinya tersedia fungsi yang membangun morfisme grup dari fungsi di antara grup yang kompatibel dengan hukum komposisi.

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

Terdapat pula tipe MulEquiv bagi isomorfisme grup (atau monoid), yang dinyatakan dengan ≃* (serta AddEquiv, yang dinyatakan dengan ≃+ dalam notasi aditif). Invers dari f : G ≃* H adalah MulEquiv.symm f : H ≃* G, komposisi f dan g adalah MulEquiv.trans f g, dan isomorfisme identitas pada G adalah MulEquiv.refl G. Dengan notasi proyektor anonim, dua yang pertama masing-masing dapat ditulis f.symm dan f.trans g. Elemen tipe ini secara otomatis dikoersikan menjadi morfisme dan fungsi apabila diperlukan.

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

Kita dapat menggunakan MulEquiv.ofBijective untuk membangun isomorfisme dari morfisme bijektif. Cara ini membuat fungsi inversnya tidak dapat dihitung.

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

9.1.3. Subgrup

Sebagaimana morfisme grup dibundel, subgrup dari G juga merupakan struktur terbundel yang terdiri atas himpunan di G beserta sifat-sifat ketertutupan yang relevan.

example {G : Type*} [Group G] (H : Subgroup G) {x y : G} (hx : x ∈ H) (hy : y ∈ H) :
    x * y ∈ H :=
  H.mul_mem hx hy

example {G : Type*} [Group G] (H : Subgroup G) {x : G} (hx : x ∈ H) :
    x⁻¹ ∈ H :=
  H.inv_mem hx

Dalam contoh di atas, penting untuk dipahami bahwa Subgroup G merupakan tipe subgrup dari G, bukan predikat IsSubgroup H dengan H sebagai elemen Set G. Subgroup G dilengkapi koersi ke Set G dan predikat keanggotaan pada G. Lihat Bab 8.3 untuk penjelasan mengenai cara dan alasan hal ini dilakukan.

Tentu saja, dua subgrup sama jika dan hanya jika keduanya memiliki elemen yang sama. Fakta ini didaftarkan untuk digunakan bersama taktik ext. Taktik tersebut dapat membuktikan kesamaan dua subgrup dengan cara yang sama seperti ketika membuktikan kesamaan dua himpunan.

Sebagai contoh, untuk menyatakan dan membuktikan bahwa ℤ merupakan subgrup aditif dari ℚ, sebenarnya kita ingin mengonstruksi term bertipe AddSubgroup ℚ yang proyeksinya ke Set ℚ adalah ℤ, atau secara lebih tepat, citra ℤ di ℚ.

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

Dengan menggunakan kelas tipe, Mathlib mengetahui bahwa subgrup dari suatu grup mewarisi struktur grup.

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

Contoh ini memiliki seluk-beluk. Objek H bukanlah tipe, tetapi Lean secara otomatis mengkoersikannya menjadi tipe dengan menafsirkannya sebagai subtipe dari G. Karena itu, contoh di atas dapat dinyatakan ulang secara lebih eksplisit sebagai berikut:

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

Manfaat penting dari penggunaan tipe Subgroup G alih-alih predikat IsSubgroup : Set G → Prop adalah bahwa Subgroup G dapat dengan mudah dilengkapi struktur tambahan. Secara khusus, tipe tersebut memiliki struktur kekisi lengkap terhadap inklusi. Sebagai contoh, alih-alih memiliki lemma yang menyatakan bahwa irisan dua subgrup dari G kembali merupakan subgrup, kita menggunakan operasi kekisi ⊓ untuk mengonstruksi irisannya. Selanjutnya, kita dapat menerapkan sembarang lemma tentang kekisi pada konstruksi tersebut.

Mari kita periksa bahwa himpunan yang mendasari infimum dua subgrup memang, berdasarkan definisi, merupakan irisan keduanya.

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

Mungkin tampak aneh menggunakan notasi yang berbeda bagi sesuatu yang pada dasarnya merupakan irisan himpunan-himpunan yang mendasarinya. Namun, korespondensi tersebut tidak berlaku bagi operasi supremum dan gabungan himpunan, sebab gabungan subgrup pada umumnya bukan subgrup. Sebagai gantinya, kita perlu menggunakan subgrup yang dibangkitkan oleh gabungan tersebut, yang dilakukan dengan Subgroup.closure.

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]

Seluk-beluk lainnya adalah bahwa G itu sendiri tidak bertipe Subgroup G. Karena itu, kita memerlukan cara untuk membicarakan G sebagai subgrup dari G. Hal ini juga disediakan oleh struktur kekisi: subgrup penuh merupakan elemen teratas kekisi tersebut.

example {G : Type*} [Group G] (x : G) : x ∈ (⊤ : Subgroup G) := trivial

Serupa dengan itu, elemen terbawah kekisi ini adalah subgrup yang satu-satunya elemen adalah elemen netral.

example {G : Type*} [Group G] (x : G) : x ∈ (⊥ : Subgroup G) ↔ x = 1 := Subgroup.mem_bot

Sebagai latihan memanipulasi grup dan subgrup, Anda dapat mendefinisikan konjugat suatu subgrup oleh elemen grup induknya.

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
    sorry
  inv_mem' := by
    dsimp
    sorry
  mul_mem' := by
    dsimp
    sorry

Dengan menghubungkan dua topik sebelumnya, kita dapat mengambil citra langsung dan prapeta subgrup menggunakan morfisme grup. Konvensi penamaan dalam Mathlib menyebut kedua operasi tersebut map dan comap. Nama-nama ini bukan istilah matematika yang lazim, tetapi lebih singkat daripada "citra langsung" dan "prapeta".

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'

#check Subgroup.mem_map
#check Subgroup.mem_comap

Secara khusus, prapeta subgrup terbawah di bawah morfisme f merupakan subgrup yang disebut kernel dari f, dan citra f juga merupakan subgrup.

example {G H : Type*} [Group G] [Group H] (f : G →* H) (g : G) :
    g ∈ MonoidHom.ker f ↔ f g = 1 :=
  f.mem_ker

example {G H : Type*} [Group G] [Group H] (f : G →* H) (h : H) :
    h ∈ MonoidHom.range f ↔ ∃ g : G, f g = h :=
  f.mem_range

Sebagai latihan memanipulasi morfisme grup dan subgrup, mari kita buktikan beberapa sifat elementer. Sifat-sifat ini sudah dibuktikan dalam Mathlib, jadi jangan terlalu cepat menggunakan exact? jika ingin memperoleh manfaat dari latihan ini.

section exercises
variable {G H : Type*} [Group G] [Group H]

open Subgroup

example (φ : G →* H) (S T : Subgroup H) (hST : S ≤ T) : comap φ S ≤ comap φ T := by
  sorry

example (φ : G →* H) (S T : Subgroup G) (hST : S ≤ T) : map φ S ≤ map φ T := by
  sorry

variable {K : Type*} [Group K]

-- Ingat bahwa Anda dapat memakai taktik `ext` untuk membuktikan kesamaan subgrup.
example (φ : G →* H) (ψ : H →* K) (U : Subgroup K) :
    comap (ψ.comp φ) U = comap φ (comap ψ U) := by
  sorry

-- Mengambil citra langsung subgrup melalui satu homomorfisme lalu homomorfisme lain
-- sama dengan mengambil citra langsungnya melalui komposisi kedua homomorfisme.
example (φ : G →* H) (ψ : H →* K) (S : Subgroup G) :
    map (ψ.comp φ) S = map ψ (S.map φ) := by
  sorry

end exercises

Mari kita akhiri pengantar tentang subgrup dalam Mathlib ini dengan dua hasil klasik. Teorema Lagrange menyatakan bahwa kardinalitas subgrup dari suatu grup hingga membagi kardinalitas grup tersebut. Teorema pertama Sylow merupakan konvers parsial yang terkenal dari teorema Lagrange.

Walaupun bagian Mathlib ini sebagian disiapkan untuk memungkinkan penghitungan, kita tetap dapat meminta Lean menggunakan logika nonkonstruktif melalui perintah open scoped berikut.

open scoped Classical


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⟩

open Subgroup

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

Dua latihan berikut menurunkan sebuah korolari dari lemma Lagrange. (Hasil ini juga sudah tersedia di Mathlib, jadi jangan terlalu cepat menggunakan exact?.)

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]
  sorry

#check card_dvd_of_le

lemma inf_bot_of_coprime {G : Type*} [Group G] (H K : Subgroup G)
    (h : (Nat.card H).Coprime (Nat.card K)) : H ⊓ K = ⊥ := by
  sorry

9.1.4. Grup konkret

Kita juga dapat memanipulasi grup konkret dalam Mathlib, walaupun hal ini biasanya lebih rumit daripada bekerja dengan teori abstrak. Sebagai contoh, untuk sembarang tipe X, grup permutasi dari X adalah Equiv.Perm X. Secara khusus, grup simetris \(\mathfrak{S}_n\) adalah Equiv.Perm (Fin n). Kita dapat menyatakan hasil abstrak mengenai grup ini, misalnya bahwa Equiv.Perm X dibangkitkan oleh siklus apabila X hingga.

open Equiv

example {X : Type*} [Finite X] : Subgroup.closure {σ : Perm X | Perm.IsCycle σ} = ⊤ :=
  Perm.closure_isCycle

Kita dapat bekerja sepenuhnya secara konkret dan menghitung hasil kali siklus yang sebenarnya. Di bawah ini kita menggunakan perintah #simp, yang memanggil taktik simp pada ekspresi yang diberikan. Notasi c[] digunakan untuk mendefinisikan permutasi siklik. Dalam contoh tersebut, hasilnya merupakan permutasi dari ℕ. Kita dapat memberikan penetapan tipe seperti (1 : Fin 5) pada bilangan pertama agar penghitungan berlangsung dalam Perm (Fin 5).

#simp [mul_assoc] c[1, 2, 3] * c[2, 3, 4]

Cara lain untuk bekerja dengan grup konkret adalah menggunakan grup bebas dan presentasi grup. Grup bebas pada tipe α adalah FreeGroup α, dan pemetaan inklusinya adalah FreeGroup.of : α → FreeGroup α. Sebagai contoh, mari kita definisikan tipe S dengan tiga elemen yang dilambangkan a, b, dan c, serta elemen ab⁻¹ dari grup bebas yang bersesuaian.

section FreeGroup

inductive S | a | b | c

open S

def myElement : FreeGroup S := (.of a) * (.of b)⁻¹

Perhatikan bahwa kita memberikan tipe yang diharapkan bagi definisi tersebut agar Lean mengetahui bahwa .of berarti FreeGroup.of.

Sifat universal grup bebas diwujudkan oleh ekuivalensi FreeGroup.lift. Sebagai contoh, mari kita definisikan morfisme grup dari FreeGroup S ke Perm (Fin 5) yang memetakan a ke c[1, 2, 3], b ke c[2, 3, 1], dan c ke c[2, 3].

def myMorphism : FreeGroup S →* Perm (Fin 5) :=
  FreeGroup.lift fun | .a => c[1, 2, 3]
                     | .b => c[2, 3, 1]
                     | .c => c[2, 3]

Sebagai contoh konkret terakhir, mari kita lihat cara mendefinisikan grup yang dibangkitkan oleh satu elemen dengan pangkat tiga sama dengan satu (sehingga grup tersebut isomorfik dengan \(\mathbb{Z}/3\)), lalu membangun morfisme dari grup tersebut ke Perm (Fin 5).

Sebagai tipe yang memiliki tepat satu elemen, kita akan menggunakan Unit, yang satu-satunya elemennya dilambangkan dengan (). Fungsi PresentedGroup menerima himpunan relasi, yakni himpunan elemen dari suatu grup bebas, dan menghasilkan hasil bagi grup bebas tersebut oleh subgrup normal yang dibangkitkan oleh relasi-relasi itu. (Kita akan melihat cara menangani hasil bagi yang lebih umum dalam Bab 9.1.6.) Karena detail ini kita sembunyikan di balik sebuah definisi, kita menggunakan deriving Group untuk memaksa pembuatan instans grup pada myGroup.

def myGroup := PresentedGroup {.of () ^ 3} deriving Group

Sifat universal grup berpresentasi memastikan bahwa morfisme dari grup ini dapat dibangun dari fungsi yang memetakan relasi ke elemen netral grup sasaran. Karena itu, kita memerlukan fungsi semacam itu beserta bukti bahwa syaratnya terpenuhi. Selanjutnya, bukti tersebut dapat diberikan kepada PresentedGroup.toGroup untuk memperoleh morfisme grup yang diinginkan.

def myMap : Unit → Perm (Fin 5)
| () => c[1, 2, 3]

lemma compat_myMap :
    ∀ r ∈ ({.of () ^ 3} : Set (FreeGroup Unit)), FreeGroup.lift myMap r = 1 := by
  rintro _ rfl
  simp
  decide

def myNewMorphism : myGroup →* Perm (Fin 5) := PresentedGroup.toGroup compat_myMap

end FreeGroup

9.1.5. Aksi grup

Salah satu cara penting teori grup berinteraksi dengan bidang matematika lainnya adalah melalui aksi grup. Aksi suatu grup G pada tipe X tidak lebih dari morfisme dari G ke Equiv.Perm X. Jadi, dalam arti tertentu, aksi grup sudah tercakup oleh pembahasan sebelumnya. Namun, kita tidak ingin terus membawa morfisme tersebut; sebisa mungkin, kita ingin Lean menyimpulkannya secara otomatis. Karena itu, tersedia kelas tipe MulAction G X.

Kekurangan pengaturan ini adalah bahwa beberapa aksi dari grup yang sama pada tipe yang sama memerlukan sejumlah penyesuaian, misalnya dengan mendefinisikan sinonim tipe yang masing-masing membawa instans kelas tipe berbeda.

Secara khusus, pengaturan ini memungkinkan kita menggunakan g • x untuk menyatakan aksi elemen grup g pada titik x.

noncomputable section GroupActions

example {G X : Type*} [Group G] [MulAction G X] (g g': G) (x : X) :
    g • (g' • x) = (g * g') • x :=
  (mul_smul g g' x).symm

Terdapat pula versi bagi grup aditif bernama AddAction, dengan aksinya dinyatakan oleh +ᵥ. Versi ini antara lain digunakan dalam definisi ruang afin.

example {G X : Type*} [AddGroup G] [AddAction G X] (g g' : G) (x : X) :
    g +ᵥ (g' +ᵥ x) = (g + g') +ᵥ x :=
  (add_vadd g g' x).symm

Morfisme grup yang mendasarinya disebut MulAction.toPermHom.

open MulAction

example {G X : Type*} [Group G] [MulAction G X] : G →* Equiv.Perm X :=
  toPermHom G X

Sebagai ilustrasi, mari kita lihat cara mendefinisikan isomorfisme Cayley yang menyematkan sembarang grup G ke grup permutasi, yaitu Perm G. Untuk membuat instans [MulAction G G], Lean menemukan aksi grup baku yang diberikan oleh perkalian kiri, tepat seperti yang kita inginkan.

def CayleyIsoMorphism (G : Type*) [Group G] : G ≃* (toPermHom G G).range :=
  Equiv.Perm.subgroupOfMulAction G G

Perhatikan bahwa sebelum definisi di atas, tidak ada sesuatu pun yang mengharuskan kita memiliki grup alih-alih monoid (atau, sebenarnya, sembarang tipe yang dilengkapi operasi perkalian).

Syarat grup baru benar-benar berperan ketika kita ingin mempartisi X menjadi orbit. Relasi ekuivalensi yang bersesuaian pada X disebut MulAction.orbitRel. Relasi tersebut tidak dideklarasikan sebagai instans global.

example {G X : Type*} [Group G] [MulAction G X] : Setoid X := orbitRel G X

Dengan menggunakan relasi ini, kita dapat menyatakan bahwa X dipartisi menjadi orbit-orbit di bawah aksi G. Secara lebih tepat, kita memperoleh bijeksi antara X dan produk dependen (ω : orbitRel.Quotient G X) × (orbit G (Quotient.out ω)), dengan Quotient.out ω sekadar memilih elemen yang diproyeksikan ke ω. Ingat bahwa elemen produk dependen ini merupakan pasangan ⟨ω, x⟩, dengan tipe orbit G (Quotient.out ω) dari x bergantung pada ω.

example {G X : Type*} [Group G] [MulAction G X] :
    X ≃ (ω : orbitRel.Quotient G X) × (orbit G (Quotient.out ω)) :=
  MulAction.selfEquivSigmaOrbits G X

Secara khusus, ketika X hingga, hasil ini dapat digabungkan dengan Fintype.card_congr dan Fintype.card_sigma untuk menyimpulkan bahwa kardinalitas X merupakan jumlah kardinalitas orbit-orbitnya. Selain itu, orbit-orbit tersebut berkorespondensi bijektif dengan hasil bagi G di bawah aksi stabilisator melalui translasi kiri. Aksi suatu subgrup melalui translasi kiri ini digunakan untuk mendefinisikan hasil bagi grup oleh subgrup dengan notasi /, sehingga kita dapat memakai pernyataan ringkas berikut.

example {G X : Type*} [Group G] [MulAction G X] (x : X) :
    orbit G x ≃ G ⧸ stabilizer G x :=
  MulAction.orbitEquivQuotientStabilizer G x

Kasus khusus penting dari penggabungan dua hasil di atas terjadi ketika X adalah grup G yang dilengkapi aksi subgrup H melalui translasi. Dalam kasus ini, semua stabilisator trivial, sehingga setiap orbit berkorespondensi bijektif dengan H dan kita memperoleh:

example {G : Type*} [Group G] (H : Subgroup G) : G ≃ (G ⧸ H) × H :=
  groupEquivQuotientProdSubgroup

Ini merupakan varian konseptual dari versi teorema Lagrange yang telah kita lihat. Perhatikan bahwa versi ini tidak membuat asumsi keterhinggaan.

Sebagai latihan untuk bagian ini, mari kita bangun aksi suatu grup pada subgrupnya melalui konjugasi, dengan menggunakan definisi conjugate dari latihan sebelumnya.

variable {G : Type*} [Group G]

lemma conjugate_one (H : Subgroup G) : conjugate 1 H = H := by
  sorry

instance : MulAction G (Subgroup G) where
  smul := conjugate
  one_smul := by
    sorry
  mul_smul := by
    sorry

end GroupActions

9.1.6. Grup hasil bagi

Dalam pembahasan di atas mengenai subgrup yang beraksi pada grup, kita melihat kemunculan hasil bagi G ⧸ H. Secara umum, hasil ini hanyalah sebuah tipe. Tipe tersebut dapat dilengkapi struktur grup sedemikian sehingga pemetaan hasil baginya merupakan morfisme grup jika dan hanya jika H merupakan subgrup normal (dan struktur grup tersebut kemudian unik).

Asumsi kenormalan berupa kelas tipe Subgroup.Normal, sehingga inferensi kelas tipe dapat menggunakannya untuk menurunkan struktur grup pada hasil bagi.

noncomputable section QuotientGroup

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

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

Sifat universal grup hasil bagi diakses melalui QuotientGroup.lift: morfisme grup φ menginduksi morfisme pada G ⧸ N segera setelah kernelnya memuat N.

example {G : Type*} [Group G] (N : Subgroup G) [N.Normal] {M : Type*}
    [Group M] (φ : G →* M) (h : N ≤ MonoidHom.ker φ) : G ⧸ N →* M :=
  QuotientGroup.lift N φ h

Fakta bahwa grup sasaran dinamai M dalam cuplikan di atas memberi petunjuk bahwa struktur monoid pada M sebenarnya sudah cukup.

Kasus khusus yang penting adalah ketika N = ker φ. Dalam kasus tersebut, morfisme yang diturunkan bersifat injektif dan kita memperoleh isomorfisme grup ke citranya. Hasil ini sering disebut teorema isomorfisme pertama.

example {G : Type*} [Group G] {M : Type*} [Group M] (φ : G →* M) :
    G ⧸ MonoidHom.ker φ →* MonoidHom.range φ :=
  QuotientGroup.quotientKerEquivRange φ

Dengan menerapkan sifat universal pada komposisi morfisme φ : G →* G' dengan proyeksi grup hasil bagi Quotient.mk' N', kita juga dapat membangun morfisme dari G ⧸ N ke G' ⧸ N'. Syarat yang diperlukan pada φ biasanya dirumuskan dengan mengatakan "φ harus memetakan N ke dalam N'". Namun, hal ini ekuivalen dengan meminta agar prapeta N' di bawah φ memuat N. Syarat terakhir lebih mudah digunakan karena definisi prapeta tidak melibatkan kuantor eksistensial.

example {G G': Type*} [Group G] [Group G']
    {N : Subgroup G} [N.Normal] {N' : Subgroup G'} [N'.Normal]
    {φ : G →* G'} (h : N ≤ Subgroup.comap φ N') : G ⧸ N →* G' ⧸ N':=
  QuotientGroup.map N N' φ h

Satu hal yang perlu diperhatikan adalah bahwa tipe G ⧸ N benar-benar bergantung pada N (hingga kesamaan definisional). Karena itu, bukti bahwa dua subgrup normal N dan M sama belum cukup untuk membuat tipe hasil bagi yang bersesuaian sama secara definisional. Namun, sifat-sifat universal memang memberikan isomorfisme dalam kasus ini.

example {G : Type*} [Group G] {M N : Subgroup G} [M.Normal]
    [N.Normal] (h : M = N) : G ⧸ M ≃* G ⧸ N := QuotientGroup.quotientMulEquivOfEq h

Sebagai rangkaian latihan terakhir untuk bagian ini, kita akan membuktikan bahwa jika H dan K merupakan subgrup normal yang saling lepas dari grup hingga G, dan hasil kali kardinalitas keduanya sama dengan kardinalitas G, maka G isomorfik dengan H × K. Ingat bahwa saling lepas dalam konteks ini berarti H ⊓ K = ⊥.

Kita mulai dengan sedikit bermain menggunakan lemma Lagrange, tanpa mengasumsikan bahwa subgrup-subgrup tersebut normal atau saling lepas.

section
variable {G : Type*} [Group G] {H K : Subgroup G}

open MonoidHom

#check Nat.card_pos -- Argumen tak kosong akan disimpulkan secara otomatis untuk subgrup
#check Subgroup.index_eq_card
#check Subgroup.index_mul_card
#check Nat.eq_of_mul_eq_mul_right

lemma aux_card_eq [Finite G] (h' : Nat.card G = Nat.card H * Nat.card K) :
    Nat.card (G ⧸ H) = Nat.card K := by
  sorry

Mulai sekarang, kita mengasumsikan bahwa subgrup-subgrup kita normal dan saling lepas, serta mengasumsikan syarat kardinalitas. Sekarang kita mengonstruksi blok pembangun pertama bagi isomorfisme yang diinginkan.

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

#check Nat.bijective_iff_injective_and_card
#check ker_eq_bot_iff
#check restrict
#check ker_restrict

def iso₁ : K ≃* G ⧸ H := by
  sorry

Sekarang kita dapat mendefinisikan blok pembangun kedua. Kita akan memerlukan MonoidHom.prod, yang membangun morfisme dari G₀ ke G₁ × G₂ dari dua morfisme yang masing-masing memetakan G₀ ke G₁ dan ke G₂.

def iso₂ : G ≃* (G ⧸ K) × (G ⧸ H) := by
  sorry

Kita siap merangkai semua bagiannya.

#check MulEquiv.prodCongr

def finalIso : G ≃* H × K :=
  sorry

9.2. Gelanggang

9.2.1. Gelanggang, unit, morfisme, dan subgelanggangnya

Tipe struktur gelanggang pada tipe R adalah Ring R. Variannya yang mengasumsikan perkalian komutatif adalah CommRing R. Kita telah melihat bahwa taktik ring akan membuktikan setiap kesamaan yang mengikuti aksioma gelanggang komutatif.

example {R : Type*} [CommRing R] (x y : R) : (x + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y := by ring

Varian yang lebih eksotis tidak mengharuskan penjumlahan pada R membentuk grup, melainkan cukup monoid aditif. Kelas tipe yang bersesuaian adalah Semiring R dan CommSemiring R. Tipe bilangan asli merupakan instans penting dari CommSemiring ℕ; demikian pula setiap tipe fungsi yang nilainya berupa bilangan asli. Contoh penting lainnya adalah tipe ideal dalam gelanggang, yang akan dibahas di bawah. Nama taktik ring menyesatkan dalam dua hal: taktik ini mengasumsikan komutativitas, tetapi juga bekerja pada semigelanggang. Dengan kata lain, taktik tersebut berlaku bagi setiap CommSemiring.

example (x y : ℕ) : (x + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y := by ring

Ada pula versi kelas gelanggang dan semigelanggang yang tidak mengasumsikan adanya unit multiplikatif atau sifat asosiatif perkalian. Kita tidak akan membahasnya di sini.

Sebagian konsep yang biasanya diajarkan dalam pengantar teori gelanggang sebenarnya menyangkut monoid multiplikatif yang mendasarinya. Contoh utamanya ialah definisi unit suatu gelanggang. Setiap monoid (multiplikatif) M memiliki predikat IsUnit : M → Prop yang menyatakan keberadaan invers dua sisi, tipe unit Units M dengan notasi Mˣ, serta koersi ke M. Tipe Units M membundel elemen yang dapat dibalik bersama inversnya dan sifat-sifat yang memastikan bahwa keduanya benar-benar saling invers.

Perincian implementasi ini terutama relevan ketika mendefinisikan fungsi yang dapat dihitung. Dalam kebanyakan keadaan, kita dapat menggunakan IsUnit.unit {x : M} : IsUnit x → Mˣ untuk membangun sebuah unit. Dalam kasus komutatif, tersedia pula Units.mkOfMulEqOne (x y : M) : x * y = 1 → Mˣ, yang membangun x sebagai sebuah unit.

example (x : ℤˣ) : x = 1 ∨ x = -1 := Int.units_eq_one_or x

example {M : Type*} [Monoid M] (x : Mˣ) : (x : M) * x⁻¹ = 1 := Units.mul_inv x

example {M : Type*} [Monoid M] : Group Mˣ := inferInstance

Tipe morfisme gelanggang di antara dua (semi)gelanggang R dan S adalah RingHom R S, dengan notasi R →+* S.

example {R S : Type*} [Ring R] [Ring S] (f : R →+* S) (x y : R) :
    f (x + y) = f x + f y := f.map_add x y

example {R S : Type*} [Ring R] [Ring S] (f : R →+* S) : Rˣ →* Sˣ :=
  Units.map f

Varian isomorfismenya adalah RingEquiv, dengan notasi ≃+*.

Seperti pada submonoid dan subgrup, terdapat tipe Subring R untuk subgelanggang dari gelanggang R. Namun, tipe ini jauh kurang berguna daripada tipe subgrup karena kita tidak dapat mengambil hasil bagi gelanggang terhadap subgelanggang.

example {R : Type*} [Ring R] (S : Subring R) : Ring S := inferInstance

Perhatikan pula bahwa RingHom.range menghasilkan subgelanggang.

9.2.2. Ideal dan hasil bagi

Karena alasan historis, Mathlib hanya memiliki teori ideal untuk gelanggang komutatif. (Pustaka gelanggang semula dikembangkan untuk mempercepat pembangunan landasan geometri aljabar modern.) Oleh sebab itu, pada bagian ini kita akan bekerja dengan (semi)gelanggang komutatif. Ideal dari R didefinisikan sebagai submodul dari R yang dipandang sebagai modul-R. Modul akan dibahas kelak dalam bab aljabar linear. Perincian implementasi ini sebagian besar dapat diabaikan dengan aman karena kebanyakan—meski tidak semua—lemma yang relevan dinyatakan ulang dalam konteks khusus ideal.

Namun, notasi proyeksi anonim tidak selalu bekerja sebagaimana yang diharapkan. Misalnya, Ideal.Quotient.mk I tidak dapat diganti dengan I.Quotient.mk dalam cuplikan berikut. Karena terdapat dua tanda . dalam ekspresi tersebut, Lean akan mengurainya sebagai (Ideal.Quotient I).mk; padahal Ideal.Quotient sendiri tidak ada.

example {R : Type*} [CommRing R] (I : Ideal R) : R →+* R ⧸ I :=
  Ideal.Quotient.mk I

example {R : Type*} [CommRing R] {a : R} {I : Ideal R} :
    Ideal.Quotient.mk I a = 0 ↔ a ∈ I :=
  Ideal.Quotient.eq_zero_iff_mem

Sifat universal gelanggang hasil bagi diwujudkan oleh Ideal.Quotient.lift.

example {R S : Type*} [CommRing R] [CommRing S] (I : Ideal R) (f : R →+* S)
    (H : I ≤ RingHom.ker f) : R ⧸ I →+* S :=
  Ideal.Quotient.lift I f H

Secara khusus, sifat ini menghasilkan teorema isomorfisme pertama untuk gelanggang.

example {R S : Type*} [CommRing R] [CommRing S](f : R →+* S) :
    R ⧸ RingHom.ker f ≃+* f.range :=
  RingHom.quotientKerEquivRange f

Dengan relasi inklusi, ideal-ideal membentuk kekisi lengkap sekaligus struktur semigelanggang. Kedua struktur ini berinteraksi dengan baik.

variable {R : Type*} [CommRing R] {I J : Ideal R}

example : I + J = I ⊔ J := rfl

example {x : R} : x ∈ I + J ↔ ∃ a ∈ I, ∃ b ∈ J, a + b = x := by
  simp [Submodule.mem_sup]

example : I * J ≤ J := Ideal.mul_le_left

example : I * J ≤ I := Ideal.mul_le_right

example : I * J ≤ I ⊓ J := Ideal.mul_le_inf

Morfisme gelanggang dapat digunakan untuk mengambil citra langsung dan prapeta ideal melalui Ideal.map dan Ideal.comap. Seperti biasa, operasi kedua lebih nyaman digunakan karena tidak melibatkan kuantor eksistensial. Itulah sebabnya operasi tersebut dipakai untuk menyatakan syarat yang memungkinkan kita membangun morfisme di antara gelanggang hasil bagi.

example {R S : Type*} [CommRing R] [CommRing S] (I : Ideal R) (J : Ideal S) (f : R →+* S)
    (H : I ≤ Ideal.comap f J) : R ⧸ I →+* S ⧸ J :=
  Ideal.quotientMap J f H

Satu hal yang perlu diperhatikan ialah bahwa tipe R ⧸ I benar-benar bergantung pada I (hingga kesamaan definisional). Karena itu, bukti bahwa dua ideal I dan J sama belum cukup untuk membuat tipe hasil bagi yang bersesuaian sama secara definisional. Meskipun demikian, sifat universal memang memberikan isomorfisme dalam kasus ini.

example {R : Type*} [CommRing R] {I J : Ideal R} (h : I = J) : R ⧸ I ≃+* R ⧸ J :=
  Ideal.quotEquivOfEq h

Sekarang kita dapat menyajikan isomorfisme sisa Tionghoa sebagai contoh. Perhatikan perbedaan antara simbol infimum terindeks ⨅ dan simbol produk besar tipe Π. Bergantung pada fon yang digunakan, keduanya dapat sangat sulit dibedakan.

example {R : Type*} [CommRing R] {ι : Type*} [Fintype ι] (f : ι → Ideal R)
    (hf : ∀ i j, i ≠ j → IsCoprime (f i) (f j)) : (R ⧸ ⨅ i, f i) ≃+* Π i, R ⧸ f i :=
  Ideal.quotientInfRingEquivPiQuotient f hf

Versi elementer teorema sisa Tionghoa, yakni pernyataan tentang ZMod, dapat dengan mudah diturunkan dari hasil sebelumnya:

open BigOperators PiNotation

example {ι : Type*} [Fintype ι] (a : ι → ℕ) (coprime : ∀ i j, i ≠ j → (a i).Coprime (a j)) :
    ZMod (∏ i, a i) ≃+* Π i, ZMod (a i) :=
  ZMod.prodEquivPi a coprime

Sebagai rangkaian latihan, kita akan membuktikan kembali teorema sisa Tionghoa dalam kasus umum.

Pertama-tama, dengan sifat universal gelanggang hasil bagi, kita perlu mendefinisikan pemetaan yang muncul dalam teorema tersebut sebagai morfisme gelanggang.

variable {ι R : Type*} [CommRing R]
open Ideal Quotient Function

#check Pi.ringHom
#check ker_Pi_Quotient_mk

/-- Homomorfisme dari ``R ⧸ ⨅ i, I i`` ke ``Π i, R ⧸ I i`` yang tampil dalam
  teorema sisa Tionghoa. -/
def chineseMap (I : ι → Ideal R) : (R ⧸ ⨅ i, I i) →+* Π i, R ⧸ I i :=
  sorry

Pastikan dua lemma berikut dapat dibuktikan dengan rfl.

lemma chineseMap_mk (I : ι → Ideal R) (x : R) :
    chineseMap I (Quotient.mk _ x) = fun i : ι ↦ Ideal.Quotient.mk (I i) x :=
  sorry

lemma chineseMap_mk' (I : ι → Ideal R) (x : R) (i : ι) :
    chineseMap I (mk _ x) i = mk (I i) x :=
  sorry

Lemma berikut membuktikan separuh yang mudah dari teorema sisa Tionghoa tanpa asumsi apa pun mengenai keluarga idealnya. Panjang buktinya kurang dari satu baris.

#check injective_lift_iff

lemma chineseMap_inj (I : ι → Ideal R) : Injective (chineseMap I) := by
  sorry

Sekarang kita siap menghadapi inti teorema, yaitu menunjukkan surjektivitas chineseMap. Pertama-tama, kita perlu mengetahui berbagai cara untuk menyatakan asumsi koprimalitas (juga disebut asumsi komaksimalitas). Hanya dua cara pertama yang akan diperlukan di bawah.

#check IsCoprime
#check isCoprime_iff_add
#check isCoprime_iff_exists
#check isCoprime_iff_sup_eq
#check isCoprime_iff_codisjoint

Kita menggunakan kesempatan ini untuk menerapkan induksi pada Finset. Lemma yang relevan mengenai Finset diberikan di bawah. Ingat bahwa taktik ring bekerja pada semigelanggang dan bahwa ideal-ideal suatu gelanggang membentuk semigelanggang.

#check Finset.mem_insert_of_mem
#check Finset.mem_insert_self

theorem isCoprime_Inf {I : Ideal R} {J : ι → Ideal R} {s : Finset ι}
    (hf : ∀ j ∈ s, IsCoprime I (J j)) : IsCoprime I (⨅ j ∈ s, J j) := by
  classical
  simp_rw [isCoprime_iff_add] at *
  induction s using Finset.induction with
  | empty =>
      simp
  | @insert i s _ hs =>
      rw [Finset.iInf_insert, inf_comm, one_eq_top, eq_top_iff, ← one_eq_top]
      set K := ⨅ j ∈ s, J j
      calc
        1 = I + K                  := sorry
        _ = I + K * (I + J i)      := sorry
        _ = (1 + K) * I + K * J i  := sorry
        _ ≤ I + K ⊓ J i            := sorry

Sekarang kita dapat membuktikan surjektivitas pemetaan yang muncul dalam teorema sisa Tionghoa.

lemma chineseMap_surj [Fintype ι] {I : ι → Ideal R}
    (hI : ∀ i j, i ≠ j → IsCoprime (I i) (I j)) : Surjective (chineseMap I) := by
  classical
  intro g
  choose f hf using fun i ↦ Ideal.Quotient.mk_surjective (g i)
  have key : ∀ i, ∃ e : R, mk (I i) e = 1 ∧ ∀ j, j ≠ i → mk (I j) e = 0 := by
    intro i
    have hI' : ∀ j ∈ ({i} : Finset ι)ᶜ, IsCoprime (I i) (I j) := by
      sorry
    sorry
  choose e he using key
  use mk _ (∑ i, f i * e i)
  sorry

Sekarang semua bagian tersebut berpadu dalam definisi berikut:

noncomputable def chineseIso [Fintype ι] (f : ι → Ideal R)
    (hf : ∀ i j, i ≠ j → IsCoprime (f i) (f j)) : (R ⧸ ⨅ i, f i) ≃+* Π i, R ⧸ f i :=
  { Equiv.ofBijective _ ⟨chineseMap_inj f, chineseMap_surj hf⟩,
    chineseMap f with }

9.2.3. Aljabar dan polinomial

Jika diberikan (semi)gelanggang komutatif R, sebuah aljabar atas R adalah semigelanggang A yang dilengkapi morfisme gelanggang dari R ke A dan setiap elemen dalam citra morfisme tersebut berkomutasi dengan setiap elemen A. Hal ini dikodekan sebagai kelas tipe Algebra R A. Morfisme dari R ke A disebut pemetaan struktur dan dinotasikan sebagai algebraMap R A : R →+* A dalam Lean. Perkalian a : A dengan algebraMap R A r untuk suatu r : R disebut perkalian skalar a oleh r dan dinotasikan sebagai r • a. Perhatikan bahwa pengertian aljabar ini kadang-kadang disebut aljabar unital asosiatif untuk menekankan adanya pengertian aljabar yang lebih umum.

Fakta bahwa algebraMap R A merupakan morfisme gelanggang mengemas banyak sifat perkalian skalar, seperti berikut ini:

example {R A : Type*} [CommRing R] [Ring A] [Algebra R A] (r r' : R) (a : A) :
    (r + r') • a = r • a + r' • a :=
  add_smul r r' a

example {R A : Type*} [CommRing R] [Ring A] [Algebra R A] (r r' : R) (a : A) :
    (r * r') • a = r • r' • a :=
  mul_smul r r' a

Morfisme di antara dua aljabar-R, A dan B, adalah morfisme gelanggang yang menghormati perkalian skalar oleh elemen R. Morfisme tersebut terbundel dalam tipe AlgHom R A B, yang dinotasikan sebagai A →ₐ[R] B.

Contoh penting aljabar nonkomutatif mencakup aljabar endomorfisme dan aljabar matriks persegi; keduanya akan dibahas dalam bab aljabar linear. Dalam bab ini, kita akan membahas salah satu contoh terpenting aljabar komutatif, yaitu aljabar polinomial.

Aljabar polinomial satu peubah dengan koefisien dalam R disebut Polynomial R dan dapat ditulis sebagai R[X] setelah namespace Polynomial dibuka. Pemetaan struktur aljabar dari R ke R[X] dinotasikan sebagai C. Huruf ini berarti "konstan" karena fungsi polinomial yang bersesuaian selalu konstan. Peubah tak tentunya dinotasikan sebagai X.

open Polynomial

example {R : Type*} [CommRing R] : R[X] := X

example {R : Type*} [CommRing R] (r : R) := X - C r

Dalam contoh pertama di atas, kita harus memberikan tipe yang diharapkan kepada Lean karena tipe tersebut tidak dapat ditentukan dari badan definisi. Dalam contoh kedua, aljabar polinomial sasaran dapat disimpulkan dari penggunaan C r karena tipe r diketahui.

Karena C merupakan morfisme gelanggang dari R ke R[X], kita dapat menggunakan semua lemma morfisme gelanggang, seperti map_zero, map_one, map_mul, dan map_pow, sebelum menghitung dalam gelanggang R[X]. Sebagai contoh:

example {R : Type*} [CommRing R] (r : R) : (X + C r) * (X - C r) = X ^ 2 - C (r ^ 2) := by
  rw [C.map_pow]
  ring

Koefisien dapat diakses menggunakan Polynomial.coeff.

example {R : Type*} [CommRing R] (r:R) : (C r).coeff 0 = r := by simp

example {R : Type*} [CommRing R] : (X ^ 2 + 2 * X + C 3 : R[X]).coeff 1 = 2 := by simp

Mendefinisikan derajat polinomial selalu rumit karena kasus khusus polinomial nol. Mathlib memiliki dua varian: Polynomial.natDegree : R[X] → ℕ memberikan derajat 0 kepada polinomial nol, sedangkan Polynomial.degree : R[X] → WithBot ℕ memberikan ⊥. Pada varian kedua, WithBot ℕ dapat dipandang sebagai ℕ ∪ {-∞}, hanya saja -∞ dinotasikan sebagai ⊥, yakni simbol yang sama dengan elemen terbawah dalam kekisi lengkap. Nilai khusus ini digunakan sebagai derajat polinomial nol dan bersifat menyerap terhadap penjumlahan. (Nilai ini hampir menyerap terhadap perkalian, kecuali bahwa ⊥ * 0 = 0.)

Secara konseptual, versi degree merupakan versi yang tepat. Sebagai contoh, versi ini memungkinkan kita menyatakan rumus yang diharapkan bagi derajat hasil kali (dengan asumsi gelanggang dasar tidak memiliki pembagi nol).

example {R : Type*} [Semiring R] [NoZeroDivisors R] {p q : R[X]} :
    degree (p * q) = degree p + degree q :=
  Polynomial.degree_mul

Sebaliknya, versi untuk natDegree perlu mengasumsikan bahwa kedua polinomial tidak nol.

example {R : Type*} [Semiring R] [NoZeroDivisors R] {p q : R[X]} (hp : p ≠ 0) (hq : q ≠ 0) :
    natDegree (p * q) = natDegree p + natDegree q :=
  Polynomial.natDegree_mul hp hq

Namun, ℕ jauh lebih nyaman digunakan daripada WithBot ℕ. Karena itu, Mathlib menyediakan kedua versi beserta lemma untuk mengonversi di antara keduanya. Selain itu, natDegree merupakan definisi yang lebih nyaman ketika menghitung derajat komposisi. Komposisi polinomial diberikan oleh Polynomial.comp, dan kita memiliki:

example {R : Type*} [Semiring R] [NoZeroDivisors R] {p q : R[X]} :
    natDegree (comp p q) = natDegree p * natDegree q :=
  Polynomial.natDegree_comp

Polinomial menghasilkan fungsi polinomial: setiap polinomial dapat dievaluasi pada R menggunakan Polynomial.eval.

example {R : Type*} [CommRing R] (P: R[X]) (x : R) := P.eval x

example {R : Type*} [CommRing R] (r : R) : (X - C r).eval r = 0 := by simp

Secara khusus, terdapat predikat IsRoot yang berlaku bagi elemen r dalam R yang membuat suatu polinomial bernilai nol.

example {R : Type*} [CommRing R] (P : R[X]) (r : R) : IsRoot P r ↔ P.eval r = 0 := Iff.rfl

Dengan asumsi R tidak memiliki pembagi nol, kita ingin mengatakan bahwa jumlah akar suatu polinomial tidak melebihi derajatnya, dengan memperhitungkan multiplisitas akar. Namun, sekali lagi kasus polinomial nol menyulitkan. Karena itu, Mathlib mendefinisikan Polynomial.roots yang memetakan polinomial P ke sebuah multihimpunan: multihimpunan ini didefinisikan kosong apabila P nol, dan selain itu memuat akar-akar P beserta multiplisitasnya. Definisi ini hanya tersedia ketika gelanggang yang mendasari merupakan domain, sebab tanpa syarat tersebut definisinya tidak memiliki sifat yang baik.

example {R : Type*} [CommRing R] [IsDomain R] (r : R) : (X - C r).roots = {r} :=
  roots_X_sub_C r

example {R : Type*} [CommRing R] [IsDomain R] (r : R) (n : ℕ):
    ((X - C r) ^ n).roots = n • {r} :=
  by simp

Baik Polynomial.eval maupun Polynomial.roots hanya mempertimbangkan gelanggang koefisien. Keduanya tidak memungkinkan kita mengatakan bahwa X ^ 2 - 2 : ℚ[X] memiliki akar dalam ℝ atau bahwa X ^ 2 + 1 : ℝ[X] memiliki akar dalam ℂ. Untuk itu, kita memerlukan Polynomial.aeval, yang mengevaluasi P : R[X] dalam sembarang aljabar-R. Lebih tepatnya, jika diberikan semigelanggang A dan instans Algebra R A, Polynomial.aeval memetakan setiap elemen a : A ke morfisme aljabar-R R[X] → A yang mengevaluasi X pada a. Karena AlgHom memiliki koersi ke fungsi, morfisme tersebut dapat diterapkan pada polinomial. Namun, aeval tidak menerima polinomial sebagai argumen langsung, sehingga notasi titik seperti pada P.eval di atas tidak dapat digunakan.

example : aeval Complex.I (X ^ 2 + 1 : ℝ[X]) = 0 := by simp

Fungsi yang bersesuaian dengan roots dalam konteks ini adalah aroots. Fungsi tersebut menerima sebuah polinomial lalu sebuah aljabar dan menghasilkan multihimpunan (dengan catatan yang sama mengenai polinomial nol seperti pada roots).

open Complex Polynomial

example : aroots (X ^ 2 + 1 : ℝ[X]) ℂ = {Complex.I, -I} := by
  suffices roots (X ^ 2 + 1 : ℂ[X]) = {I, -I} by simpa [aroots_def]
  have factored : (X ^ 2 + 1 : ℂ[X]) = (X - C I) * (X - C (-I)) := by
    have key : (C I * C I : ℂ[X]) = -1 := by simp [← C_mul]
    rw [C_neg]
    linear_combination key
  have p_ne_zero : (X - C I) * (X - C (-I)) ≠ 0 := by
    intro H
    apply_fun eval 0 at H
    simp [eval] at H
  simp only [factored, roots_mul p_ne_zero, roots_X_sub_C]
  rfl

-- Mathlib mengetahui teorema d'Alembert–Gauss: ``ℂ`` tertutup secara aljabar.
example : IsAlgClosed ℂ := inferInstance

Secara lebih umum, jika diberikan morfisme gelanggang f : R →+* S, kita dapat mengevaluasi P : R[X] pada suatu titik dalam S menggunakan Polynomial.eval₂. Fungsi ini benar-benar menghasilkan fungsi dari R[X] ke S karena tidak mengasumsikan adanya instans Algebra R S; oleh sebab itu, notasi titik bekerja sebagaimana yang diharapkan.

#check (Complex.ofRealHom : ℝ →+* ℂ)

example : (X ^ 2 + 1 : ℝ[X]).eval₂ Complex.ofRealHom Complex.I = 0 := by simp

Mari kita akhiri dengan membahas polinomial multipeubah secara singkat. Jika diberikan semigelanggang komutatif R, aljabar-R dari polinomial berkoefisien dalam R dengan peubah tak tentu yang diindeks oleh tipe σ adalah MvPolynomial σ R. Jika diberikan i : σ, polinomial yang bersesuaian adalah MvPolynomial.X i. (Seperti biasa, namespace MvPolynomial dapat dibuka agar penulisannya dipersingkat menjadi X i.) Misalnya, jika kita menginginkan dua peubah tak tentu, kita dapat memakai Fin 2 sebagai σ dan menulis polinomial yang mendefinisikan lingkaran satuan dalam \(\mathbb{R}^2\) sebagai berikut:

open MvPolynomial

def circleEquation : MvPolynomial (Fin 2) ℝ := X 0 ^ 2 + X 1 ^ 2 - 1

Ingat bahwa penerapan fungsi memiliki prioritas sangat tinggi, sehingga ekspresi di atas dibaca sebagai (X 0) ^ 2 + (X 1) ^ 2 - 1. Kita dapat mengevaluasinya untuk memastikan bahwa titik berkoordinat \((1, 0)\) terletak pada lingkaran. Ingat bahwa notasi ![...] menyatakan elemen Fin n → X untuk suatu bilangan asli n yang ditentukan oleh banyaknya argumen dan suatu tipe X yang ditentukan oleh tipe argumen-argumennya.

example : MvPolynomial.eval ![1, 0] circleEquation = 0 := by simp [circleEquation]