8. Hierarki

Dalam Bab 7, kita telah melihat cara mendefinisikan kelas grup dan membangun instans kelas tersebut, lalu cara membangun instans kelas gelanggang komutatif. Namun, tentu saja terdapat hierarki di sini: gelanggang komutatif khususnya merupakan grup aditif. Dalam bab ini, kita akan mempelajari cara membangun hierarki semacam itu. Hierarki muncul di semua cabang matematika, tetapi dalam bab ini penekanannya terletak pada contoh-contoh aljabar.

Membahas cara membangun hierarki sebelum membahas lebih jauh penggunaan hierarki yang sudah ada mungkin terasa terlalu dini. Namun, pemahaman tertentu tentang teknologi yang mendasari hierarki diperlukan untuk menggunakannya. Karena itu, Anda sebaiknya tetap membaca bab ini, tetapi pada pembacaan pertama tidak perlu terlalu berusaha mengingat semuanya. Setelah itu, bacalah bab-bab berikutnya dan kembali ke sini untuk pembacaan kedua.

Dalam bab ini, kita akan mendefinisikan ulang versi yang lebih sederhana dari banyak hal yang terdapat di Mathlib, sehingga kita akan menggunakan indeks untuk membedakan versi kita. Misalnya, Ring₁ akan menjadi versi kita dari Ring. Karena kita akan secara bertahap menjelaskan cara-cara yang lebih canggih untuk memformalkan struktur, indeks tersebut kadang-kadang akan bertambah melampaui satu.

8.1. Dasar-Dasar

Pada lapisan paling bawah dari semua hierarki di Lean, terdapat kelas-kelas yang membawa data. Kelas berikut mencatat bahwa tipe α yang diberikan dilengkapi sebuah elemen khusus bernama one. Pada tahap ini, elemen tersebut sama sekali belum memiliki sifat apa pun.

class One₁ (α : Type) where
  /-- Elemen satu -/
  one : α

Karena dalam bab ini kita akan jauh lebih banyak menggunakan kelas, kita perlu memahami secara lebih terperinci apa yang dilakukan perintah class. Pertama, perintah class di atas mendefinisikan struktur One₁ dengan parameter α : Type dan satu field one. Perintah tersebut juga menandai struktur ini sebagai kelas, sehingga argumen bertipe One₁ α untuk suatu tipe α dapat disimpulkan melalui prosedur resolusi instans, asalkan ditandai sebagai argumen implisit-instans, yakni ditulis di antara tanda kurung siku. Kedua efek ini juga dapat diperoleh dengan menggunakan perintah structure beserta atribut class, yakni dengan menulis @[class] structure alih-alih class. Namun, perintah untuk mendefinisikan kelas juga memastikan bahwa One₁ α muncul sebagai argumen implisit-instans pada field-fieldnya sendiri. Bandingkan:

#check One₁.one -- One₁.one {α : Type} [self : One₁ α] : α

@[class] structure One₂ (α : Type) where
  /-- Elemen satu -/
  one : α

#check One₂.one

Pada pemeriksaan kedua, terlihat bahwa self : One₂ α merupakan argumen eksplisit. Mari kita pastikan bahwa versi pertama memang dapat digunakan tanpa argumen eksplisit apa pun.

example (α : Type) [One₁ α] : α := One₁.one

Catatan: dalam contoh di atas, argumen One₁ α ditandai sebagai implisit-instans. Hal ini sedikit ganjil karena penandaan tersebut hanya memengaruhi penggunaan deklarasi, sedangkan deklarasi yang dibuat oleh perintah example tidak dapat digunakan. Namun, cara ini memungkinkan kita tidak memberi nama pada argumen tersebut dan, yang lebih penting, mulai membiasakan diri menandai argumen One₁ α sebagai implisit-instans.

Catatan lainnya adalah bahwa semua ini hanya akan bekerja apabila Lean mengetahui tipe α. Dalam contoh di atas, jika penetapan tipe : α dihilangkan, Lean akan menghasilkan pesan galat seperti: typeclass instance problem is stuck, it is often due to metavariables One₁ (?m.263 α). Di sini, ?m.263 α berarti "suatu tipe yang bergantung pada α" (dan 263 hanyalah indeks yang dibuat secara otomatis untuk membedakan beberapa hal yang belum diketahui). Cara lain untuk menghindari masalah ini adalah menggunakan anotasi tipe, seperti berikut:

example (α : Type) [One₁ α] := (One₁.one : α)

Anda mungkin telah menjumpai masalah ini ketika bereksperimen dengan limit barisan di Bab 3.6. Misalnya, hal itu terjadi jika Anda mencoba menyatakan 0 < 1 tanpa memberi tahu Lean apakah pertidaksamaan tersebut berkaitan dengan bilangan asli atau bilangan real.

Tugas kita berikutnya adalah memberikan notasi kepada One₁.one. Karena kita tidak ingin berbenturan dengan notasi bawaan untuk 1, kita akan menggunakan 𝟙. Hal ini dilakukan oleh perintah berikut; baris pertamanya meminta Lean menggunakan dokumentasi One₁.one sebagai dokumentasi untuk simbol 𝟙.

@[inherit_doc]
notation "𝟙" => One₁.one

example {α : Type} [One₁ α] : α := 𝟙

example {α : Type} [One₁ α] : (𝟙 : α) = 𝟙 := rfl

Sekarang kita menginginkan kelas pembawa data yang mencatat suatu operasi biner. Untuk saat ini, kita tidak ingin memilih antara penjumlahan dan perkalian, sehingga kita akan menggunakan simbol wajik.

class Dia₁ (α : Type) where
  dia : α → α → α

infixl:70 " ⋄ "   => Dia₁.dia

Seperti dalam contoh One₁, pada tahap ini operasinya sama sekali belum memiliki sifat apa pun. Sekarang mari kita definisikan kelas struktur semigrup yang operasinya dinyatakan dengan ⋄. Untuk sementara, kita mendefinisikannya secara manual sebagai struktur dengan dua field: sebuah instans Dia₁ dan field bernilai Prop bernama dia_assoc yang menyatakan sifat asosiatif dari ⋄.

class Semigroup₀ (α : Type) where
  toDia₁ : Dia₁ α
  /-- Operasi wajik bersifat asosiatif -/
  dia_assoc : ∀ a b c : α, a ⋄ b ⋄ c = a ⋄ (b ⋄ c)

Perhatikan bahwa ketika dia_assoc dinyatakan, field toDia₁ yang telah didefinisikan berada dalam konteks lokal. Karena itu, field tersebut dapat digunakan ketika Lean mencari instans Dia₁ α untuk memaknai a ⋄ b. Namun, field toDia₁ ini tidak menjadi bagian dari basis data instans kelas tipe. Akibatnya, penulisan example {α : Type} [Semigroup₀ α] (a b : α) : α := a ⋄ b akan gagal dengan pesan galat failed to synthesize instance Dia₁ α.

Kita dapat memperbaikinya dengan menambahkan atribut instance sesudahnya.

attribute [instance] Semigroup₀.toDia₁

example {α : Type} [Semigroup₀ α] (a b : α) : α := a ⋄ b

Sebelum melanjutkan pembangunan hierarki, kita perlu memakai sintaks yang berbeda untuk menambahkan field toDia₁ ini. Sintaks tersebut memberi tahu Lean agar memperlakukan Dia₁ α seolah-olah field-fieldnya merupakan field milik Semigroup₁ sendiri. Sintaks ini juga secara otomatis menambahkan instans toDia₁. Perintah class mendukung hal tersebut melalui sintaks extends, seperti berikut:

class Semigroup₁ (α : Type) extends toDia₁ : Dia₁ α where
  /-- Operasi wajik bersifat asosiatif -/
  dia_assoc : ∀ a b c : α, a ⋄ b ⋄ c = a ⋄ (b ⋄ c)

example {α : Type} [Semigroup₁ α] (a b : α) : α := a ⋄ b

Perhatikan bahwa sintaks ini juga tersedia pada perintah structure. Namun, dalam kasus tersebut sintaks ini hanya mengatasi kerepotan menulis field seperti toDia₁, karena tidak ada instans yang perlu didefinisikan.

Nama field toDia₁ bersifat opsional dalam sintaks extends. Secara baku, nama field diambil dari nama kelas yang diperluas lalu diberi prefiks "to".

class Semigroup₂ (α : Type) extends Dia₁ α where
  /-- Operasi wajik bersifat asosiatif -/
  dia_assoc : ∀ a b c : α, a ⋄ b ⋄ c = a ⋄ (b ⋄ c)

Sekarang mari kita coba menggabungkan operasi wajik dengan sebuah elemen satu khusus, beserta aksioma yang menyatakan bahwa elemen tersebut netral di kedua sisi.

class DiaOneClass₁ (α : Type) extends One₁ α, Dia₁ α where
  /-- Satu adalah elemen netral kiri untuk wajik. -/
  one_dia : ∀ a : α, 𝟙 ⋄ a = a
  /-- Satu adalah elemen netral kanan untuk wajik. -/
  dia_one : ∀ a : α, a ⋄ 𝟙 = a

Dalam contoh berikut, kita memberi tahu Lean bahwa α memiliki struktur DiaOneClass₁, lalu menyatakan sebuah sifat yang menggunakan instans Dia₁ dan instans One₁ sekaligus. Untuk melihat cara Lean menemukan instans-instans tersebut, kita mengaktifkan opsi pelacakan yang hasilnya dapat dilihat di Infoview. Secara baku, hasil ini cukup ringkas, tetapi dapat diperluas dengan mengeklik baris yang berakhir dengan panah hitam. Hasil tersebut mencakup percobaan gagal ketika Lean berusaha menemukan instans sebelum memiliki informasi tipe yang cukup. Percobaan yang berhasil memang melibatkan instans yang dihasilkan oleh sintaks extends.

set_option trace.Meta.synthInstance true in
example {α : Type} [DiaOneClass₁ α] (a b : α) : Prop := a ⋄ b = 𝟙

Perhatikan bahwa kita tidak perlu menyertakan field tambahan ketika menggabungkan kelas-kelas yang sudah ada. Karena itu, monoid dapat didefinisikan sebagai berikut:

class Monoid₁ (α : Type) extends Semigroup₁ α, DiaOneClass₁ α

Walaupun definisi di atas tampak langsung, ada satu seluk-beluk penting yang tersembunyi. Semigroup₁ α dan DiaOneClass₁ α sama-sama memperluas Dia₁ α. Karena itu, kita mungkin khawatir bahwa sebuah instans Monoid₁ α akan memberi dua operasi wajik yang tidak berkaitan pada α: satu berasal dari field Monoid₁.toSemigroup₁ dan satu lagi dari field Monoid₁.toDiaOneClass₁.

Memang, jika kita mencoba membangun kelas monoid secara manual dengan:

class Monoid₂ (α : Type) where
  toSemigroup₁ : Semigroup₁ α
  toDiaOneClass₁ : DiaOneClass₁ α

kita akan memperoleh dua operasi wajik yang sama sekali tidak berkaitan, Monoid₂.toSemigroup₁.toDia₁.dia dan Monoid₂.toDiaOneClass₁.toDia₁.dia.

Versi yang dihasilkan dengan sintaks extends tidak memiliki cacat ini.

example {α : Type} [Monoid₁ α] :
  (Monoid₁.toSemigroup₁.toDia₁.dia : α → α → α) = Monoid₁.toDiaOneClass₁.toDia₁.dia := rfl

Jadi, perintah class telah melakukan semacam keajaiban bagi kita (dan perintah structure juga akan melakukan hal yang sama). Cara mudah untuk melihat field-field kelas kita adalah dengan memeriksa konstruktornya. Bandingkan:

/- Monoid₂.mk {α : Type} (toSemigroup₁ : Semigroup₁ α) (toDiaOneClass₁ : DiaOneClass₁ α) : Monoid₂ α -/
#check Monoid₂.mk

/- Monoid₁.mk {α : Type} [toSemigroup₁ : Semigroup₁ α] [toOne₁ : One₁ α] (one_dia : ∀ (a : α), 𝟙 ⋄ a = a) (dia_one : ∀ (a : α), a ⋄ 𝟙 = a) : Monoid₁ α -/
#check Monoid₁.mk

Jadi, terlihat bahwa Monoid₁ menerima argumen Semigroup₁ α seperti yang diharapkan. Namun, ia tidak menerima argumen DiaOneClass₁ α yang akan tumpang-tindih; sebaliknya, argumen itu diurai dan hanya bagian yang tidak tumpang-tindih yang disertakan. Lean juga secara otomatis menghasilkan instans Monoid₁.toDiaOneClass₁. Instans ini bukan sebuah field, tetapi memiliki tipe yang diharapkan dan, dari sudut pandang pengguna akhir, memulihkan simetri antara dua kelas yang diperluas, Semigroup₁ dan DiaOneClass₁.

#check Monoid₁.toSemigroup₁
#check Monoid₁.toDiaOneClass₁

Sekarang kita hampir dapat mendefinisikan grup. Kita dapat menambahkan field pada struktur monoid yang menyatakan keberadaan invers untuk setiap elemen. Akan tetapi, kita kemudian harus bekerja lebih jauh untuk mengakses invers tersebut. Dalam praktik, invers lebih mudah ditambahkan sebagai data. Agar dapat digunakan kembali secara optimal, kita mendefinisikan kelas pembawa data baru lalu memberinya notasi.

class Inv₁ (α : Type) where
  /-- Fungsi inversi -/
  inv : α → α

@[inherit_doc]
postfix:max "⁻¹" => Inv₁.inv

class Group₁ (G : Type) extends Monoid₁ G, Inv₁ G where
  inv_dia : ∀ a : G, a⁻¹ ⋄ a = 𝟙

Definisi di atas mungkin tampak terlalu lemah: kita hanya meminta agar a⁻¹ menjadi invers kiri dari a. Namun, sifat pada sisi lainnya berlaku secara otomatis. Untuk membuktikannya, kita memerlukan sebuah lemma pendahuluan.

lemma left_inv_eq_right_inv₁ {M : Type} [Monoid₁ M] {a b c : M} (hba : b ⋄ a = 𝟙) (hac : a ⋄ c = 𝟙) : b = c := by
  rw [← DiaOneClass₁.one_dia c, ← hba, Semigroup₁.dia_assoc, hac, DiaOneClass₁.dia_one b]

Dalam lemma ini, penggunaan nama lengkap cukup merepotkan, terlebih karena kita harus mengetahui bagian hierarki mana yang menyediakan setiap fakta. Salah satu cara mengatasinya adalah memakai perintah export untuk menyalin fakta-fakta tersebut sebagai lemma ke namespace akar.

export DiaOneClass₁ (one_dia dia_one)
export Semigroup₁ (dia_assoc)
export Group₁ (inv_dia)

Selanjutnya, bukti di atas dapat ditulis ulang sebagai berikut:

example {M : Type} [Monoid₁ M] {a b c : M} (hba : b ⋄ a = 𝟙) (hac : a ⋄ c = 𝟙) : b = c := by
  rw [← one_dia c, ← hba, dia_assoc, hac, dia_one b]

Sekarang giliran Anda membuktikan beberapa hal tentang struktur aljabar kita.

lemma inv_eq_of_dia [Group₁ G] {a b : G} (h : a ⋄ b = 𝟙) : a⁻¹ = b :=
  sorry

lemma dia_inv [Group₁ G] (a : G) : a ⋄ a⁻¹ = 𝟙 :=
  sorry

Pada tahap ini, kita ingin beralih ke definisi gelanggang, tetapi ada masalah serius. Struktur gelanggang pada suatu tipe memuat struktur grup aditif, struktur monoid multiplikatif, dan beberapa sifat mengenai interaksi keduanya. Namun, sejauh ini kita telah menetapkan notasi ⋄ secara langsung untuk semua operasi. Pada tingkat yang lebih mendasar, sistem kelas tipe mengasumsikan bahwa setiap tipe hanya memiliki satu instans dari masing-masing kelas tipe.

Ada berbagai cara untuk menyelesaikan masalah ini. Agak mengejutkan, Mathlib menggunakan gagasan sederhana untuk menggandakan segala sesuatu bagi teori aditif dan multiplikatif dengan bantuan atribut pembangkit kode. Struktur dan kelas didefinisikan dalam notasi aditif maupun multiplikatif, lalu dihubungkan dengan atribut to_additive. Dalam kasus pewarisan berganda seperti pada semigrup, instans "pemulih simetri" yang dibuat secara otomatis juga perlu ditandai. Bagian ini agak teknis; Anda tidak perlu memahami perinciannya. Pokok pentingnya adalah bahwa lemma cukup dinyatakan dalam notasi multiplikatif dan diberi atribut to_additive. Sebagai contoh, lemma multiplikatif left_inv_eq_right_inv' akan menghasilkan versi aditif left_neg_eq_right_neg' secara otomatis. Untuk memeriksa nama versi aditif tersebut, kita menggunakan perintah whatsnew in pada left_inv_eq_right_inv'.

class AddSemigroup₃ (α : Type) extends Add α where
  /-- Penjumlahan bersifat asosiatif -/
  add_assoc₃ : ∀ a b c : α, a + b + c = a + (b + c)

@[to_additive AddSemigroup₃]
class Semigroup₃ (α : Type) extends Mul α where
  /-- Perkalian bersifat asosiatif -/
  mul_assoc₃ : ∀ a b c : α, a * b * c = a * (b * c)

class AddMonoid₃ (α : Type) extends AddSemigroup₃ α, AddZeroClass α

@[to_additive AddMonoid₃]
class Monoid₃ (α : Type) extends Semigroup₃ α, MulOneClass α

export Semigroup₃ (mul_assoc₃)
export AddSemigroup₃ (add_assoc₃)

whatsnew in
@[to_additive]
lemma left_inv_eq_right_inv' {M : Type} [Monoid₃ M] {a b c : M} (hba : b * a = 1) (hac : a * c = 1) : b = c := by
  rw [← one_mul c, ← hba, mul_assoc₃, hac, mul_one b]

#check left_neg_eq_right_neg'

Dilengkapi teknologi ini, kita juga dapat dengan mudah mendefinisikan semigrup komutatif, monoid komutatif, dan grup komutatif, lalu mendefinisikan gelanggang.

class AddCommSemigroup₃ (α : Type) extends AddSemigroup₃ α where
  add_comm : ∀ a b : α, a + b = b + a

@[to_additive AddCommSemigroup₃]
class CommSemigroup₃ (α : Type) extends Semigroup₃ α where
  mul_comm : ∀ a b : α, a * b = b * a

class AddCommMonoid₃ (α : Type) extends AddMonoid₃ α, AddCommSemigroup₃ α

@[to_additive AddCommMonoid₃]
class CommMonoid₃ (α : Type) extends Monoid₃ α, CommSemigroup₃ α

class AddGroup₃ (G : Type) extends AddMonoid₃ G, Neg G where
  neg_add : ∀ a : G, -a + a = 0

@[to_additive AddGroup₃]
class Group₃ (G : Type) extends Monoid₃ G, Inv G where
  inv_mul : ∀ a : G, a⁻¹ * a = 1

Kita perlu ingat untuk menandai lemma dengan simp apabila sesuai.

attribute [simp] Group₃.inv_mul AddGroup₃.neg_add

Selanjutnya, kita perlu sedikit mengulang karena beralih ke notasi baku. Namun, setidaknya to_additive menangani penerjemahan dari notasi multiplikatif ke notasi aditif.

@[to_additive]
lemma inv_eq_of_mul [Group₃ G] {a b : G} (h : a * b = 1) : a⁻¹ = b :=
  sorry

Perhatikan bahwa kita dapat meminta to_additive menandai sebuah lemma dengan simp dan meneruskan atribut tersebut ke versi aditifnya sebagai berikut.

@[to_additive (attr := simp)]
lemma Group₃.mul_inv {G : Type} [Group₃ G] (a : G) : a * a⁻¹ = 1 := by
  sorry

@[to_additive]
lemma mul_left_cancel₃ {G : Type} [Group₃ G] {a b c : G} (h : a * b = a * c) : b = c := by
  sorry

@[to_additive]
lemma mul_right_cancel₃ {G : Type} [Group₃ G] {a b c : G} (h : b*a = c*a) : b = c := by
  sorry

class AddCommGroup₃ (G : Type) extends AddGroup₃ G, AddCommMonoid₃ G

@[to_additive AddCommGroup₃]
class CommGroup₃ (G : Type) extends Group₃ G, CommMonoid₃ G

Sekarang kita siap mendefinisikan gelanggang. Untuk tujuan demonstrasi, kita tidak akan mengasumsikan bahwa penjumlahan bersifat komutatif, lalu langsung menyediakan instans AddCommGroup₃. Mathlib tidak memakai cara ini. Pertama, dalam praktiknya cara tersebut tidak mempermudah pembuatan instans gelanggang. Kedua, hierarki aljabar Mathlib melewati semigelanggang, yang menyerupai gelanggang tetapi tidak memiliki lawan, sehingga bukti di bawah tidak berlaku untuknya.

Selain menjadi latihan yang bagus jika Anda belum pernah melihatnya, pendekatan ini memberi kita contoh pembangunan instans dengan sintaks yang memungkinkan struktur induk diberikan sebagai parameter instans, lalu field tambahan dipasok secara terpisah. Di sini, argumen Ring₃ R menyediakan semua yang diperlukan AddCommGroup₃ R kecuali add_comm.

class Ring₃ (R : Type) extends AddGroup₃ R, Monoid₃ R, MulZeroClass R where
  /-- Perkalian distributif kiri terhadap penjumlahan -/
  left_distrib : ∀ a b c : R, a * (b + c) = a * b + a * c
  /-- Perkalian distributif kanan terhadap penjumlahan -/
  right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c

instance {R : Type} [Ring₃ R] : AddCommGroup₃ R :=
{ add_comm := by
    sorry }

Tentu saja kita juga dapat membangun instans konkret, misalnya struktur gelanggang pada bilangan bulat. Instans di bawah memanfaatkan semua pekerjaan yang telah diselesaikan di Mathlib.

instance : Ring₃ ℤ where
  add := (· + ·)
  add_assoc₃ := add_assoc
  zero := 0
  zero_add := by simp
  add_zero := by simp
  neg := (- ·)
  neg_add := by simp
  mul := (· * ·)
  mul_assoc₃ := mul_assoc
  one := 1
  one_mul := by simp
  mul_one := by simp
  zero_mul := by simp
  mul_zero := by simp
  left_distrib := Int.mul_add
  right_distrib := Int.add_mul

Sebagai latihan, sekarang Anda dapat menyusun hierarki sederhana bagi relasi urutan. Hierarki ini mencakup kelas monoid komutatif terurut, yang memiliki struktur urutan parsial sekaligus struktur monoid komutatif sedemikian sehingga ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b. Tentu saja, Anda perlu menambahkan field dan mungkin klausa extends pada kelas-kelas berikut.

class LE₁ (α : Type) where
  /-- Relasi kurang dari atau sama dengan. -/
  le : α → α → Prop

@[inherit_doc] infix:50 " ≤₁ " => LE₁.le

class Preorder₁ (α : Type)

class PartialOrder₁ (α : Type)

class OrderedCommMonoid₁ (α : Type)

instance : OrderedCommMonoid₁ ℕ where

Sekarang kita akan membahas struktur aljabar yang melibatkan beberapa tipe. Contoh utamanya adalah modul atas gelanggang. Jika Anda belum mengetahui apa itu modul, anggap saja modul berarti ruang vektor dan semua gelanggang kita adalah medan. Struktur tersebut merupakan grup aditif komutatif yang dilengkapi perkalian skalar oleh elemen suatu gelanggang.

Pertama, kita mendefinisikan kelas tipe pembawa data untuk perkalian skalar oleh suatu tipe α pada tipe β, lalu memberinya notasi asosiatif kanan.

class SMul₃ (α : Type) (β : Type) where
  /-- Perkalian skalar -/
  smul : α → β → β

infixr:73 " • " => SMul₃.smul

Selanjutnya kita dapat mendefinisikan modul (sekali lagi, bayangkan ruang vektor jika Anda belum mengenal modul).

class Module₁ (R : Type) [Ring₃ R] (M : Type) [AddCommGroup₃ M] extends SMul₃ R M where
  zero_smul : ∀ m : M, (0 : R) • m = 0
  one_smul : ∀ m : M, (1 : R) • m = m
  mul_smul : ∀ (a b : R) (m : M), (a * b) • m = a • b • m
  add_smul : ∀ (a b : R) (m : M), (a + b) • m = a • m + b • m
  smul_add : ∀ (a : R) (m n : M), a • (m + n) = a • m + a • n

Ada sesuatu yang menarik di sini. Tidak terlalu mengejutkan bahwa struktur gelanggang pada R menjadi parameter dalam definisi ini, tetapi Anda mungkin menduga AddCommGroup₃ M akan menjadi bagian dari klausa extends, sama seperti SMul₃ R M. Jika kita mencobanya, akan terbentuk field Module₁.toAddCommGroup₃ yang ditandai sebagai instans. Instans tersebut akan memiliki tipe: (R : Type) → [inst : Ring₃ R] → {M : Type} → [self : Module₁ R M] → AddCommGroup₃ M. Dengan instans seperti itu di basis data kelas tipe, setiap kali Lean mencari instans AddCommGroup₃ M bagi suatu M, ia harus terlebih dahulu memburu tipe R yang sama sekali belum ditentukan beserta instans Ring₃ R, sebelum memulai pencarian utama atas instans Module₁ R M. Kedua pencarian sampingan ini direpresentasikan oleh metavariabel dalam pesan galat, yang masing-masing dilambangkan dengan ?R dan ?inst✝. Instans Module₁.toAddCommGroup₃ semacam itu akan menjadi jebakan besar bagi prosedur resolusi instans.

Lalu bagaimana dengan extends SMul₃ R M? Klausa ini membuat field Module₁.toSMul₃ : {R : Type} →  [inst : Ring₃ R] → {M : Type} → [inst_1 : AddCommGroup₃ M] → [self : Module₁ R M] → SMul₃ R M. Hasil akhirnya, SMul₃ R M, menyebut R maupun M, sehingga field ini aman digunakan sebagai instans. Aturannya mudah diingat: setiap kelas yang muncul dalam klausa extends harus menyebut setiap tipe yang muncul dalam parameter.

Mari kita buat instans modul pertama: suatu gelanggang merupakan modul atas dirinya sendiri, dengan perkaliannya sebagai perkalian skalar.

instance selfModule (R : Type) [Ring₃ R] : Module₁ R R where
  smul := fun r s ↦ r*s
  zero_smul := zero_mul
  one_smul := one_mul
  mul_smul := mul_assoc₃
  add_smul := Ring₃.right_distrib
  smul_add := Ring₃.left_distrib

Sebagai contoh kedua, setiap grup abelian merupakan modul atas ℤ (inilah salah satu alasan untuk memperumum teori ruang vektor dengan mengizinkan skalar yang tidak dapat dibalik). Pertama, kita dapat mendefinisikan perkalian skalar dengan bilangan asli pada setiap tipe yang dilengkapi nol dan penjumlahan: n • a didefinisikan sebagai a + ⋯ + a, dengan a muncul sebanyak n kali. Definisi ini kemudian diperluas menjadi perkalian skalar dengan bilangan bulat dengan memastikan bahwa (-1) • a = -a.

def nsmul₁ {M : Type*} [Zero M] [Add M] : ℕ → M → M
  | 0, _ => 0
  | n + 1, a => a + nsmul₁ n a

def zsmul₁ {M : Type*} [Zero M] [Add M] [Neg M] : ℤ → M → M
  | Int.ofNat n, a => nsmul₁ n a
  | Int.negSucc n, a => -nsmul₁ n.succ a

Membuktikan bahwa konstruksi ini menghasilkan struktur modul sedikit melelahkan dan tidak menarik bagi pembahasan sekarang, sehingga kita akan membiarkan semua aksiomanya sebagai sorry. Anda tidak diminta mengganti sorry tersebut dengan bukti. Jika tetap ingin melakukannya, Anda mungkin perlu menyatakan dan membuktikan beberapa lemma perantara mengenai nsmul₁ dan zsmul₁.

instance abGrpModule (A : Type) [AddCommGroup₃ A] : Module₁ ℤ A where
  smul := zsmul₁
  zero_smul := sorry
  one_smul := sorry
  mul_smul := sorry
  add_smul := sorry
  smul_add := sorry

Masalah yang jauh lebih penting adalah bahwa sekarang kita memiliki dua struktur modul atas gelanggang ℤ bagi ℤ itu sendiri: abGrpModule ℤ karena ℤ merupakan grup abelian, dan selfModule ℤ karena ℤ merupakan gelanggang. Kedua struktur modul tersebut berkaitan dengan struktur grup abelian yang sama, tetapi belum jelas bahwa keduanya memiliki perkalian skalar yang sama. Sebenarnya memang sama, tetapi fakta ini tidak berlaku berdasarkan definisi dan memerlukan bukti. Ini merupakan kabar yang sangat buruk bagi prosedur resolusi instans kelas tipe dan akan menimbulkan kegagalan yang sangat menjengkelkan bagi pengguna hierarki ini. Ketika diminta secara langsung mencari sebuah instans, Lean akan memilih salah satunya. Kita dapat melihat pilihannya dengan:

#synth Module₁ ℤ ℤ -- abGrpModule ℤ

Namun, dalam konteks yang lebih tidak langsung, Lean dapat menyimpulkan instans yang lain lalu menjadi bingung. Keadaan ini dikenal sebagai wajik buruk. Istilah ini tidak berkaitan dengan operasi wajik yang kita gunakan di atas, melainkan dengan cara menggambar lintasan dari ℤ menuju Module₁ ℤ melalui AddCommGroup₃ ℤ atau Ring₃ ℤ.

Penting untuk dipahami bahwa tidak semua wajik bersifat buruk. Faktanya, wajik terdapat di mana-mana dalam Mathlib, juga dalam bab ini. Sejak awal, kita telah melihat bahwa lintasan dari Monoid₁ α ke Dia₁ α dapat melewati Semigroup₁ α atau DiaOneClass₁ α. Berkat pekerjaan yang dilakukan perintah class, kedua instans Dia₁ α yang dihasilkan sama secara definisional. Secara khusus, wajik dengan kelas bernilai Prop pada bagian bawahnya tidak mungkin buruk, sebab setiap dua bukti atas pernyataan yang sama bersifat sama secara definisional.

Namun, wajik yang kita buat dengan modul benar-benar buruk. Bagian penyebabnya adalah field smul, yang berupa data, bukan bukti, dan kita memiliki dua konstruksi yang tidak sama secara definisional. Cara tangguh untuk memperbaiki masalah ini adalah memastikan bahwa perpindahan dari struktur yang kaya ke struktur yang lebih miskin selalu dilakukan dengan melupakan data, bukan dengan mendefinisikan data. Pola terkenal ini disebut "pewarisan dengan pelupaan data" dan dibahas secara luas dalam https://inria.hal.science/hal-02463336v2.

Dalam kasus konkret kita, definisi AddMonoid₃ dapat diubah agar menyertakan field data nsmul dan beberapa field bernilai Prop yang memastikan bahwa operasi ini terbukti sama dengan operasi yang kita konstruksi di atas. Field-field tersebut diberi nilai baku menggunakan := setelah tipenya dalam definisi di bawah. Berkat nilai baku ini, kebanyakan instans dapat dikonstruksi tepat seperti pada definisi sebelumnya. Namun, dalam kasus khusus ℤ, kita dapat memberikan nilai tertentu.

class AddMonoid₄ (M : Type) extends AddSemigroup₃ M, AddZeroClass M where
  /-- Perkalian dengan bilangan asli. -/
  nsmul : ℕ → M → M := nsmul₁
  /-- Perkalian dengan `(0 : ℕ)` menghasilkan `0`. -/
  nsmul_zero : ∀ x, nsmul 0 x = 0 := by intros; rfl
  /-- Perkalian dengan `(n + 1 : ℕ)` berperilaku seperti yang diharapkan. -/
  nsmul_succ : ∀ (n : ℕ) (x), nsmul (n + 1) x = x + nsmul n x := by intros; rfl

instance mySMul {M : Type} [AddMonoid₄ M] : SMul ℕ M := ⟨AddMonoid₄.nsmul⟩

Mari kita periksa bahwa kita tetap dapat mengonstruksi instans monoid produk tanpa menyediakan field-field yang berkaitan dengan nsmul.

instance (M N : Type) [AddMonoid₄ M] [AddMonoid₄ N] : AddMonoid₄ (M × N) where
  add := fun p q ↦ (p.1 + q.1, p.2 + q.2)
  add_assoc₃ := fun a b c ↦ by ext <;> apply add_assoc₃
  zero := (0, 0)
  zero_add := fun a ↦ by ext <;> apply zero_add
  add_zero := fun a ↦ by ext <;> apply add_zero

Sekarang mari kita tangani kasus khusus ℤ. Di sini, kita ingin membangun nsmul menggunakan koersi dari ℕ ke ℤ dan perkalian pada ℤ. Perhatikan khususnya bahwa field-field bukti memerlukan lebih banyak pekerjaan daripada nilai baku di atas.

instance : AddMonoid₄ ℤ where
  add := (· + ·)
  add_assoc₃ := Int.add_assoc
  zero := 0
  zero_add := Int.zero_add
  add_zero := Int.add_zero
  nsmul := fun n m ↦ (n : ℤ) * m
  nsmul_zero := Int.zero_mul
  nsmul_succ := fun n m ↦ show (n + 1 : ℤ) * m = m + n * m
    by rw [Int.add_mul, Int.add_comm, Int.one_mul]

Mari kita periksa bahwa masalah kita telah terselesaikan. Karena Lean sudah memiliki definisi perkalian skalar antara bilangan asli dan bilangan bulat, dan kita ingin memastikan instans kita yang digunakan, kita tidak akan memakai notasi •. Sebagai gantinya, kita memanggil SMul.smul dan secara eksplisit memberikan instans yang didefinisikan di atas.

example (n : ℕ) (m : ℤ) : SMul.smul (self := mySMul) n m = n * m := rfl

Pembahasan ini kemudian berlanjut dengan memasukkan field zsmul ke dalam definisi grup serta menerapkan kiat-kiat serupa. Sekarang Anda siap membaca definisi monoid, grup, gelanggang, dan modul dalam Mathlib. Definisi tersebut lebih rumit daripada yang telah kita lihat di sini karena menjadi bagian dari hierarki yang sangat besar, tetapi semua prinsip dasarnya telah dijelaskan di atas.

Sebagai latihan, Anda dapat kembali ke hierarki relasi urutan yang dibangun di atas dan mencoba memasukkan kelas tipe LT₁ yang membawa notasi kurang dari <₁. Pastikan bahwa setiap praurutan dilengkapi <₁ dengan nilai baku yang dibangun dari ≤₁ serta sebuah field bernilai Prop yang menyatakan hubungan alami antara kedua operator perbandingan tersebut.

8.2. Morfisme

Sejauh ini dalam bab ini, kita telah membahas cara membuat hierarki struktur matematika. Namun, definisi struktur belum benar-benar lengkap sebelum kita memiliki morfisme. Ada dua pendekatan utama. Pendekatan yang paling jelas adalah mendefinisikan predikat pada fungsi.

def isMonoidHom₁ [Monoid G] [Monoid H] (f : G → H) : Prop :=
  f 1 = 1 ∧ ∀ g g', f (g * g') = f g * f g'

Dalam definisi ini, penggunaan konjungsi sedikit merepotkan. Secara khusus, pengguna harus mengingat urutan yang kita pilih ketika ingin mengakses kedua syarat tersebut. Karena itu, kita dapat menggunakan struktur sebagai gantinya.

structure isMonoidHom₂ [Monoid G] [Monoid H] (f : G → H) : Prop where
  map_one : f 1 = 1
  map_mul : ∀ g g', f (g * g') = f g * f g'

Setelah sampai di sini, kita bahkan mungkin tergoda menjadikannya kelas dan memakai prosedur resolusi instans kelas tipe untuk menyimpulkan isMonoidHom₂ secara otomatis bagi fungsi rumit dari instans-instans fungsi yang lebih sederhana. Sebagai contoh, komposisi morfisme monoid merupakan morfisme monoid, sehingga tampaknya berguna sebagai instans. Namun, instans semacam itu akan sangat sulit bagi prosedur resolusi karena harus menemukan g ∘ f di mana-mana. Kegagalannya pada g (f x) akan sangat menjengkelkan. Secara lebih umum, kita harus selalu mengingat bahwa mengenali fungsi mana yang diterapkan dalam suatu ekspresi merupakan masalah yang sangat sulit, yang disebut "masalah unifikasi orde tinggi". Karena itu, Mathlib tidak menggunakan pendekatan berbasis kelas ini.

Pertanyaan yang lebih mendasar adalah apakah kita menggunakan predikat seperti di atas (melalui def atau structure), atau memakai struktur yang mengemas fungsi beserta predikatnya. Hal ini sebagian merupakan persoalan psikologis. Sangat jarang kita mempertimbangkan fungsi di antara monoid yang bukan morfisme. "Morfisme monoid" benar-benar terasa sebagai nomina, bukan adjektiva yang dapat dilekatkan pada fungsi biasa. Di sisi lain, orang dapat berpendapat bahwa fungsi kontinu di antara ruang topologi memang merupakan fungsi yang kebetulan kontinu. Inilah salah satu alasan Mathlib memiliki predikat Continuous. Sebagai contoh, Anda dapat menulis:

example : Continuous (id : ℝ → ℝ) := continuous_id

Kita tetap memiliki bundel fungsi kontinu, yang antara lain memudahkan pemberian topologi pada suatu ruang fungsi kontinu, tetapi bundel tersebut bukan alat utama untuk bekerja dengan kekontinuan.

Sebaliknya, morfisme di antara monoid (atau struktur aljabar lainnya) dibundel sebagai berikut:

@[ext]
structure MonoidHom₁ (G H : Type) [Monoid G] [Monoid H]  where
  toFun : G → H
  map_one : toFun 1 = 1
  map_mul : ∀ g g', toFun (g * g') = toFun g * toFun g'

Tentu saja kita tidak ingin mengetik toFun di mana-mana. Karena itu, kita mendaftarkan koersi dengan menggunakan kelas tipe CoeFun. Argumen pertamanya adalah tipe yang ingin kita koersikan menjadi fungsi. Argumen kedua menjelaskan tipe fungsi sasaran. Dalam kasus kita, tipenya selalu G → H untuk setiap f : MonoidHom₁ G H. Kita juga menandai MonoidHom₁.toFun dengan atribut coe agar tampil nyaris tak terlihat dalam keadaan taktik, hanya dengan prefiks ↑.

instance [Monoid G] [Monoid H] : CoeFun (MonoidHom₁ G H) (fun _ ↦ G → H) where
  coe := MonoidHom₁.toFun

attribute [coe] MonoidHom₁.toFun

Mari kita periksa bahwa morfisme monoid terbundel memang dapat diterapkan pada sebuah elemen.

example [Monoid G] [Monoid H] (f : MonoidHom₁ G H) : f 1 = 1 :=  f.map_one

Kita dapat melakukan hal yang sama dengan jenis morfisme lain hingga mencapai morfisme gelanggang.

@[ext]
structure AddMonoidHom₁ (G H : Type) [AddMonoid G] [AddMonoid H]  where
  toFun : G → H
  map_zero : toFun 0 = 0
  map_add : ∀ g g', toFun (g + g') = toFun g + toFun g'

instance [AddMonoid G] [AddMonoid H] : CoeFun (AddMonoidHom₁ G H) (fun _ ↦ G → H) where
  coe := AddMonoidHom₁.toFun

attribute [coe] AddMonoidHom₁.toFun

@[ext]
structure RingHom₁ (R S : Type) [Ring R] [Ring S] extends MonoidHom₁ R S, AddMonoidHom₁ R S

Pendekatan ini memiliki beberapa masalah. Masalah kecilnya adalah kita tidak tahu persis di mana harus menempatkan atribut coe, sebab RingHom₁.toFun tidak ada. Fungsi yang relevan ialah MonoidHom₁.toFun ∘ RingHom₁.toMonoidHom₁, yang bukan deklarasi yang dapat ditandai dengan atribut (meskipun kita tetap dapat mendefinisikan instans CoeFun  (RingHom₁ R S) (fun _ ↦ R → S)).

Masalah yang jauh lebih penting adalah bahwa lemma tentang morfisme monoid tidak langsung berlaku pada morfisme gelanggang. Pilihannya adalah mengutak-atik RingHom₁.toMonoidHom₁ setiap kali ingin menerapkan lemma morfisme monoid, atau menyatakan ulang setiap lemma semacam itu bagi morfisme gelanggang. Kedua pilihan ini tidak menarik, sehingga Mathlib menggunakan kiat hierarki baru. Gagasannya adalah mendefinisikan kelas tipe bagi objek yang setidaknya merupakan morfisme monoid, membuat instans kelas tersebut untuk morfisme monoid maupun morfisme gelanggang, lalu menggunakannya untuk menyatakan setiap lemma. Dalam definisi di bawah, F dapat berupa MonoidHom₁ M N, atau RingHom₁ M N apabila M dan N memiliki struktur gelanggang.

class MonoidHomClass₁ (F : Type) (M N : Type) [Monoid M] [Monoid N] where
  toFun : F → M → N
  map_one : ∀ f : F, toFun f 1 = 1
  map_mul : ∀ f g g', toFun f (g * g') = toFun f g * toFun f g'

Namun, implementasi di atas memiliki masalah. Kita belum mendaftarkan instans koersi ke fungsi. Mari kita coba melakukannya sekarang.

def badInst [Monoid M] [Monoid N] [MonoidHomClass₁ F M N] : CoeFun F (fun _ ↦ M → N) where
  coe := MonoidHomClass₁.toFun

Menjadikannya instans merupakan gagasan buruk. Ketika menghadapi bentuk seperti f x dan tipe f bukan tipe fungsi, Lean akan mencoba menemukan instans CoeFun untuk mengoersikan f menjadi fungsi. Fungsi di atas memiliki tipe: {M N F : Type} → [Monoid M] → [Monoid N] → [MonoidHomClass₁ F M N] → CoeFun F (fun x ↦ M → N). Jadi, ketika mencoba menerapkannya, Lean sejak awal tidak mengetahui urutan untuk menyimpulkan tipe-tipe tak diketahui M, N, dan F. Ini merupakan jenis instans buruk yang sedikit berbeda dari yang telah kita lihat, tetapi sumber masalahnya sama: tanpa mengetahui M, Lean harus mencari instans monoid pada tipe yang belum diketahui dan dengan sia-sia mencoba setiap instans monoid di basis data. Jika ingin melihat dampak instans semacam itu, Anda dapat menulis set_option synthInstance.checkSynthOrder false in di atas deklarasi tersebut, mengganti def badInst dengan instance, lalu mencari kegagalan acak dalam berkas ini.

Di sini solusinya mudah: kita perlu memberi tahu Lean agar terlebih dahulu mencari tipe F, lalu menyimpulkan M dan N. Hal ini dilakukan dengan fungsi outParam. Fungsi tersebut didefinisikan sebagai fungsi identitas, tetapi tetap dikenali oleh mekanisme kelas tipe dan memicu perilaku yang diinginkan. Karena itu, kita dapat mencoba lagi mendefinisikan kelas kita dengan memperhatikan fungsi outParam:

class MonoidHomClass₂ (F : Type) (M N : outParam Type) [Monoid M] [Monoid N] where
  toFun : F → M → N
  map_one : ∀ f : F, toFun f 1 = 1
  map_mul : ∀ f g g', toFun f (g * g') = toFun f g * toFun f g'

instance [Monoid M] [Monoid N] [MonoidHomClass₂ F M N] : CoeFun F (fun _ ↦ M → N) where
  coe := MonoidHomClass₂.toFun

attribute [coe] MonoidHomClass₂.toFun

Sekarang kita dapat melanjutkan rencana untuk membuat instans kelas ini.

instance (M N : Type) [Monoid M] [Monoid N] : MonoidHomClass₂ (MonoidHom₁ M N) M N where
  toFun := MonoidHom₁.toFun
  map_one := fun f ↦ f.map_one
  map_mul := fun f ↦ f.map_mul

instance (R S : Type) [Ring R] [Ring S] : MonoidHomClass₂ (RingHom₁ R S) R S where
  toFun := fun f ↦ f.toMonoidHom₁.toFun
  map_one := fun f ↦ f.toMonoidHom₁.map_one
  map_mul := fun f ↦ f.toMonoidHom₁.map_mul

Seperti dijanjikan, setiap lemma yang kita buktikan mengenai f : F dengan asumsi instans MonoidHomClass₂ F M N akan berlaku bagi morfisme monoid maupun morfisme gelanggang. Mari kita lihat sebuah contoh lemma dan periksa bahwa lemma tersebut berlaku dalam kedua keadaan.

lemma map_inv_of_inv [Monoid M] [Monoid N] [MonoidHomClass₂ F M N] (f : F) {m m' : M} (h : m*m' = 1) :
    f m * f m' = 1 := by
  rw [← MonoidHomClass₂.map_mul, h, MonoidHomClass₂.map_one]

example [Monoid M] [Monoid N] (f : MonoidHom₁ M N) {m m' : M} (h : m*m' = 1) : f m * f m' = 1 :=
map_inv_of_inv f h

example [Ring R] [Ring S] (f : RingHom₁ R S) {r r' : R} (h : r*r' = 1) : f r * f r' = 1 :=
map_inv_of_inv f h

Sekilas, mungkin tampak bahwa kita kembali pada gagasan buruk lama untuk menjadikan MonoidHom₁ sebuah kelas. Namun, sebenarnya tidak demikian. Semuanya digeser naik satu tingkat abstraksi. Prosedur resolusi kelas tipe tidak akan mencari fungsi; ia akan mencari MonoidHom₁ atau RingHom₁.

Satu masalah yang tersisa dari pendekatan kita adalah adanya kode berulang di sekitar field toFun, instans CoeFun yang bersesuaian, dan atribut coe. Sebaiknya kita juga mencatat bahwa pola ini hanya digunakan bagi fungsi dengan sifat tambahan, yang berarti koersi ke fungsi harus injektif. Karena itu, Mathlib menambahkan satu lapisan abstraksi lagi melalui kelas dasar DFunLike ("DFun" merupakan singkatan dari istilah bahasa Inggris yang berarti fungsi dependen). Mari kita definisikan ulang MonoidHomClass di atas lapisan dasar ini.

class MonoidHomClass₃ (F : Type) (M N : outParam Type) [Monoid M] [Monoid N] extends
    DFunLike F M (fun _ ↦ N) where
  map_one : ∀ f : F, f 1 = 1
  map_mul : ∀ (f : F) g g', f (g * g') = f g * f g'

instance (M N : Type) [Monoid M] [Monoid N] : MonoidHomClass₃ (MonoidHom₁ M N) M N where
  coe := MonoidHom₁.toFun
  coe_injective' _ _ := MonoidHom₁.ext
  map_one := MonoidHom₁.map_one
  map_mul := MonoidHom₁.map_mul

Tentu saja hierarki morfisme tidak berhenti di sini. Kita dapat melanjutkan dengan mendefinisikan kelas RingHomClass₃ yang memperluas MonoidHomClass₃, lalu membuat instansnya pada RingHom dan kemudian AlgebraHom (aljabar adalah gelanggang dengan struktur tambahan). Namun, kita telah membahas gagasan utama formalisasi morfisme yang digunakan dalam Mathlib. Anda kini seharusnya siap memahami cara morfisme didefinisikan di Mathlib.

Sebagai latihan, cobalah mendefinisikan kelas bagi fungsi pelestari urutan terbundel di antara tipe-tipe terurut, lalu bagi morfisme monoid pelestari urutan. Latihan ini hanya ditujukan untuk berlatih. Seperti fungsi kontinu, fungsi pelestari urutan di Mathlib terutama digunakan tanpa bundel dan didefinisikan melalui predikat Monotone. Tentu saja, Anda perlu melengkapi definisi kelas di bawah.

@[ext]
structure OrderPresHom (α β : Type) [LE α] [LE β] where
  toFun : α → β
  le_of_le : ∀ a a', a ≤ a' → toFun a ≤ toFun a'

@[ext]
structure OrderPresMonoidHom (M N : Type) [Monoid M] [LE M] [Monoid N] [LE N] extends
MonoidHom₁ M N, OrderPresHom M N

class OrderPresHomClass (F : Type) (α β : outParam Type) [LE α] [LE β]

instance (α β : Type) [LE α] [LE β] : OrderPresHomClass (OrderPresHom α β) α β where

instance (α β : Type) [LE α] [Monoid α] [LE β] [Monoid β] :
    OrderPresHomClass (OrderPresMonoidHom α β) α β where

instance (α β : Type) [LE α] [Monoid α] [LE β] [Monoid β] :
    MonoidHomClass₃ (OrderPresMonoidHom α β) α β
  := sorry

8.3. Subobjek

Setelah mendefinisikan suatu struktur aljabar beserta morfismenya, langkah berikutnya adalah mempertimbangkan himpunan yang mewarisi struktur aljabar tersebut, misalnya subgrup atau subgelanggang. Hal ini banyak bertumpang tindih dengan topik sebelumnya. Memang, himpunan pada X diimplementasikan sebagai fungsi dari X ke Prop, sehingga subobjek merupakan fungsi yang memenuhi predikat tertentu. Karena itu, kita dapat menggunakan kembali banyak gagasan yang menghasilkan kelas DFunLike beserta turunannya.

Kita tidak akan menggunakan kembali DFunLike itu sendiri karena hal tersebut akan melanggar penghalang abstraksi dari Set X ke X → Prop. Sebagai gantinya, terdapat kelas SetLike. Alih-alih membungkus injeksi ke suatu tipe fungsi, kelas ini membungkus injeksi ke tipe Set dan mendefinisikan koersi serta instans Membership yang bersesuaian.

@[ext]
structure Submonoid₁ (M : Type) [Monoid M] where
  /-- Himpunan pembawa sebuah submonoid. -/
  carrier : Set M
  /-- Hasil kali dua elemen submonoid termasuk dalam submonoid tersebut. -/
  mul_mem {a b} : a ∈ carrier → b ∈ carrier → a * b ∈ carrier
  /-- Elemen satu termasuk dalam submonoid. -/
  one_mem : 1 ∈ carrier

/-- Submonoid di `M` dapat dipandang sebagai himpunan di `M`. -/
instance [Monoid M] : SetLike (Submonoid₁ M) M where
  coe := Submonoid₁.carrier
  coe_injective' _ _ := Submonoid₁.ext

Dilengkapi instans SetLike di atas, kita sudah dapat menyatakan secara alami bahwa submonoid N memuat 1 tanpa menggunakan N.carrier. Kita juga dapat secara diam-diam memperlakukan N sebagai himpunan di M dan mengambil citra langsungnya di bawah suatu pemetaan.

example [Monoid M] (N : Submonoid₁ M) : 1 ∈ N := N.one_mem

example [Monoid M] (N : Submonoid₁ M) (α : Type) (f : M → α) := f '' N

Kita juga memiliki koersi ke Type yang menggunakan Subtype. Dengan demikian, jika diberikan submonoid N, kita dapat menulis parameter (x : N) yang dapat dikoersikan menjadi elemen M yang termasuk dalam N.

example [Monoid M] (N : Submonoid₁ M) (x : N) : (x : M) ∈ N := x.property

Dengan menggunakan koersi ke Type ini, kita juga dapat menangani tugas melengkapi submonoid dengan struktur monoid. Kita akan menggunakan koersi dari tipe yang terkait dengan N seperti di atas, serta lemma SetCoe.ext yang menyatakan bahwa koersi tersebut injektif. Keduanya disediakan oleh instans SetLike.

instance SubMonoid₁Monoid [Monoid M] (N : Submonoid₁ M) : Monoid N where
  mul := fun x y ↦ ⟨x*y, N.mul_mem x.property y.property⟩
  mul_assoc := fun x y z ↦ SetCoe.ext (mul_assoc (x : M) y z)
  one := ⟨1, N.one_mem⟩
  one_mul := fun x ↦ SetCoe.ext (one_mul (x : M))
  mul_one := fun x ↦ SetCoe.ext (mul_one (x : M))

Perhatikan bahwa pada instans di atas, alih-alih menggunakan koersi ke M dan memanggil field property, kita dapat menggunakan pengikat destrukturisasi sebagai berikut.

example [Monoid M] (N : Submonoid₁ M) : Monoid N where
  mul := fun ⟨x, hx⟩ ⟨y, hy⟩ ↦ ⟨x*y, N.mul_mem hx hy⟩
  mul_assoc := fun ⟨x, _⟩ ⟨y, _⟩ ⟨z, _⟩ ↦ SetCoe.ext (mul_assoc x y z)
  one := ⟨1, N.one_mem⟩
  one_mul := fun ⟨x, _⟩ ↦ SetCoe.ext (one_mul x)
  mul_one := fun ⟨x, _⟩ ↦ SetCoe.ext (mul_one x)

Agar dapat menerapkan lemma tentang submonoid pada subgrup atau subgelanggang, kita memerlukan kelas, sama seperti pada morfisme. Perhatikan bahwa kelas ini menerima instans SetLike sebagai parameter, sehingga tidak memerlukan field pembawa dan dapat menggunakan notasi keanggotaan dalam field-fieldnya.

class SubmonoidClass₁ (S : Type) (M : Type) [Monoid M] [SetLike S M] : Prop where
  mul_mem : ∀ (s : S) {a b : M}, a ∈ s → b ∈ s → a * b ∈ s
  one_mem : ∀ s : S, 1 ∈ s

instance [Monoid M] : SubmonoidClass₁ (Submonoid₁ M) M where
  mul_mem := Submonoid₁.mul_mem
  one_mem := Submonoid₁.one_mem

Sebagai latihan, Anda perlu mendefinisikan struktur Subgroup₁, melengkapinya dengan instans SetLike dan instans SubmonoidClass₁, menempatkan instans Group pada subtipe yang terkait dengan Subgroup₁, serta mendefinisikan kelas SubgroupClass₁.

Hal sangat penting lainnya yang perlu diketahui adalah bahwa subobjek dari suatu objek aljabar di Mathlib selalu membentuk kekisi lengkap, dan struktur ini sering digunakan. Misalnya, Anda mungkin mencari lemma yang menyatakan bahwa irisan submonoid merupakan submonoid. Namun, hal tersebut bukan sebuah lemma, melainkan konstruksi infimum. Mari kita kerjakan kasus dua submonoid.

instance [Monoid M] : Min (Submonoid₁ M) :=
  ⟨fun S₁ S₂ ↦
    { carrier := S₁ ∩ S₂
      one_mem := ⟨S₁.one_mem, S₂.one_mem⟩
      mul_mem := fun ⟨hx, hx'⟩ ⟨hy, hy'⟩ ↦ ⟨S₁.mul_mem hx hy, S₂.mul_mem hx' hy'⟩ }⟩

Hal ini memungkinkan kita memperoleh irisan dua submonoid sebagai submonoid.

example [Monoid M] (N P : Submonoid₁ M) : Submonoid₁ M := N ⊓ P

Anda mungkin menyayangkan bahwa dalam contoh di atas kita harus menggunakan simbol infimum ⊓ alih-alih simbol irisan ∩. Namun, pertimbangkan supremumnya. Gabungan dua submonoid bukanlah submonoid. Meskipun demikian, submonoid tetap membentuk kekisi, bahkan kekisi lengkap. Sebenarnya, N ⊔ P adalah submonoid yang dibangkitkan oleh gabungan N dan P, dan tentu akan sangat membingungkan jika dinyatakan dengan N ∪ P. Karena itu, penggunaan N ⊓ P dapat dipandang jauh lebih konsisten. Notasi tersebut juga jauh lebih konsisten di antara berbagai jenis struktur aljabar.

Pada mulanya, mungkin tampak agak aneh melihat jumlah dua subruang vektor E dan F dinyatakan dengan E ⊔ F alih-alih E + F. Namun, Anda akan terbiasa. Tak lama kemudian, Anda akan menganggap notasi E + F sebagai pengalih perhatian yang menekankan fakta sampingan bahwa elemen E ⊔ F dapat ditulis sebagai jumlah elemen E dan elemen F, alih-alih menekankan fakta mendasar bahwa E ⊔ F merupakan subruang vektor terkecil yang memuat E dan F.

Topik terakhir kita dalam bab ini adalah hasil bagi. Sekali lagi, kita ingin menjelaskan cara Mathlib membangun notasi yang nyaman sambil menghindari duplikasi kode. Perangkat utamanya di sini adalah kelas HasQuotient, yang memungkinkan notasi seperti M ⧸ N. Perhatikan bahwa simbol hasil bagi ⧸ merupakan karakter Unicode khusus, bukan simbol pembagian ASCII biasa.

Sebagai contoh, kita akan membangun hasil bagi monoid komutatif oleh sebuah submonoid dan menyerahkan buktinya kepada Anda. Dalam contoh terakhir, Anda dapat menggunakan Setoid.refl, tetapi Lean tidak akan secara otomatis mengambil struktur Setoid yang relevan. Masalah ini dapat diperbaiki dengan memberikan semua argumen melalui sintaks @, seperti dalam @Setoid.refl M N.Setoid.

def Submonoid.Setoid [CommMonoid M] (N : Submonoid M) : Setoid M  where
  r := fun x y ↦ ∃ w ∈ N, ∃ z ∈ N, x*w = y*z
  iseqv := {
    refl := fun x ↦ ⟨1, N.one_mem, 1, N.one_mem, rfl⟩
    symm := fun ⟨w, hw, z, hz, h⟩ ↦ ⟨z, hz, w, hw, h.symm⟩
    trans := by
      sorry
  }

instance [CommMonoid M] : HasQuotient M (Submonoid M) where
  Quotient := fun N ↦ Quotient N.Setoid

def QuotientMonoid.mk [CommMonoid M] (N : Submonoid M) : M → M ⧸ N := Quotient.mk N.Setoid

instance [CommMonoid M] (N : Submonoid M) : Monoid (M ⧸ N) where
  mul := Quotient.map₂ (· * ·) (by
      sorry
        )
  mul_assoc := by
      sorry
  one := QuotientMonoid.mk N 1
  one_mul := by
      sorry
  mul_one := by
      sorry