10. Aljabar Linear

10.1. Ruang vektor dan pemetaan linear

10.1.1. Ruang vektor

Kita akan langsung memulai dengan aljabar linear abstrak dalam konteks ruang vektor atas sembarang medan. Namun, Anda dapat menemukan informasi tentang matriks dalam Bagian 10.4.1, yang secara logis tidak bergantung pada teori abstrak ini. Sebenarnya, Mathlib menangani versi aljabar linear yang lebih umum dan melibatkan istilah modul, tetapi untuk sementara kita akan berpura-pura bahwa hal itu hanyalah kebiasaan ejaan yang nyentrik.

Cara menyatakan “misalkan \(K\) suatu medan dan \(V\) ruang vektor atas \(K\)” (serta menjadikannya argumen implisit bagi hasil-hasil berikutnya) adalah:

variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]

Dalam Bab 8, kita telah menjelaskan mengapa diperlukan dua kelas tipe terpisah, [AddCommGroup V] [Module K V]. Secara ringkas, alasannya sebagai berikut. Secara matematis, kita ingin mengatakan bahwa adanya struktur ruang vektor atas \(K\) mengakibatkan adanya struktur grup aditif komutatif. Kita dapat memberi tahu Lean tentang hal ini. Akan tetapi, setiap kali Lean perlu menemukan struktur grup semacam itu pada tipe \(V\), Lean kemudian harus mencari struktur ruang vektor dengan medan \(K\) yang sama sekali tidak ditentukan dan tidak dapat disimpulkan dari \(V\). Hal itu akan sangat merugikan sistem sintesis kelas tipe.

Perkalian vektor v dengan skalar a dinotasikan sebagai a • v. Contoh berikut mencantumkan beberapa aturan aljabar mengenai interaksi operasi ini dengan penjumlahan. Tentu saja, simp atau apply? dapat menemukan bukti-bukti tersebut. Terdapat pula taktik module yang menyelesaikan sasaran yang mengikuti aksioma ruang vektor dan medan, sebagaimana taktik ring digunakan dalam gelanggang komutatif atau taktik group digunakan dalam grup. Namun, tetap berguna untuk mengingat bahwa perkalian skalar disingkat smul dalam nama lemma.

example (a : K) (u v : V) : a • (u + v) = a • u + a • v :=
  smul_add a u v

example (a b : K) (u : V) : (a + b) • u = a • u + b • u :=
  add_smul a b u

example (a b : K) (u : V) : a • b • u = b • a • u :=
  smul_comm a b u

Sebagai catatan singkat bagi pembaca yang lebih mahir, sesuai petunjuk terminologinya, aljabar linear Mathlib juga mencakup modul atas gelanggang (yang tidak harus komutatif). Bahkan, cakupannya meliputi semimodul atas semigelanggang. Jika Anda merasa tidak memerlukan tingkat keumuman ini, renungkan contoh berikut, yang dengan apik merangkum banyak aturan aljabar mengenai aksi ideal pada submodul:

example {R M : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M] :
    Module (Ideal R) (Submodule R M) :=
  inferInstance

Untuk menyatakan bahwa M merupakan modul atas gelanggang R, kita menulis:

section
variable {R : Type*} [Ring R] {M : Type*} [AddCommGroup M] [Module R M]
end

Jika dibandingkan dengan deklarasi ruang vektor, tampak dua perbedaan. Selain mengganti nama variabel, satu-satunya perubahan ialah mengganti hipotesis Field K dengan hipotesis Ring R.

Untuk menyatakan bahwa M merupakan semimodul atas semigelanggang R, kita mengganti hipotesis Ring R dengan hipotesis Semiring R dan juga mengganti AddCommGroup M dengan AddCommMonoid M. Perubahan ini mencerminkan fakta bahwa semimodul tidak memiliki negasi:

section
variable {R : Type*} [Semiring R] {M : Type*} [AddCommMonoid M] [Module R M]
end

Lean tidak dapat secara otomatis menyimpulkan bahwa M memiliki negasi jika R memilikinya, sebab secara apriori Lean tidak dapat menebak R yang tepat hanya dari M. Jadi, jika kita mendeklarasikan R sebagai gelanggang dan M sebagai modul atas R, kita harus mendeklarasikan M sebagai AddCommGroup atau menambahkan instans tersebut ke konteks secara manual:

example {R : Type*} [Ring R] {M : Type*} [AddCommMonoid M] [Module R M] : M → M :=
  -- Pastikan menggunakan `letI` (bukan `haveI` atau `let`) agar struktur aditif
  -- yang sudah ada dari hipotesis `AddCommMonoid M` lebih mudah diidentifikasi
  -- dengan struktur baru yang diperkenalkan pada baris berikutnya.
  letI : AddCommGroup M := Module.addCommMonoidToAddCommGroup R
  fun x => - x

10.1.2. Pemetaan linear

Selanjutnya, kita memerlukan pemetaan linear. Seperti morfisme grup, pemetaan linear dalam Mathlib merupakan pemetaan terbundel, yakni paket yang terdiri atas sebuah pemetaan dan bukti sifat-sifat linearitasnya. Pemetaan terbundel tersebut dikonversi menjadi fungsi biasa ketika diterapkan. Lihat Bab 8 untuk informasi lebih lanjut mengenai rancangan ini.

Tipe pemetaan linear di antara dua ruang vektor-K, V dan W, dinotasikan sebagai V →ₗ[K] W. Subskrip l berarti linear. Pada mulanya, pencantuman K dalam notasi ini mungkin terasa ganjil, tetapi hal itu sangat penting ketika beberapa medan terlibat. Sebagai contoh, semua pemetaan yang linear atas bilangan real dari \(ℂ\) ke \(ℂ\) berbentuk \(z ↦ az + b\bar{z}\), sedangkan hanya pemetaan berbentuk \(z ↦ az\) yang linear atas bilangan kompleks. Perbedaan ini sangat penting dalam analisis kompleks.

variable {W : Type*} [AddCommGroup W] [Module K W]

variable (φ : V →ₗ[K] W)

example (a : K) (v : V) : φ (a • v) = a • φ v :=
  map_smul φ a v

example (v w : V) : φ (v + w) = φ v + φ w :=
  map_add φ v w

Perhatikan bahwa V →ₗ[K] W sendiri memiliki struktur aljabar yang menarik (inilah salah satu alasan pemetaan tersebut dibundel). Tipe ini merupakan ruang vektor-K, sehingga kita dapat menjumlahkan pemetaan linear dan mengalikannya dengan skalar.

variable (ψ : V →ₗ[K] W)

#check (2 • φ + ψ : V →ₗ[K] W)

Salah satu kekurangan pemetaan terbundel ialah komposisi fungsi biasa tidak dapat digunakan. Kita perlu memakai LinearMap.comp atau notasi ∘ₗ.

variable (θ : W →ₗ[K] V)

#check (φ.comp θ : W →ₗ[K] W)
#check (φ ∘ₗ θ : W →ₗ[K] W)

Ada dua cara utama untuk membangun pemetaan linear. Pertama, kita dapat membangun strukturnya dengan memberikan fungsi beserta bukti linearitasnya. Seperti biasa, tindakan kode untuk struktur memudahkan hal ini: Anda dapat mengetik example : V →ₗ[K] V := _ lalu menggunakan tindakan kode “Generate a skeleton” (buat kerangka) yang terlampir pada garis bawah tersebut.

example : V →ₗ[K] V where
  toFun v := 3 • v
  map_add' _ _ := smul_add ..
  map_smul' _ _ := smul_comm ..

Anda mungkin bertanya-tanya mengapa nama komponen bukti pada LinearMap berakhiran tanda prima. Penyebabnya, komponen tersebut didefinisikan sebelum koersi ke fungsi didefinisikan, sehingga pernyataannya menggunakan LinearMap.toFun. Setelah itu, komponen tersebut dinyatakan ulang sebagai LinearMap.map_add dan LinearMap.map_smul dengan menggunakan koersi ke fungsi.

Namun, ceritanya belum berakhir. Kita juga menginginkan versi map_add yang berlaku bagi setiap pemetaan (terbundel) yang mempertahankan penjumlahan, seperti morfisme grup aditif, pemetaan linear, pemetaan linear kontinu, pemetaan aljabar-K, dan sebagainya. Versi tersebut adalah map_add (dalam namespace akar). Versi antara, LinearMap.map_add, agak redundan, tetapi memungkinkan penggunaan notasi titik, yang kadang-kadang nyaman. Kisah serupa berlaku bagi map_smul, dan kerangka umumnya dijelaskan dalam Bab 8.

#check (φ.map_add' : ∀ x y : V, φ.toFun (x + y) = φ.toFun x + φ.toFun y)
#check (φ.map_add : ∀ x y : V, φ (x + y) = φ x + φ y)
#check (map_add φ : ∀ x y : V, φ (x + y) = φ x + φ y)

Kita juga dapat membangun pemetaan linear dari pemetaan yang telah didefinisikan dalam Mathlib dengan menggunakan berbagai kombinator. Sebagai contoh, pemetaan pada contoh di atas telah dikenal sebagai LinearMap.lsmul K V 3. Ada beberapa alasan mengapa K dan V menjadi argumen eksplisit di sini. Alasan yang paling mendesak ialah bahwa dari LinearMap.lsmul 3 saja, Lean sama sekali tidak dapat menyimpulkan V, bahkan K. Selain itu, LinearMap.lsmul K V merupakan objek yang menarik dengan sendirinya: tipenya adalah K →ₗ[K] V →ₗ[K] V, yang berarti bahwa objek tersebut merupakan pemetaan linear-K dari K—dipandang sebagai ruang vektor atas dirinya sendiri—ke ruang pemetaan linear-K dari V ke V.

#check (LinearMap.lsmul K V 3 : V →ₗ[K] V)
#check (LinearMap.lsmul K V : K →ₗ[K] V →ₗ[K] V)

Terdapat pula tipe isomorfisme linear LinearEquiv, yang dinotasikan sebagai V ≃ₗ[K] W. Invers dari f : V ≃ₗ[K] W adalah f.symm : W ≃ₗ[K] V; komposisi f dan g adalah f.trans g, yang juga dinotasikan sebagai f ≪≫ₗ g; dan isomorfisme identitas pada V adalah LinearEquiv.refl K V. Elemen tipe ini secara otomatis dikoersikan menjadi morfisme dan fungsi ketika diperlukan.

example (f : V ≃ₗ[K] W) : f ≪≫ₗ f.symm = LinearEquiv.refl K V :=
  f.self_trans_symm

LinearEquiv.ofBijective dapat digunakan untuk membangun isomorfisme dari morfisme bijektif. Dengan cara ini, fungsi inversnya menjadi tidak dapat dihitung.

noncomputable example (f : V →ₗ[K] W) (h : Function.Bijective f) : V ≃ₗ[K] W :=
  .ofBijective f h

Perhatikan bahwa dalam contoh di atas, Lean menggunakan tipe yang telah dinyatakan untuk memahami bahwa .ofBijective merujuk pada LinearEquiv.ofBijective (tanpa perlu membuka namespace apa pun).

10.1.3. Jumlah dan produk ruang vektor

Kita dapat membangun ruang vektor baru dari ruang yang telah ada dengan menggunakan jumlah langsung dan produk langsung. Mari kita mulai dengan dua ruang vektor. Dalam kasus ini, tidak ada perbedaan antara jumlah dan produk, sehingga kita cukup menggunakan tipe produk. Cuplikan kode berikut menunjukkan cara memperoleh semua pemetaan struktur (inklusi dan proyeksi) sebagai pemetaan linear, serta sifat universal yang membangun pemetaan linear menuju produk dan keluar dari jumlah. (Jika Anda belum mengenal perbedaan antara jumlah dan produk dari sudut pandang teori kategori, abaikan saja istilah sifat universal dan perhatikan tipe contoh-contoh berikut.)

section binary_product

variable {W : Type*} [AddCommGroup W] [Module K W]
variable {U : Type*} [AddCommGroup U] [Module K U]
variable {T : Type*} [AddCommGroup T] [Module K T]

  -- Pemetaan proyeksi pertama
example : V × W →ₗ[K] V := LinearMap.fst K V W

  -- Pemetaan proyeksi kedua
example : V × W →ₗ[K] W := LinearMap.snd K V W

  -- Sifat universal produk
example (φ : U →ₗ[K] V) (ψ : U →ₗ[K] W) : U →ₗ[K]  V × W := LinearMap.prod φ ψ

  -- Pemetaan produk bekerja sebagaimana diharapkan pada komponen pertama
example (φ : U →ₗ[K] V) (ψ : U →ₗ[K] W) : LinearMap.fst K V W ∘ₗ LinearMap.prod φ ψ = φ := rfl

  -- Pemetaan produk bekerja sebagaimana diharapkan pada komponen kedua
example (φ : U →ₗ[K] V) (ψ : U →ₗ[K] W) : LinearMap.snd K V W ∘ₗ LinearMap.prod φ ψ = ψ := rfl

  -- Kita juga dapat menggabungkan pemetaan secara paralel
example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] T) : (V × W) →ₗ[K] (U × T) := φ.prodMap ψ

  -- Hal ini cukup dilakukan dengan menggabungkan proyeksi dan sifat universal
example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] T) :
  φ.prodMap ψ = (φ ∘ₗ .fst K V W).prod (ψ ∘ₗ .snd K V W) := rfl

  -- Pemetaan inklusi pertama
example : V →ₗ[K] V × W := LinearMap.inl K V W

  -- Pemetaan inklusi kedua
example : W →ₗ[K] V × W := LinearMap.inr K V W

  -- Sifat universal jumlah (alias koproduk)
example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] U) : V × W →ₗ[K] U := φ.coprod ψ

  -- Pemetaan koproduk bekerja sebagaimana diharapkan pada komponen pertama
example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] U) : φ.coprod ψ ∘ₗ LinearMap.inl K V W = φ :=
  LinearMap.coprod_inl φ ψ

  -- Pemetaan koproduk bekerja sebagaimana diharapkan pada komponen kedua
example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] U) : φ.coprod ψ ∘ₗ LinearMap.inr K V W = ψ :=
  LinearMap.coprod_inr φ ψ

  -- Pemetaan koproduk didefinisikan sebagaimana yang diharapkan
example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] U) (v : V) (w : W) :
    φ.coprod ψ (v, w) = φ v + ψ w :=
  rfl

end binary_product

Sekarang mari kita beralih ke jumlah dan produk dari sembarang keluarga ruang vektor. Kita akan melihat cara mendefinisikan keluarga ruang vektor dan mengakses sifat universal jumlah serta produk. Perhatikan bahwa notasi jumlah langsung berada dalam lingkup namespace DirectSum dan bahwa sifat universal jumlah langsung memerlukan kesamaan yang dapat diputuskan pada tipe indeks (ini sekadar kekhasan implementasi).

section families
open DirectSum

variable {ι : Type*} [DecidableEq ι]
         (V : ι → Type*) [∀ i, AddCommGroup (V i)] [∀ i, Module K (V i)]

-- Sifat universal jumlah langsung merakit pemetaan dari suku-sukunya untuk
-- membangun pemetaan dari jumlah langsung
example (φ : Π i, (V i →ₗ[K] W)) : (⨁ i, V i) →ₗ[K] W :=
  DirectSum.toModule K ι W φ

-- Sifat universal produk langsung merakit pemetaan menuju faktor-faktornya untuk
-- membangun pemetaan menuju produk langsung
example (φ : Π i, (W →ₗ[K] V i)) : W →ₗ[K] (Π i, V i) :=
  LinearMap.pi φ

-- Pemetaan proyeksi dari produk
example (i : ι) : (Π j, V j) →ₗ[K] V i := LinearMap.proj i

-- Pemetaan inklusi menuju jumlah
example (i : ι) : V i →ₗ[K] (⨁ i, V i) := DirectSum.lof K ι V i

-- Pemetaan inklusi menuju produk
example (i : ι) : V i →ₗ[K] (Π i, V i) := LinearMap.single K V i

-- Jika `ι` merupakan tipe hingga, terdapat isomorfisme antara jumlah dan produk.
example [Fintype ι] : (⨁ i, V i) ≃ₗ[K] (Π i, V i) :=
  linearEquivFunOnFintype K ι V

end families

10.2. Subruang dan ruang hasil bagi

10.2.1. Subruang

Seperti pemetaan linear yang dibundel, subruang linear dari V juga merupakan struktur terbundel. Struktur ini terdiri atas sebuah himpunan bagian dari V, yang disebut himpunan pembawa subruang, beserta sifat-sifat ketertutupan yang relevan. Sekali lagi, istilah modul muncul alih-alih ruang vektor karena Mathlib sebenarnya menggunakan konteks yang lebih umum bagi aljabar linear.

section
variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]

example (U : Submodule K V) {x y : V} (hx : x ∈ U) (hy : y ∈ U) :
    x + y ∈ U :=
  U.add_mem hx hy

example (U : Submodule K V) {x : V} (hx : x ∈ U) (a : K) :
    a • x ∈ U :=
  U.smul_mem a hx
end

Dalam contoh di atas, penting untuk memahami bahwa Submodule K V merupakan tipe subruang linear-K dari V, bukan predikat IsSubmodule U dengan U sebagai elemen Set V. Submodule K V dilengkapi koersi ke Set V dan predikat keanggotaan pada V. Lihat Bab 8.3 untuk penjelasan mengenai bagaimana dan mengapa hal ini dilakukan.

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

Sebagai contoh, untuk menyatakan dan membuktikan bahwa ℝ merupakan subruang linear-ℝ dari ℂ, yang sebenarnya ingin kita lakukan ialah membangun term bertipe Submodule ℝ ℂ yang proyeksinya ke Set ℂ adalah ℝ, atau lebih tepatnya, citra ℝ dalam ℂ.

noncomputable example : Submodule ℝ ℂ where
  carrier := Set.range ((↑) : ℝ → ℂ)
  add_mem' := by
    rintro _ _ ⟨n, rfl⟩ ⟨m, rfl⟩
    use n + m
    simp
  zero_mem' := by
    use 0
    simp
  smul_mem' := by
    rintro c - ⟨a, rfl⟩
    use c*a
    simp

Tanda prima di akhir komponen bukti dalam Submodule serupa dengan tanda prima dalam LinearMap. Komponen tersebut dinyatakan menggunakan komponen carrier karena didefinisikan sebelum instans Membership. Setelah itu, perannya digantikan oleh Submodule.add_mem, Submodule.zero_mem, dan Submodule.smul_mem yang telah kita lihat di atas.

Sebagai latihan memanipulasi subruang dan pemetaan linear, Anda akan mendefinisikan prapeta suatu subruang oleh pemetaan linear. (Tentu saja, nanti kita akan melihat bahwa hal ini sudah tersedia di Mathlib.) Ingat bahwa Set.mem_preimage dapat digunakan untuk menulis ulang pernyataan yang melibatkan keanggotaan dan prapeta. Inilah satu-satunya lemma tambahan yang diperlukan selain lemma mengenai LinearMap dan Submodule yang telah dibahas di atas.

variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]

def preimage {W : Type*} [AddCommGroup W] [Module K W] (φ : V →ₗ[K] W) (H : Submodule K W) :
    Submodule K V where
  carrier := φ ⁻¹' H
  zero_mem' := by
    sorry
  add_mem' := by
    sorry
  smul_mem' := by
    sorry

Melalui kelas tipe, Mathlib mengetahui bahwa subruang dari ruang vektor mewarisi struktur ruang vektor.

example (U : Submodule K V) : Module K U := inferInstance

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

example (U : Submodule K V) : Module K {x : V // x ∈ U} := inferInstance

10.2.2. Struktur kekisi lengkap dan jumlah langsung internal

Manfaat penting dari tipe Submodule K V alih-alih predikat IsSubmodule : Set V → Prop ialah bahwa Submodule K V dapat dengan mudah dilengkapi struktur tambahan. Secara khusus, tipe ini memiliki struktur kekisi lengkap terhadap inklusi. Sebagai contoh, alih-alih memakai lemma yang menyatakan bahwa irisan dua subruang dari V kembali merupakan subruang, kita menggunakan operasi kekisi ⊓ untuk membangun irisannya. Setelah itu, sembarang lemma mengenai kekisi dapat diterapkan pada konstruksi tersebut.

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

example (H H' : Submodule K V) :
    ((H ⊓ H' : Submodule K V) : Set V) = (H : Set V) ∩ (H' : Set V) := rfl

Penggunaan notasi yang berbeda bagi sesuatu yang pada dasarnya merupakan irisan himpunan pembawanya mungkin tampak ganjil. Namun, korespondensi tersebut tidak berlaku bagi operasi supremum dan gabungan himpunan karena, secara umum, gabungan subruang bukanlah subruang. Sebagai gantinya, kita perlu memakai subruang yang direntang oleh gabungan tersebut melalui Submodule.span.

example (H H' : Submodule K V) :
    ((H ⊔ H' : Submodule K V) : Set V) = Submodule.span K ((H : Set V) ∪ (H' : Set V)) := by
  simp [Submodule.span_union]

Seluk-beluk lainnya ialah bahwa V sendiri tidak bertipe Submodule K V. Karena itu, kita memerlukan cara untuk membicarakan V yang dipandang sebagai subruang dari V. Hal ini juga disediakan oleh struktur kekisi: subruang penuh merupakan elemen teratas kekisi tersebut.

example (x : V) : x ∈ (⊤ : Submodule K V) := trivial

Serupa dengan itu, elemen terbawah kekisi ini adalah subruang yang satu-satunya elemennya ialah elemen nol.

example (x : V) : x ∈ (⊥ : Submodule K V) ↔ x = 0 := Submodule.mem_bot K

Secara khusus, kita dapat membahas subruang-subruang yang membentuk jumlah langsung (internal). Untuk dua subruang, kita menggunakan predikat serbaguna IsCompl, yang bermakna bagi setiap tipe dengan tatanan parsial berbatas. Untuk keluarga subruang umum, kita menggunakan DirectSum.IsInternal.

-- Jika dua subruang berada dalam jumlah langsung, keduanya merentang seluruh ruang.
example (U V : Submodule K V) (h : IsCompl U V) :
  U ⊔ V = ⊤ := h.sup_eq_top

-- Jika dua subruang berada dalam jumlah langsung, irisannya hanya memuat nol.
example (U V : Submodule K V) (h : IsCompl U V) :
  U ⊓ V = ⊥ := h.inf_eq_bot

section
open DirectSum
variable {ι : Type*} [DecidableEq ι]

-- Jika subruang-subruang berada dalam jumlah langsung, semuanya merentang seluruh ruang.
example (U : ι → Submodule K V) (h : DirectSum.IsInternal U) :
  ⨆ i, U i = ⊤ := h.submodule_iSup_eq_top

-- Jika subruang-subruang berada dalam jumlah langsung, irisan berpasangannya hanya memuat nol.
example {ι : Type*} [DecidableEq ι] (U : ι → Submodule K V) (h : DirectSum.IsInternal U)
    {i j : ι} (hij : i ≠ j) : U i ⊓ U j = ⊥ :=
  (h.submodule_iSupIndep.pairwiseDisjoint hij).eq_bot

-- Syarat-syarat tersebut mencirikan jumlah langsung.
#check DirectSum.isInternal_submodule_iff_iSupIndep_and_iSup_eq_top

-- Hubungannya dengan jumlah langsung eksternal: jika suatu keluarga subruang berada
-- dalam jumlah langsung internal, pemetaan dari jumlah langsung eksternalnya ke `V`
-- merupakan isomorfisme linear.
noncomputable example {ι : Type*} [DecidableEq ι] (U : ι → Submodule K V)
    (h : DirectSum.IsInternal U) : (⨁ i, U i) ≃ₗ[K] V :=
  LinearEquiv.ofBijective (coeLinearMap U) h
end

10.2.3. Subruang yang direntang oleh himpunan

Selain membangun subruang dari subruang yang telah ada, kita dapat membangunnya dari sembarang himpunan s menggunakan Submodule.span K s, yang menghasilkan subruang terkecil yang memuat s. Di atas kertas, lazim digunakan fakta bahwa ruang ini terdiri atas semua kombinasi linear elemen s. Namun, sering kali lebih efisien menggunakan sifat universalnya yang dinyatakan oleh Submodule.span_le beserta seluruh teori koneksi Galois.

example {s : Set V} (E : Submodule K V) : Submodule.span K s ≤ E ↔ s ⊆ E :=
  Submodule.span_le

example : GaloisInsertion (Submodule.span K) ((↑) : Submodule K V → Set V) :=
  Submodule.gi K V

Jika semua itu belum cukup, kita dapat menggunakan prinsip induksi yang relevan, Submodule.span_induction. Prinsip ini memastikan bahwa suatu sifat berlaku bagi setiap elemen rentangan s, asalkan sifat tersebut berlaku pada zero dan elemen-elemen s serta stabil terhadap penjumlahan dan perkalian skalar.

Sebagai latihan, mari kita buktikan kembali salah satu arah implikasi Submodule.mem_sup. Ingat bahwa taktik module dapat digunakan untuk menutup sasaran yang mengikuti aksioma yang menghubungkan berbagai operasi aljabar pada V.

example {S T : Submodule K V} {x : V} (h : x ∈ S ⊔ T) :
    ∃ s ∈ S, ∃ t ∈ T, x = s + t  := by
  rw [← S.span_eq, ← T.span_eq, ← Submodule.span_union] at h
  induction h using Submodule.span_induction with
  | mem y h =>
      sorry
  | zero =>
      sorry
  | add x y hx hy hx' hy' =>
      sorry
  | smul a x hx hx' =>
      sorry

10.2.4. Mengambil citra dan prapeta subruang

Seperti yang dijanjikan sebelumnya, sekarang kita menjelaskan cara mengambil citra dan prapeta subruang melalui pemetaan linear. Seperti biasa dalam Mathlib, operasi pertama disebut map dan operasi kedua disebut comap.

section

variable {W : Type*} [AddCommGroup W] [Module K W] (φ : V →ₗ[K] W)

variable (E : Submodule K V) in
#check (Submodule.map φ E : Submodule K W)

variable (F : Submodule K W) in
#check (Submodule.comap φ F : Submodule K V)

Perhatikan bahwa keduanya berada dalam namespace Submodule, sehingga notasi titik dapat digunakan untuk menulis E.map φ alih-alih Submodule.map φ E. Namun, bentuk ini cukup janggal untuk dibaca (meski sebagian kontributor Mathlib menggunakannya).

Secara khusus, citra dan kernel pemetaan linear merupakan subruang. Kasus khusus tersebut cukup penting sehingga memiliki deklarasi tersendiri.

example : LinearMap.range φ = .map φ ⊤ := LinearMap.range_eq_map φ

example : LinearMap.ker φ = .comap φ ⊥ := Submodule.comap_bot φ -- atau `rfl`

Perhatikan bahwa φ.ker tidak dapat ditulis sebagai pengganti LinearMap.ker φ. Penyebabnya, LinearMap.ker juga berlaku bagi kelas pemetaan yang mempertahankan lebih banyak struktur, sehingga tidak mengharapkan argumen yang tipenya diawali LinearMap. Oleh sebab itu, notasi titik tidak bekerja di sini. Namun, kita dapat menggunakan bentuk notasi titik yang lain pada ruas kanan. Setelah mengelaborasi ruas kiri, Lean mengharapkan term bertipe Submodule K V, sehingga .comap ditafsirkan sebagai Submodule.comap.

Lemma-lemma berikut memberikan hubungan utama antara subruang-subruang tersebut dan sifat-sifat φ.

open Function LinearMap

example : Injective φ ↔ ker φ = ⊥ := ker_eq_bot.symm

example : Surjective φ ↔ range φ = ⊤ := range_eq_top.symm

Sebagai latihan, mari kita buktikan sifat koneksi Galois bagi map dan comap. Lemma-lemma berikut dapat digunakan, tetapi tidak diperlukan karena berlaku menurut definisi.

#check Submodule.mem_map_of_mem
#check Submodule.mem_map
#check Submodule.mem_comap

example (E : Submodule K V) (F : Submodule K W) :
    Submodule.map φ E ≤ F ↔ E ≤ Submodule.comap φ F := by
  sorry

10.2.5. Ruang hasil bagi

Ruang vektor hasil bagi menggunakan notasi hasil bagi umum (diketik dengan \quot, bukan / biasa). Proyeksi ke ruang hasil bagi adalah Submodule.mkQ, sedangkan sifat universalnya adalah Submodule.liftQ.

variable (E : Submodule K V)

example : Module K (V ⧸ E) := inferInstance

example : V →ₗ[K] V ⧸ E := E.mkQ

example : ker E.mkQ = E := E.ker_mkQ

example : range E.mkQ = ⊤ := E.range_mkQ

example (hφ : E ≤ ker φ) : V ⧸ E →ₗ[K] W := E.liftQ φ hφ

example (F : Submodule K W) (hφ : E ≤ .comap φ F) : V ⧸ E →ₗ[K] W ⧸ F := E.mapQ F φ hφ

noncomputable example : (V ⧸ LinearMap.ker φ) ≃ₗ[K] range φ := φ.quotKerEquivRange

Sebagai latihan, mari kita buktikan teorema korespondensi bagi subruang dari ruang hasil bagi. Mathlib mengenal versi yang sedikit lebih presisi sebagai Submodule.comapMkQRelIso.

open Submodule

#check Submodule.map_comap_eq
#check Submodule.comap_map_eq

example : Submodule K (V ⧸ E) ≃ { F : Submodule K V // E ≤ F } where
  toFun := sorry
  invFun := sorry
  left_inv := sorry
  right_inv := sorry

10.3. Endomorfisme

Kasus khusus penting dari pemetaan linear ialah endomorfisme: pemetaan linear dari ruang vektor ke dirinya sendiri. Endomorfisme menarik karena membentuk aljabar-K. Secara khusus, kita dapat mengevaluasi polinomial berkoefisien dalam K pada endomorfisme, dan endomorfisme dapat memiliki nilai eigen serta vektor eigen.

Mathlib menggunakan singkatan Module.End K V := V →ₗ[K] V, yang praktis ketika kita banyak menggunakannya (terutama setelah membuka namespace Module).

variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]

variable {W : Type*} [AddCommGroup W] [Module K W]


open Polynomial Module LinearMap End

example (φ ψ : End K V) : φ * ψ = φ ∘ₗ ψ :=
  End.mul_eq_comp φ ψ -- `rfl` juga dapat digunakan

-- mengevaluasi `P` pada `φ`
example (P : K[X]) (φ : End K V) : V →ₗ[K] V :=
  aeval φ P

-- mengevaluasi `X` pada `φ` menghasilkan kembali `φ`
example (φ : End K V) : aeval φ (X : K[X]) = φ :=
  aeval_X φ

Sebagai latihan memanipulasi endomorfisme, subruang, dan polinomial, mari kita buktikan lemma kernel (biner): untuk setiap endomorfisme \(φ\) dan setiap pasangan polinomial relatif prima \(P\) dan \(Q\), berlaku \(\ker P(φ) ⊕ \ker Q(φ) = \ker \big(PQ(φ)\big)\).

Perhatikan bahwa IsCoprime x y didefinisikan sebagai ∃ a b, a * x + b * y = 1.

#check Submodule.eq_bot_iff
#check Submodule.mem_inf
#check LinearMap.mem_ker

example (P Q : K[X]) (h : IsCoprime P Q) (φ : End K V) : ker (aeval φ P) ⊓ ker (aeval φ Q) = ⊥ := by
  sorry

#check Submodule.add_mem_sup
#check map_mul
#check End.mul_apply
#check LinearMap.ker_le_ker_comp

example (P Q : K[X]) (h : IsCoprime P Q) (φ : End K V) :
    ker (aeval φ P) ⊔ ker (aeval φ Q) = ker (aeval φ (P*Q)) := by
  sorry

Sekarang kita beralih ke pembahasan ruang eigen dan nilai eigen. Ruang eigen yang berkaitan dengan endomorfisme \(φ\) dan skalar \(a\) adalah kernel dari \(φ - aId\). Ruang eigen didefinisikan bagi semua nilai a, meskipun ruang tersebut hanya menarik ketika tidak nol. Namun, menurut definisi, vektor eigen merupakan elemen tak nol dari ruang eigen. Predikat yang bersesuaian adalah End.HasEigenvector.

example (φ : End K V) (a : K) : φ.eigenspace a = LinearMap.ker (φ - a • 1) :=
  End.eigenspace_def

Selanjutnya, terdapat predikat End.HasEigenvalue dan subtipe yang bersesuaian, End.Eigenvalues.

example (φ : End K V) (a : K) : φ.HasEigenvalue a ↔ φ.eigenspace a ≠ ⊥ :=
  Iff.rfl

example (φ : End K V) (a : K) : φ.HasEigenvalue a ↔ ∃ v, φ.HasEigenvector a v  :=
  ⟨End.HasEigenvalue.exists_hasEigenvector, fun ⟨_, hv⟩ ↦ φ.hasEigenvalue_of_hasEigenvector hv⟩

example (φ : End K V) : φ.Eigenvalues = {a // φ.HasEigenvalue a} :=
  rfl

-- Nilai eigen merupakan akar polinomial minimal
example (φ : End K V) (a : K) : φ.HasEigenvalue a → (minpoly K φ).IsRoot a :=
  φ.isRoot_of_hasEigenvalue

-- Dalam dimensi hingga, konversnya juga berlaku (dimensi akan dibahas di bawah)
example [FiniteDimensional K V] (φ : End K V) (a : K) :
    φ.HasEigenvalue a ↔ (minpoly K φ).IsRoot a :=
  φ.hasEigenvalue_iff_isRoot

-- Cayley–Hamilton
example [FiniteDimensional K V] (φ : End K V) : aeval φ φ.charpoly = 0 :=
  φ.aeval_self_charpoly

10.4. Matriks, basis, dan dimensi

10.4.1. Matriks

Sebelum memperkenalkan basis bagi ruang vektor abstrak, kita kembali ke konteks aljabar linear yang jauh lebih elementer dalam \(K^n\) untuk suatu medan \(K\). Objek utamanya adalah vektor dan matriks. Bagi vektor konkret, kita dapat menggunakan notasi ![…], dengan komponen yang dipisahkan oleh koma. Bagi matriks konkret, kita dapat menggunakan notasi !![…]; baris dipisahkan oleh titik koma, sedangkan elemen dalam setiap baris dipisahkan oleh koma. Jika entri-entri memiliki tipe yang dapat dihitung, seperti ℕ atau ℚ, kita dapat menggunakan perintah #eval untuk bereksperimen dengan operasi dasar.

section matrices

-- Menjumlahkan vektor
#eval ![1, 2] + ![3, 4]  -- ![4, 6]

-- Menjumlahkan matriks
#eval !![1, 2; 3, 4] + !![3, 4; 5, 6]  -- !![4, 6; 8, 10]

-- Mengalikan matriks
#eval !![1, 2; 3, 4] * !![3, 4; 5, 6]  -- !![13, 16; 29, 36]

Penting untuk dipahami bahwa penggunaan #eval ini hanya berguna bagi eksplorasi; tujuannya bukan menggantikan sistem aljabar komputer seperti Sage. Representasi data matriks yang digunakan di sini sama sekali tidak efisien secara komputasional. Representasi tersebut menggunakan fungsi alih-alih larik dan dioptimalkan untuk pembuktian, bukan perhitungan. Mesin virtual yang digunakan oleh #eval juga tidak dioptimalkan untuk keperluan ini.

Perhatikan bahwa notasi matriks mencantumkan baris-barisnya, sedangkan notasi vektor tidak menyatakan vektor baris maupun vektor kolom. Perkalian vektor dengan matriks dari sebelah kiri (atau kanan) menafsirkan vektor tersebut sebagai vektor baris (atau kolom). Hal ini bersesuaian dengan operasi Matrix.vecMul bernotasi ᵥ* dan Matrix.mulVec bernotasi *ᵥ. Kedua notasi tersebut berada dalam lingkup namespace Matrix, sehingga namespace itu perlu kita buka.

open Matrix

-- matriks yang beraksi pada vektor dari sebelah kiri
#eval !![1, 2; 3, 4] *ᵥ ![1, 1] -- ![3, 7]

-- aksi matriks pada vektor dari kiri menghasilkan vektor berukuran satu
#eval !![1, 2] *ᵥ ![1, 1]  -- ![3]

-- matriks yang beraksi pada vektor dari sebelah kanan
#eval  ![1, 1, 1] ᵥ* !![1, 2; 3, 4; 5, 6] -- ![9, 12]

Untuk menghasilkan matriks dengan baris-baris atau kolom-kolom identik yang ditentukan oleh sebuah vektor, kita menggunakan Matrix.replicateRow dan Matrix.replicateCol. Argumennya adalah tipe yang mengindeks baris atau kolom serta vektornya. Sebagai contoh, kita dapat memperoleh matriks satu baris atau satu kolom (lebih tepatnya, matriks yang baris atau kolomnya diindeks oleh Fin 1).

#eval replicateRow (Fin 1) ![1, 2] -- !![1, 2]

#eval replicateCol (Fin 1) ![1, 2] -- !![1; 2]

Operasi lain yang tidak asing mencakup hasil kali titik vektor, transpos matriks, serta—bagi matriks persegi—determinan dan jejak.

-- hasil kali titik vektor
#eval ![1, 2] ⬝ᵥ ![3, 4] -- `11`

-- transpos matriks
#eval !![1, 2; 3, 4]ᵀ -- `!![1, 3; 2, 4]`

-- determinan
#eval !![(1 : ℤ), 2; 3, 4].det -- `-2`

-- jejak
#eval !![(1 : ℤ), 2; 3, 4].trace -- `5`

Jika entri-entri tidak memiliki tipe yang dapat dihitung, misalnya berupa bilangan real, kita tidak dapat mengharapkan bantuan dari #eval. Evaluasi semacam ini juga tidak dapat digunakan dalam pembuktian tanpa memperluas basis kode tepercaya secara substansial (yakni bagian Lean yang perlu Anda percayai ketika memeriksa bukti).

Karena itu, sebaiknya gunakan pula taktik simp dan norm_num dalam pembuktian, atau padanan perintahnya untuk eksplorasi cepat.

#simp !![(1 : ℝ), 2; 3, 4].det -- `4 - 2*3`

#norm_num !![(1 : ℝ), 2; 3, 4].det -- `-2`

#norm_num !![(1 : ℝ), 2; 3, 4].trace -- `5`

variable (a b c d : ℝ) in
#simp !![a, b; c, d].det -- `a * d - b * c`

Operasi penting berikutnya pada matriks persegi ialah inversi. Sama seperti pembagian bilangan yang selalu didefinisikan dan menghasilkan nilai artifisial nol bagi pembagian dengan nol, operasi inversi didefinisikan pada semua matriks dan menghasilkan matriks nol bagi matriks yang tidak dapat dibalik.

Lebih tepatnya, terdapat fungsi umum Ring.inverse yang melakukan hal ini dalam sembarang gelanggang. Bagi setiap matriks A, A⁻¹ didefinisikan sebagai Ring.inverse A.det • A.adjugate. Menurut aturan Cramer, nilai tersebut memang merupakan invers A apabila determinan A tidak nol.

#norm_num [Matrix.inv_def] !![(1 : ℝ), 2; 3, 4]⁻¹ -- !![-2, 1; 3 / 2, -(1 / 2)]

Tentu saja, definisi ini benar-benar berguna hanya bagi matriks yang dapat dibalik. Terdapat kelas tipe umum Invertible yang membantu mencatat sifat tersebut. Sebagai contoh, pemanggilan simp dalam contoh berikut akan menggunakan lemma inv_mul_of_invertible, yang memiliki asumsi kelas tipe Invertible. Karena itu, lemma tersebut hanya terpicu apabila asumsi ini dapat ditemukan oleh sistem sintesis kelas tipe. Di sini, kita menyediakan fakta tersebut melalui pernyataan have.

example : !![(1 : ℝ), 2; 3, 4]⁻¹ * !![(1 : ℝ), 2; 3, 4] = 1 := by
  have : Invertible !![(1 : ℝ), 2; 3, 4] := by
    apply Matrix.invertibleOfIsUnitDet
    norm_num
  simp

Dalam kasus yang sepenuhnya konkret ini, kita juga dapat menggunakan mekanisme norm_num dan apply? untuk menemukan baris terakhir:

example : !![(1 : ℝ), 2; 3, 4]⁻¹ * !![(1 : ℝ), 2; 3, 4] = 1 := by
  norm_num [Matrix.inv_def]
  exact one_fin_two.symm

Semua matriks konkret di atas memiliki baris dan kolom yang diindeks oleh Fin n untuk suatu n (yang tidak harus sama bagi baris dan kolom). Namun, kadang-kadang lebih nyaman mengindeks matriks dengan sembarang tipe hingga. Sebagai contoh, baris dan kolom matriks ketetanggaan suatu graf hingga secara alami diindeks oleh simpul graf tersebut.

Sebenarnya, ketika kita sekadar ingin mendefinisikan matriks tanpa mendefinisikan operasi apa pun padanya, tipe indeksnya bahkan tidak perlu hingga dan koefisiennya dapat bertipe apa saja tanpa struktur aljabar. Karena itu, Mathlib cukup mendefinisikan Matrix m n α sebagai m → n → α bagi sembarang tipe m, n, dan α. Matriks yang telah kita gunakan sejauh ini memiliki tipe seperti Matrix (Fin 2) (Fin 2) ℝ. Tentu saja, operasi aljabar memerlukan lebih banyak asumsi atas m, n, dan α.

Perhatikan bahwa alasan utama kita tidak langsung menggunakan m → n → α ialah agar sistem kelas tipe dapat memahami apa yang kita inginkan. Sebagai contoh, bagi gelanggang R, tipe n → R dilengkapi operasi perkalian titik demi titik. Demikian pula, m → n → R memiliki operasi tersebut, yang bukan perkalian yang kita inginkan pada matriks.

Dalam contoh pertama di bawah, kita memaksa Lean menembus definisi Matrix dan menerima bahwa pernyataannya bermakna, lalu membuktikannya dengan memeriksa semua entri.

Namun, dua contoh berikutnya memperlihatkan bahwa Lean menggunakan perkalian titik demi titik pada Fin 2 → Fin 2 → ℤ, tetapi perkalian matriks pada Matrix (Fin 2) (Fin 2) ℤ.

section

example : (fun _ ↦ 1 : Fin 2 → Fin 2 → ℤ) = !![1, 1; 1, 1] := by
  ext i j
  fin_cases i <;> fin_cases j <;> rfl

example : (fun _ ↦ 1 : Fin 2 → Fin 2 → ℤ) * (fun _ ↦ 1 : Fin 2 → Fin 2 → ℤ) = !![1, 1; 1, 1] := by
  ext i j
  fin_cases i <;> fin_cases j <;> rfl

example : !![1, 1; 1, 1] * !![1, 1; 1, 1] = !![2, 2; 2, 2] := by
  norm_num

Untuk mendefinisikan matriks sebagai fungsi tanpa kehilangan manfaat Matrix bagi sintesis kelas tipe, kita dapat menggunakan ekuivalensi Matrix.of antara fungsi dan matriks. Diam-diam, ekuivalensi ini didefinisikan menggunakan Equiv.refl.

Sebagai contoh, kita dapat mendefinisikan matriks Vandermonde yang bersesuaian dengan vektor v.

example {n : ℕ} (v : Fin n → ℝ) :
    Matrix.vandermonde v = Matrix.of (fun i j : Fin n ↦ v i ^ (j : ℕ)) :=
  rfl
end
end matrices

10.4.2. Basis

Sekarang kita ingin membahas basis ruang vektor. Secara informal, ada banyak cara untuk mendefinisikan gagasan ini. Kita dapat menggunakan sifat universal. Kita dapat mengatakan bahwa basis merupakan keluarga vektor yang bebas linear dan merentang. Kita juga dapat menggabungkan kedua sifat itu dan langsung mengatakan bahwa basis adalah keluarga vektor sedemikian sehingga setiap vektor dapat ditulis secara unik sebagai kombinasi linear vektor-vektor basis. Cara lainnya ialah mengatakan bahwa basis memberikan isomorfisme linear dengan suatu pangkat dari medan dasar K, yang dipandang sebagai ruang vektor atas K.

Versi isomorfisme inilah yang sebenarnya digunakan Mathlib sebagai definisi di balik layar; karakterisasi lainnya dibuktikan darinya. Kita perlu sedikit berhati-hati dengan gagasan “pangkat dari K” dalam kasus basis tak hingga. Dalam konteks aljabar ini, hanya kombinasi linear hingga yang bermakna. Karena itu, ruang vektor acuan yang kita perlukan bukan produk langsung salinan K, melainkan jumlah langsung. Kita dapat menggunakan ⨁ i : ι, K bagi suatu tipe ι yang mengindeks basis, tetapi sebagai gantinya kita memakai penulisan yang lebih khusus, ι →₀ K. Notasi ini berarti “fungsi dari ι ke K dengan dukungan hingga”, yakni fungsi yang bernilai nol di luar suatu himpunan bagian hingga dari ι (himpunan ini tidak tetap, tetapi bergantung pada fungsinya). Mengevaluasi fungsi semacam itu yang berasal dari basis B pada vektor v dan i : ι menghasilkan komponen (atau koordinat) v pada vektor basis ke-i.

Tipe basis ruang vektor-K V yang diindeks oleh tipe ι adalah Basis ι K V. Isomorfismenya disebut Basis.repr.

variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]

section

open Module

variable {ι : Type*} (B : Basis ι K V) (v : V) (i : ι)

-- Vektor basis dengan indeks ``i``
#check (B i : V)

-- Isomorfisme linear dengan ruang model yang diberikan oleh ``B``
#check (B.repr : V ≃ₗ[K] ι →₀ K)

-- Fungsi komponen dari ``v``
#check (B.repr v : ι →₀ K)

-- Komponen dari ``v`` dengan indeks ``i``
#check (B.repr v i : K)

Alih-alih memulai dengan isomorfisme semacam itu, kita dapat memulai dengan keluarga vektor b yang bebas linear dan merentang. Konstruksi ini adalah Basis.mk.

Asumsi bahwa keluarga tersebut merentang ditulis sebagai ⊤ ≤ Submodule.span K (Set.range b). Di sini, ⊤ adalah submodul teratas dari V, yakni V yang dipandang sebagai submodul dari dirinya sendiri. Penulisan ini tampak agak berbelit, tetapi di bawah kita akan melihat bahwa bentuk tersebut hampir ekuivalen menurut definisi dengan bentuk yang lebih mudah dibaca, ∀ v, v ∈ Submodule.span K (Set.range b). Garis-garis bawah dalam cuplikan berikut merujuk pada informasi v ∈ ⊤ yang tidak berguna.

noncomputable example (b : ι → V) (b_indep : LinearIndependent K b)
    (b_spans : ∀ v, v ∈ Submodule.span K (Set.range b)) : Basis ι K V :=
  Basis.mk b_indep (fun v _ ↦ b_spans v)

-- Keluarga vektor yang mendasari basis di atas memang ``b``.
example (b : ι → V) (b_indep : LinearIndependent K b)
    (b_spans : ∀ v, v ∈ Submodule.span K (Set.range b)) (i : ι) :
    Basis.mk b_indep (fun v _ ↦ b_spans v) i = b i :=
  Basis.mk_apply b_indep (fun v _ ↦ b_spans v) i

Secara khusus, ruang vektor model ι →₀ K memiliki basis yang disebut basis kanonik, dengan fungsi repr yang merupakan isomorfisme identitas dan karenanya mengembalikan setiap vektor tanpa perubahan. Basis ini disebut Finsupp.basisSingleOne. Finsupp berarti fungsi dengan dukungan hingga, sedangkan basisSingleOne merujuk pada fakta bahwa vektor-vektor basisnya berupa fungsi yang bernilai nol kecuali pada satu nilai masukan. Lebih tepatnya, vektor basis yang diindeks oleh i : ι adalah Finsupp.single i 1, yakni fungsi berdukungan hingga yang bernilai 1 pada i dan 0 di semua tempat lain.

variable [DecidableEq ι]

example : Finsupp.basisSingleOne.repr = LinearEquiv.refl K (ι →₀ K) :=
  rfl

example (i : ι) : Finsupp.basisSingleOne i = Finsupp.single i 1 :=
  rfl

Pembahasan fungsi berdukungan hingga tidak diperlukan ketika tipe indeksnya hingga. Dalam kasus ini, kita dapat menggunakan Pi.basisFun yang lebih sederhana dan memberikan basis bagi seluruh ι → K.

example [Finite ι] (x : ι → K) (i : ι) : (Pi.basisFun K ι).repr x i = x i := by
  simp

Kembali ke kasus umum basis ruang vektor abstrak, kita dapat menyatakan sembarang vektor sebagai kombinasi linear vektor-vektor basis. Mari kita lihat terlebih dahulu kasus mudah berupa basis hingga.

example [Fintype ι] : ∑ i : ι, B.repr v i • (B i) = v :=
  B.sum_repr v

Apabila ι tidak hingga, pernyataan di atas secara apriori tidak bermakna: kita tidak dapat mengambil jumlah atas ι. Namun, dukungan fungsi yang dijumlahkan bersifat hingga (yakni dukungan B.repr v). Kita perlu menerapkan konstruksi yang memperhitungkan fakta ini. Di sini, Mathlib menggunakan fungsi khusus yang perlu waktu untuk dipahami, yaitu Finsupp.linearCombination (yang dibangun di atas Finsupp.sum yang lebih umum). Jika diberikan fungsi berdukungan hingga c dari tipe ι ke medan dasar K dan sembarang fungsi f dari ι ke V, maka Finsupp.linearCombination K f c adalah jumlah atas dukungan c dari perkalian skalar c i • f i. Secara khusus, kita dapat menggantinya dengan jumlah atas sembarang himpunan hingga yang memuat dukungan c.

example (c : ι →₀ K) (f : ι → V) (s : Finset ι) (h : c.support ⊆ s) :
    Finsupp.linearCombination K f c = ∑ i ∈ s, c i • f i :=
  Finsupp.linearCombination_apply_of_mem_supported K h

Kita juga dapat mengasumsikan bahwa f berdukungan hingga dan tetap memperoleh jumlah yang terdefinisi dengan baik. Namun, pilihan yang dibuat oleh Finsupp.linearCombination relevan bagi pembahasan basis karena memungkinkan kita menyatakan generalisasi Basis.sum_repr.

example : Finsupp.linearCombination K B (B.repr v) = v :=
  B.linearCombination_repr v

Kita mungkin bertanya-tanya mengapa K menjadi argumen eksplisit di sini, meskipun dapat disimpulkan dari tipe c. Alasannya adalah bahwa Finsupp.linearCombination K f yang diterapkan sebagian merupakan objek yang menarik untuk dikaji tersendiri. Objek tersebut bukan fungsi biasa dari ι →₀ K ke V, melainkan pemetaan linear-K.

variable (f : ι → V) in
#check (Finsupp.linearCombination K f : (ι →₀ K) →ₗ[K] V)

Kembali ke pembahasan matematis, penting untuk memahami bahwa representasi vektor dalam suatu basis kurang berguna dalam matematika terformalisasi daripada yang mungkin Anda bayangkan. Sering kali, lebih efisien menggunakan sifat basis yang lebih abstrak secara langsung. Secara khusus, sifat universal basis yang menghubungkannya dengan objek bebas lain dalam aljabar memungkinkan kita membangun pemetaan linear dengan menentukan citra vektor-vektor basis. Konstruksi ini adalah Basis.constr. Bagi sembarang ruang vektor-K W, basis B memberikan isomorfisme linear Basis.constr B K dari ι → W ke V →ₗ[K] W. Isomorfisme ini dicirikan oleh fakta bahwa setiap fungsi u : ι → W dipetakan ke pemetaan linear yang mengirim vektor basis B i ke u i bagi setiap i : ι.

section

variable {W : Type*} [AddCommGroup W] [Module K W]
         (φ : V →ₗ[K] W) (u : ι → W)

#check (B.constr K : (ι → W) ≃ₗ[K] (V →ₗ[K] W))

#check (B.constr K u : V →ₗ[K] W)

example (i : ι) : B.constr K u (B i) = u i :=
  B.constr_basis K u i

Sifat ini memang mencirikan konstruksi tersebut karena pemetaan linear ditentukan oleh nilainya pada vektor-vektor basis:

example (φ ψ : V →ₗ[K] W) (h : ∀ i, φ (B i) = ψ (B i)) : φ = ψ :=
  B.ext h

Jika kita juga memiliki basis B' pada ruang sasaran, pemetaan linear dapat diidentifikasi dengan matriks. Identifikasi ini merupakan isomorfisme linear-K.

variable {ι' : Type*} (B' : Basis ι' K W) [Fintype ι] [DecidableEq ι] [Fintype ι'] [DecidableEq ι']

open LinearMap

#check (toMatrix B B' : (V →ₗ[K] W) ≃ₗ[K] Matrix ι' ι K)

open Matrix -- memperoleh akses ke notasi ``*ᵥ`` untuk perkalian matriks dan vektor.

example (φ : V →ₗ[K] W) (v : V) : (toMatrix B B' φ) *ᵥ (B.repr v) = B'.repr (φ v) :=
  toMatrix_mulVec_repr B B' φ v


variable {ι'' : Type*} (B'' : Basis ι'' K W) [Fintype ι''] [DecidableEq ι'']

example (φ : V →ₗ[K] W) : (toMatrix B B'' φ) = (toMatrix B' B'' .id) * (toMatrix B B' φ) := by
  simp

end

Sebagai latihan mengenai topik ini, kita akan membuktikan bagian dari teorema yang menjamin bahwa endomorfisme memiliki determinan yang terdefinisi dengan baik. Secara khusus, kita ingin membuktikan bahwa apabila dua basis diindeks oleh tipe yang sama, matriks representasi sembarang endomorfisme relatif terhadap masing-masing basis memiliki determinan yang sama. Untuk memperoleh hasil lengkap, bukti ini kemudian perlu dilengkapi dengan fakta bahwa semua basis memiliki tipe indeks yang isomorfik.

Tentu saja, Mathlib telah mengetahui hal ini dan simp dapat langsung menutup sasaran. Karena itu, jangan gunakan taktik tersebut terlalu dini; gunakanlah lemma yang disediakan.

open Module LinearMap Matrix

-- Beberapa lemma yang berasal dari fakta bahwa `LinearMap.toMatrix` adalah morfisme aljabar.
#check toMatrix_comp
#check id_comp
#check comp_id
#check toMatrix_id

-- Beberapa lemma yang berasal dari fakta bahwa ``Matrix.det`` adalah morfisme monoid multiplikatif.
#check Matrix.det_mul
#check Matrix.det_one

example [Fintype ι] (B' : Basis ι K V) (φ : End K V) :
    (toMatrix B B φ).det = (toMatrix B' B' φ).det := by
  set M := toMatrix B B φ
  set M' := toMatrix B' B' φ
  set P := (toMatrix B B') LinearMap.id
  set P' := (toMatrix B' B) LinearMap.id
  sorry
end

10.4.3. Dimensi

Kembali ke kasus satu ruang vektor, basis juga berguna untuk mendefinisikan konsep dimensi. Sekali lagi, terdapat kasus elementer berupa ruang vektor berdimensi hingga. Bagi ruang semacam itu, kita mengharapkan dimensi berupa bilangan asli. Dimensi ini diberikan oleh Module.finrank. Fungsi tersebut menerima medan dasar sebagai argumen eksplisit karena suatu grup abelian dapat menjadi ruang vektor atas medan yang berbeda-beda.

section

#check (Module.finrank K V : ℕ)

-- `Fin n → K` adalah ruang arketipal berdimensi `n` atas `K`.
example (n : ℕ) : Module.finrank K (Fin n → K) = n :=
  Module.finrank_fin_fun K

-- Dipandang sebagai ruang vektor atas dirinya sendiri, `ℂ` berdimensi satu.
example : Module.finrank ℂ ℂ = 1 :=
  Module.finrank_self ℂ

-- Namun, sebagai ruang vektor real, ruang tersebut berdimensi dua.
example : Module.finrank ℝ ℂ = 2 :=
  Complex.finrank_real_complex

Perhatikan bahwa Module.finrank didefinisikan bagi setiap ruang vektor. Fungsi ini menghasilkan nol bagi ruang vektor berdimensi tak hingga, sebagaimana pembagian dengan nol menghasilkan nol.

Tentu saja, banyak lemma memerlukan asumsi dimensi hingga. Inilah peran kelas tipe FiniteDimensional. Sebagai contoh, pikirkan bagaimana contoh berikut gagal tanpa asumsi tersebut.

example [FiniteDimensional K V] : 0 < Module.finrank K V ↔ Nontrivial V  :=
  Module.finrank_pos_iff

Dalam pernyataan di atas, Nontrivial V berarti V memiliki setidaknya dua elemen berbeda. Perhatikan bahwa Module.finrank_pos_iff tidak memiliki argumen eksplisit. Hal ini tidak bermasalah ketika digunakan dari kiri ke kanan, tetapi bermasalah ketika digunakan dari kanan ke kiri karena Lean tidak dapat menebak K dari pernyataan Nontrivial V. Dalam kasus tersebut, sintaks argumen bernama berguna setelah kita memeriksa bahwa lemma dinyatakan atas gelanggang bernama R. Jadi, kita dapat menulis:

example [FiniteDimensional K V] (h : 0 < Module.finrank K V) : Nontrivial V := by
  apply (Module.finrank_pos_iff (R := K)).1
  exact h

Penulisan di atas terasa ganjil karena kita telah memiliki h sebagai asumsi, sehingga kita dapat langsung memberikan bukti lengkap Module.finrank_pos_iff.1 h. Namun, teknik tersebut tetap berguna untuk diketahui dalam kasus yang lebih rumit.

Menurut definisi, FiniteDimensional K V dapat disimpulkan dari sembarang basis.

variable {ι : Type*} (B : Module.Basis ι K V)

example [Finite ι] : FiniteDimensional K V := Module.Basis.finiteDimensional_of_finite B

example [FiniteDimensional K V] : Finite ι :=
  (FiniteDimensional.fintypeBasisIndex B).finite
end

Dengan menggunakan fakta bahwa subtipe yang bersesuaian dengan subruang linear memiliki struktur ruang vektor, kita dapat membicarakan dimensi subruang.

section
variable (E F : Submodule K V) [FiniteDimensional K V]

open Module

example : finrank K (E ⊔ F : Submodule K V) + finrank K (E ⊓ F : Submodule K V) =
    finrank K E + finrank K F :=
  Submodule.finrank_sup_add_finrank_inf_eq E F

example : finrank K E ≤ finrank K V := Submodule.finrank_le E

Dalam pernyataan pertama di atas, tujuan anotasi tipe ialah memastikan bahwa koersi ke Type* tidak terpicu terlalu dini.

Sekarang kita siap mengerjakan latihan mengenai finrank dan subruang.

example (h : finrank K V < finrank K E + finrank K F) :
    Nontrivial (E ⊓ F : Submodule K V) := by
  sorry
end

Sekarang mari kita beralih ke kasus umum teori dimensi. Dalam kasus ini, finrank tidak berguna. Namun, bagi setiap dua basis dari ruang vektor yang sama, tetap terdapat bijeksi di antara tipe-tipe yang mengindeks kedua basis tersebut. Karena itu, kita masih dapat berharap mendefinisikan rank sebagai kardinal, yakni elemen dari “hasil bagi koleksi tipe oleh relasi ekuivalensi berupa keberadaan bijeksi”.

Ketika membahas kardinal, semakin sulit untuk mengabaikan persoalan landasan seputar paradoks Russell seperti yang kita lakukan di bagian lain buku ini. Tidak ada tipe yang memuat semua tipe karena hal itu akan menimbulkan inkonsistensi logis. Persoalan ini diselesaikan oleh hierarki semesta, yang biasanya kita coba abaikan.

Setiap tipe memiliki level semesta, dan level-level tersebut berperilaku serupa dengan bilangan asli. Secara khusus, terdapat level ke-0; semesta yang bersesuaian, Type 0, cukup dinotasikan sebagai Type. Semesta ini cukup untuk memuat hampir seluruh matematika klasik. Sebagai contoh, ℕ dan ℝ bertipe Type. Setiap level u memiliki penerus yang dinotasikan sebagai u + 1, dan Type u bertipe Type (u+1).

Namun, level semesta bukan bilangan asli; sifat dasarnya sangat berbeda dan level semesta tidak memiliki tipe. Secara khusus, Anda tidak dapat menyatakan sesuatu seperti u ≠ u + 1 dalam Lean. Tidak ada tipe tempat pernyataan tersebut dapat dibentuk. Bahkan, menyatakan Type u ≠ Type (u+1) pun tidak bermakna karena Type u dan Type (u+1) memiliki tipe yang berbeda.

Setiap kali kita menulis Type*, Lean menyisipkan variabel level semesta bernama u_n, dengan n berupa bilangan. Hal ini memungkinkan definisi dan pernyataan berlaku dalam semua semesta.

Jika diberikan level semesta u, kita dapat mendefinisikan relasi ekuivalensi pada Type u yang menyatakan bahwa dua tipe α dan β ekuivalen apabila terdapat bijeksi di antara keduanya. Tipe hasil bagi Cardinal.{u} berada dalam Type (u+1). Kurung kurawal menyatakan variabel semesta. Citra α : Type u dalam hasil bagi ini adalah Cardinal.mk α : Cardinal.{u}.

Namun, kita tidak dapat langsung membandingkan kardinal dalam semesta yang berbeda. Jadi, secara teknis kita tidak dapat mendefinisikan rank ruang vektor V sebagai kardinal semua tipe yang mengindeks basis V. Sebagai gantinya, rank didefinisikan sebagai supremum Module.rank K V dari kardinal semua himpunan bebas linear dalam V. Jika V memiliki level semesta u, rank-nya bertipe Cardinal.{u}.

#check V -- Type u_2
#check Module.rank K V -- Cardinal.{u_2}

Definisi ini tetap dapat dihubungkan dengan basis. Memang, terdapat pula operasi komutatif max pada level semesta. Jika diberikan dua level semesta u dan v, terdapat operasi Cardinal.lift.{u, v} : Cardinal.{v} → Cardinal.{max v u} yang memungkinkan kita menempatkan kardinal dalam semesta bersama dan menyatakan teorema dimensi.

universe u v -- `u` dan `v` menyatakan level semesta

variable {ι : Type u} (B : Module.Basis ι K V)
         {ι' : Type v} (B' : Module.Basis ι' K V)

example : Cardinal.lift.{v, u} (.mk ι) = Cardinal.lift.{u, v} (.mk ι') :=
  mk_eq_mk_of_basis B B'

Kita dapat menghubungkan kasus berdimensi hingga dengan pembahasan ini melalui koersi dari bilangan asli ke kardinal hingga (atau lebih tepatnya, kardinal hingga yang berada dalam Cardinal.{v}, dengan v sebagai level semesta dari V).

example [FiniteDimensional K V] :
    (Module.finrank K V : Cardinal) = Module.rank K V :=
  Module.finrank_eq_rank K V