9. 線形代数

9.1. ベクトル空間と線形写像

9.1.1. ベクトル空間

本書では任意の体上のベクトル空間を取り扱う抽象線形代数を直接始めます．しかし，行列はこの抽象的な理論には依存していません．これに関する情報は Section 9.4.1 で取り扱っています．Mathlibは実際には加群という用語による線形代数のより一般的なバージョンを扱っていますが，今のところ，これは風変わりな言い換えに過ぎないということにしておきます．

「 \(K\) を体とし， \(V\) を \(K\) 上のベクトル空間とする」（そして後続の結果への暗黙の引数とする）ということを述べるには次のようにします：

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

なぜ [AddCommGroup V] [Module K V] と2つの別々の型クラスが必要であるかについては Chapter 7 にて説明しました．簡単に説明すると次のようになります．数学的には \(K\) 上のベクトル空間構造を持つことは加法可換群構造を持つことを意味すると述べたいです．これをLeanに伝えることも可能です．しかし，Leanが \(V\) 型についてそのような群構造を見つけるにあたって必ず \(V\) から推論することができない 完全に未指定の 体 \(K\) を使ったベクトル空間構造を探しに行くことになります．これは型クラスの合成システムにとって非常に悪いことです．

ベクトル v とスカラー a の掛け算は a • v と表記されます．以下の例にて，この演算と足し算の相互作用に関する代数的なルールをいくつか挙げます．もちろん， simp や apply? でもこれらの証明を見つけてくれるでしょう．また，ベクトル空間や体の公理から導かれるゴールを解決するための module タクティクが存在し，可換環に対しての ring や 群に対しての group と同じように用いられます．しかし，スカラー倍が補題の名前で smul と略されることを覚えておくことも有益です．

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

より専門的な読者のために補足しておくと，Mathlibの線形代数は用語から示唆されるように，（必ずしも可換である必要はない）環上の加群も扱っています．実は，半環上の半加群さえもカバーしています．このようなレベルの一般性は必要ないと思われる方は，部分加群に作用するイデアルに関する多くの代数的ルールをうまく捉えた次の例について熟考するとよいでしょう：

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

9.1.2. 線形写像

次に必要なものは線形写像です．群の射と同様に，Mathlibの線形写像は束縛写像，つまり写像とその線形性の証明を詰め込んだものです．これらの束縛写像は適用されると普通の関数に変換されます．この設計の詳細については Chapter 7 を参照してください．

2つの K 上のベクトル空間 V と W の間の線形写像の型は V →ₗ[K] W で表されます．添字の l は線形（linear）を表します． K をこのように表記するのは奇妙に感じるかもしれません．しかし，これは複数の体が登場するときに真価を発揮します．例えば， \(ℂ\) から \(ℂ\) への実線形写像はすべて写像 \(z ↦ az + b\bar{z}\) ですが，写像 \(z ↦ az\) だけが複素直線であり，この違いは複素解析において非常に重要です．

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

V →ₗ[K] W 自体が興味深い代数的構造を持つことに注意してください（これがこれらの写像を束ねる動機のひとつです）．これは K 上のベクトル空間であり，そのため線形写像を足したりスカラーを掛けたりすることができます．

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

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

束縛写像を使うことの1つの欠点は，通常の関数合成が使えないことです．合成するには LinearMap.comp か ∘ₗ という記法を使う必要があります．

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

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

線形写像を構築するには主に2つの方法があります．まず関数とその線形性の証明を提供することで構造体を構築することです．いつものように，これは構造体のコードアクションによって容易になります： example : V →ₗ[K] V := _ と入力し，アンダースコアについているコードアクション「Generate a skeleton」を使用します．

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

なぜ LinearMap の証明についてのフィールドの名前はプライムで終わるのか不思議に思われるかもしれません．これは関数への強制が定義される前に定義されているためで，そのためこれらのフィールドは LinearMap.toFun という表現で記述されています．これらが関数に強制された表現で LinearMap.map_add と LinearMap.map_smul として再表現されるのはその後になります．まだこれで話は終わりではありません． map_add について，加法群の射，線形写像，連続線形写像， K 上の代数の写像など（束縛）写像を保存する足し算に適用するバージョンも必要になるかもしれません．これは（ルートの名前空間の） map_add です．中間バージョンの LinearMap.map_add は少し冗長ですが，ドット記法を使うことができ，時としてうまく機能します．同様の話は map_smul にもあり，一般的なフレームワークは Chapter 7 で説明されています．

#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)

また，Mathlibですでに定義されている線形写像を様々に組み合わせることで線形写像を作ることもできます．例えば，上記の例はすでに LinearMap.lsmul K V 3 として知られているものです．ここで K と V が明示的な引数である理由はいくつかあります．最も直接的な理由は，ただの LinearMap.lsmul 3 ではLeanが V や K を推論する方法がないからです．ただ， LinearMap.lsmul K V もそれ自体興味深いものです：これは K →ₗ[K] V →ₗ[K] V という型をもち， K （それ自体の上へのベクトル空間と見ています）から V から V への K 線型写像の空間への K 上の線形写像を意味します．

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

線形同型の型 LinearEquiv も存在し， V ≃ₗ[K] W で表されます． f : V ≃ₗ[K] W の逆は f.symm : W ≃ₗ[K] V ， f と g の合成は f.trans g であり f ≪≫ₗ g と表記され， V での自己同型は LinearEquiv.refl K V です．この型の要素は必要に応じて射や関数に強制されます．

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

LinearEquiv.ofBijective を使えば，全単射から同型を作ることができます．これによって逆関数は計算不可能になります．

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

上記の例では，宣言された型を使用して， .ofBijective が LinearEquiv.ofBijective を（名前空間を開くことなく）指していることをLeanが理解していることに注意してください．

9.1.3. ベクトル空間の直和と直積

直和と直積を使って，古いベクトル空間から新しいベクトル空間を作ることができます．まず2つのベクトル空間から始めましょう．この場合，直和と直積に違いはなく，単純に直積型を使うことができます．以下のコード片では，すべての構造写像（包含と射影）を線形写像として得る方法と，線形写像について直積へ入るものと直和から出るものを構築する際の普遍性を示しています（直和と直積の圏論的な区別に慣れていない場合は，普遍性の語彙を無視して以下の例に出てくる型に着目するとよいでしょう）．

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]

-- 1つ目への射影写像
example : V × W →ₗ[K] V := LinearMap.fst K V W

-- 2つ目への射影写像
example : V × W →ₗ[K] W := LinearMap.snd K V W

-- 直積の普遍性
example (φ : U →ₗ[K] V) (ψ : U →ₗ[K] W) : U →ₗ[K]  V × W := LinearMap.prod φ ψ

-- 写像の直積が1つ目の要素について期待されたものであること
example (φ : U →ₗ[K] V) (ψ : U →ₗ[K] W) : LinearMap.fst K V W ∘ₗ LinearMap.prod φ ψ = φ := rfl

-- 写像の直積が2つ目の要素について期待されたものであること
example (φ : U →ₗ[K] V) (ψ : U →ₗ[K] W) : LinearMap.snd K V W ∘ₗ LinearMap.prod φ ψ = ψ := rfl

-- 写像を並列に組み合わせることもできます
example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] T) : (V × W) →ₗ[K] (U × T) := φ.prodMap ψ

--- 以下は直積の普遍性を組み合わせるだけで得られます
example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] T) :
  φ.prodMap ψ = (φ ∘ₗ .fst K V W).prod (ψ ∘ₗ .snd K V W) := rfl

-- 1つ目の包含写像
example : V →ₗ[K] V × W := LinearMap.inl K V W

-- 2つ目の包含写像
example : W →ₗ[K] V × W := LinearMap.inr K V W

-- 直和（いわゆる余積）の普遍性
example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] U) : V × W →ₗ[K] U := φ.coprod ψ

-- 余積の写像が1つ目の要素について期待されたものであること
example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] U) : φ.coprod ψ ∘ₗ LinearMap.inl K V W = φ :=
  LinearMap.coprod_inl φ ψ

-- 余積の写像が2つ目の要素について期待されたものであること
example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] U) : φ.coprod ψ ∘ₗ LinearMap.inr K V W = ψ :=
  LinearMap.coprod_inr φ ψ

-- 余積の写像が期待されるように定義されていること
example (φ : V →ₗ[K] U) (ψ : W →ₗ[K] U) (v : V) (w : W) :
    φ.coprod ψ (v, w) = φ v + ψ w :=
  rfl

end binary_product

次に任意のベクトル空間の族の直和と直積について考えましょう．ここでは，ベクトル空間の族を定義し，直和と直積の普遍性にアクセスする方法を簡単に説明します．直和の表記は DirectSum 名前空間にスコープされ，直和の普遍性は添字型に決定可能な等式を要求することに注意してください（これは実装上の偶然です）．

section families
open DirectSum

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

-- 直和の普遍性によって直和からの写像の構築は総和からの写像をまとめます
example (φ : Π i, (V i →ₗ[K] W)) : (⨁ i, V i) →ₗ[K] W :=
  DirectSum.toModule K ι W φ

-- 直積の普遍性によって直積への写像の構築は直積の因子への写像をまとめます
example (φ : Π i, (W →ₗ[K] V i)) : W →ₗ[K] (Π i, V i) :=
  LinearMap.pi φ

-- OMIT: The projection maps from the product
-- 直積からの射影写像
example (i : ι) : (Π j, V j) →ₗ[K] V i := LinearMap.proj i

-- 直和への包含写像
example (i : ι) : V i →ₗ[K] (⨁ i, V i) := DirectSum.lof K ι V i

-- 直積への包含写像
example (i : ι) : V i →ₗ[K] (Π i, V i) := LinearMap.single K V i

-- `ι` が有限型の場合，直和と直積の間には同型があります．
example [Fintype ι] : (⨁ i, V i) ≃ₗ[K] (Π i, V i) :=
  linearEquivFunOnFintype K ι V

end families

9.2. 部分空間と商空間

9.2.1. 部分空間

線形写像が束ねられているように， V の線形部分空間も束ねられた構造であり，部分空間の台集合と呼ばれる V の集合から構成され，関連する閉方の性質を持ちます．ここでもベクトル空間の代わりに加群の言葉が出てきますが，これはMathlibが線形代数により一般的な文脈を使用しているためです．

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

上の例では， Submodule K V は V の K 上の線形部分空間の型であり， U が Set V の元である IsSubmodule U という述語ではないことを理解することが重要です． Submodule K V は Set V への強制子と V への所属についての述語を持ちます．この方法と理由については Section 7.3 を参照してください．

もちろん，2つの部分空間が同じであるのは，同じ要素を持つ場合に限ります．この事実は ext タクティクで使用するために登録されており，2つの集合が等しいことを証明するのと同じように，2つの部分空間が等しいことを証明するために使用することができます．

例えば， ℝ が ℂ の ℝ 上の線形部分空間であることを述べて証明するために実際に必要なものは， Set ℂ への射影が ℝ （より正確には ℂ 中の像 ℝ ）である Submodule ℝ ℂ 型の項を構成することです．

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

Submodule の証明フィールドの末尾についているプライムは LinearMap のものと似ています．これらのフィールドは MemberShip インスタンスの前に定義されているため， carrier フィールドを使って記述されています．この記述の後では，これらのフィールドは Submodule.add_mem と Submodule.zero_mem ， Submodule.smul_mem に取って代わられます．

部分空間と線形写像の操作の演習として，線形写像による部分空間の逆像を定義しましょう（もちろん，Mathlibがこのことを知っていることは後で見ます）． Set.mem_preimage は所属と逆像を含む文を書き換えるのに使うことができることを覚えておいてください．必要な補題は今のこれと， LinearMap と Submodule について上述した補題だけです．

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
    dsimp
    sorry
  add_mem' := by
    sorry
  smul_mem' := by
    dsimp
    sorry

型クラスを使うことで，Mathlibはベクトル空間の部分空間がベクトル空間の構造を継承することを知っています．

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

この例は微妙です．オブジェクト U は型ではありませんが，Leanはそれを V の部分型と解釈することで，自動的に型に強制しています．つまり，上の例はより明確に次のように言い換えることができます：

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

9.2.2. 完備束構造と内部直和

述語 IsSubmodule : Set V → Prop の代わりに Submodule K V 型を持つことの重要な利点は， Submodule K V に追加の構造を簡単に与えられることです．重要なものとしては，包含に関して完備束構造を持つことです．例えば， V の2つの部分空間の共通部分が再び部分空間であるという補題を持つ代わりに，束の演算 ⊓ を使って共通部分を構成します．そして，束に関する任意の補題をこの構成に適用することができます．

ここで，2つの部分空間の下限の台集合が定義上確かにそれらの共通部分であることを確認しましょう．

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

台集合の共通部分に相当するものに対して異なる表記をするのは奇妙に見えるかもしれませんが，部分空間の合併は一般的に部分空間ではないため，この対応関係は上限演算や集合の合併には引き継がれません．代わりに合併によって生成される部分空間を使用する必要があり，これは 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]

もう1つの微妙な点は， V 自身は Submodule K V という型を持たないため， V の部分空間として見た V について語る方法が必要だということです．これは束の構造によって提供されます：完全な部分空間はこの束の一番上の要素です．

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

同じように，この束のボトムの要素は，唯一の要素が零元である部分空間です．

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

特に，（内部）直和の中の部分空間の場合について議論することができます．部分空間が2つの場合，任意の有界な半順序型に対して意味を為す汎用的な述語 IsCompl を使用します．一般的な部分空間の族である場合は， DirectSum.IsInternal を使用します．

-- 2つの部分空間が直和である場合，それらで空間全体が張られます．
example (U V : Submodule K V) (h : IsCompl U V) :
  U ⊔ V = ⊤ := h.sup_eq_top

-- 2つの部分空間が直和である場合，それらは0でのみ交わります．
example (U V : Submodule K V) (h : IsCompl U V) :
  U ⊓ V = ⊥ := h.inf_eq_bot

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

-- 部分空間が直和である場合，それらで空間全体が張られます．
example (U : ι → Submodule K V) (h : DirectSum.IsInternal U) :
  ⨆ i, U i = ⊤ := h.submodule_iSup_eq_top

-- 部分空間が直和である場合，それらは0でのみ交わります．
example {ι : Type*} [DecidableEq ι] (U : ι → Submodule K V) (h : DirectSum.IsInternal U)
    {i j : ι} (hij : i ≠ j) : U i ⊓ U j = ⊥ :=
  (h.submodule_independent.pairwiseDisjoint hij).eq_bot

-- これらの条件は直和で特徴づけられています．
#check DirectSum.isInternal_submodule_iff_independent_and_iSup_eq_top

-- 外部直和との関係：ある部分空間の族が内部直和にある場合，その外部直和からの `V` への写像は線形同型です．
noncomputable example {ι : Type*} [DecidableEq ι] (U : ι → Submodule K V)
    (h : DirectSum.IsInternal U) : (⨁ i, U i) ≃ₗ[K] V :=
  LinearEquiv.ofBijective (coeLinearMap U) h
end

9.2.3. 集合で張られた部分空間

既存の部分空間から部分空間を構築するだけでなく，集合 s を含む最小の部分空間を構築する Submodule.span K s を使って，任意の集合 s から部分空間を構築することもできます．紙の上では，この空間は s の要素のすべての線形結合で構成されることが一般的です．しかし，多くの場合 Submodule.span_le で表される普遍性とガロア接続の理論全体を使用する方が効率的です．

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

これらでは十分ではない場合，関連した帰納的原理 Submodule.span_induction を使うことができます．これは，ある性質が zero と s の要素で成り立ち，直和とスカラー倍で保たれる限り， s のスパンのすべての要素で成り立つことを保証するものです．このような補題の常として，Leanは関心のある述語を理解するために利用者の助けを必要とすることがあります．

演習として， Submodule.mem_sup の片方の含意を再証明してみましょう． V 上の様々な代数演算に関連する公理から従うゴールを閉じるために module というタクティクが使えることを覚えておいてください．

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
  apply Submodule.span_induction h (p := fun x ↦ ∃ s ∈ S, ∃ t ∈ T, x = s + t)
  · sorry
  · sorry
  · sorry
  · sorry

9.2.4. 部分空間の押し出しと引き戻し

以前の約束通り，線形写像による部分空間の押し出しと引き戻しの方法を説明しましょう．Mathlibの常として，1つ目の操作は map と呼ばれ，2つ目の操作は 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)

これらは Submodule 名前空間の中に存在するため， Submodule.map φ E の代わりにドット記法を使って E.map φ と書くこともできますが，これは大変読みにくいものになります（Mathlibのコントリビュータの中にはこの書き方を使う人もいます）．

特に，線形写像の範囲と核は部分空間です．これらの特殊ケースはあえて宣言する必要があるほど重要です．

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

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

LinearMap.ker φ の代わりに φ.ker と書けないことに注意してください．というのも LinearMap.ker はより多くの構造を保存する写像のクラスにも適用されるため，型が LinearMap で始まる引数を想定しておらず，そのためドット記法はここでは使えません．しかし，右辺ではドット記法の他の方法を使うことができます．Leanは左辺をエラボレートした後には Submodule K V という型を持つ項を期待するため， .comap を Submodule.comap と解釈します．

以下の補題は，これらの部分加群と φ の性質との間の重要な関係を与えます．

open Function LinearMap

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

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

演習として， map と comap のガロア接続の性質を証明してみましょう．以下の補題を使うこともできますが，定義上真であるためこれは必須ではありません．

#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

9.2.5. 商空間

商ベクトル空間は一般的な商記法（通常の / ではなく \quot と打ち込みます）を使用します．商空間への射影は Submodule.mkQ で，普遍性は 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

演習問題として，商空間の部分空間の対応定理を証明しましょう．Mathlibはこの事実をもう少し正確なバージョンである 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

9.3. 自己準同型

線形写像の重要な特殊ケースは自己準同型です：これはあるベクトル空間からそれ自体への線形写像です．これらは K 代数を形成するため興味深いものです．特に， K に係数を持つ多項式を評価することができ，固有値と固有ベクトルを持つことができます．

Mathlibでは Module.End K V := V →ₗ[K] V という略語を使いますが，これは（特に 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

example (φ ψ : End K V) : φ * ψ = φ ∘ₗ ψ :=
  LinearMap.mul_eq_comp φ ψ -- `rfl` would also work

-- `φ` にて `P` を評価する
example (P : K[X]) (φ : End K V) : V →ₗ[K] V :=
  aeval φ P

-- `φ` にて `X` を評価すると `φ` が戻ってくる
example (φ : End K V) : aeval φ (X : K[X]) = φ :=
  aeval_X φ

自己準同型と部分空間，多項式を操作する練習として，（二項）核の補題を証明しましょう：任意の自己準同型 \(φ\) と2つの互いに素な多項式 \(P\) と \(Q\) に対して， \(\ker P(φ) ⊕ \ker Q(φ) = \ker \big(PQ(φ)\big)\) が成り立ちます．

IsCoprime x y は ∃ 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 LinearMap.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

ここで固有空間と固有値の議論に移ります．定義によれば，自己準同型 \(φ\) とスカラー \(a\) の固有空間は \(φ - aId\) の核です．まず理解しなければならないのは， \(aId\) の書き方です． a • LinearMap.id を使うこともできますが，Mathlibでは algebraMap K (End K V) a を使っており，これは K 代数構造と直接うまく動きます．

example (a : K) : algebraMap K (End K V) a = a • LinearMap.id := rfl

次に注意しなければならないのは，固有空間はすべての a の値に対して定義されますが，それが0ではない場合にのみ興味があるということです．しかし，固有ベクトルは定義上，固有空間の非0要素です．対応する述語は End.HasEigenvector です．

example (φ : End K V) (a : K) :
    φ.eigenspace a = LinearMap.ker (φ - algebraMap K (End K V) a) :=
  rfl

そして述語 End.HasEigenvalue とこれに対応する部分型 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

-- 固有値は最小多項式の平方根
example (φ : End K V) (a : K) : φ.HasEigenvalue a → (minpoly K φ).IsRoot a :=
  φ.isRoot_of_hasEigenvalue

-- 有限次元では，その逆もまた真である（次元については以下で議論します）
example [FiniteDimensional K V] (φ : End K V) (a : K) :
    φ.HasEigenvalue a ↔ (minpoly K φ).IsRoot a :=
  φ.hasEigenvalue_iff_isRoot

-- ケーリーハミルトン
example [FiniteDimensional K V] (φ : End K V) : aeval φ φ.charpoly = 0 :=
  φ.aeval_self_charpoly

9.4. 行列・基底・次元

9.4.1. 行列

抽象的なベクトル空間の基底を導入する前に，ある体 \(K\) に対する \(K^n\) における線形代数の最も初歩的な設定に戻ります．ここでの主な対象はベクトルと行列です．具体的なベクトルには ![…] という表記を使うことができ，成分はカンマで区切られます．具体的な行列には !![…] という表記を使うことができ，行はセミコロンで，行の成分はカンマで区切ります．要素が ℕ や ℚ のような計算可能な型を持っている場合， eval コマンドを使って基本的な演算を行うことができます．

section matrices

-- ベクトルの加法
#eval !![1, 2] + !![3, 4]  -- !![4, 6]

-- 行列の加法
#eval !![1, 2; 3, 4] + !![3, 4; 5, 6]  -- !![4, 6; 8, 10]

-- 行列の乗法
#eval !![1, 2; 3, 4] * !![3, 4; 5, 6]  -- !![4, 6; 8, 10]

この #eval の使用は確認のためだけのものであり，Sageのようなコンピュータ代数システムを置き換えるものではないことを理解することが重要です．ここで使用されている行列のデータ表現は計算効率に優れているわけではありません．配列の代わりに関数を使っており，計算ではなく証明に最適化されています． #eval が使用する仮想マシンもこの用途に最適化されていません．

行列表記は行のリストですが，ベクトル表記は行ベクトルでも列ベクトルでもない点に注意してください．行列に左（または右）からのベクトルを掛ける場合，そのベクトルを行（または列）ベクトルとして解釈します．これはそれぞれ ᵥ* という表記の Matrix.vecMul と *ᵥ という表記の Matrix.mulVec に対応します．これらの記法は Matrix 名前空間にスコープされているため，使う場合は開く必要があります．

open Matrix

-- 行列をベクトルに左から作用させる
#eval !![1, 2; 3, 4] *ᵥ ![1, 1] -- ![3, 7]

-- 行列をベクトルに左から作用させ，結果はサイズが1の行列になる
#eval !![1, 2] *ᵥ ![1, 1]  -- ![3]

-- 行列をベクトルに右から作用させる
#eval  ![1, 1, 1] ᵥ* !![1, 2; 3, 4; 5, 6] -- ![9, 12]

ベクトルで指定された内容と同一の行または列を持つ行列を生成するには Matrix.row と Matrix.column を使用します．引数には行または列のインデックスを指定する型とベクトルを指定します．例えば，単一行または単一列の行列（より正確には行または列のインデックスが Fin 1 である行列）を得ることができます．

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

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

その他には，ベクトルのドット積，行列の転置，正方行列の行列式やトレースなどのおなじみの演算があります．

-- ベクトルのドット積
#eval ![1, 2] ⬝ᵥ ![3, 4] -- `11`

-- 行列の転置
#eval !![1, 2; 3, 4]ᵀ -- `!![1, 3; 2, 4]`

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

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

例えば実数など，要素が計算可能な型を持っていない場合， #eval の助けを期待することはできません．また，このような評価は信頼できるコードベース（つまり証明をチェックする際に信頼する必要があるLeanの部分）を大幅に拡張しない限り，証明に使用することはできません．

そのため simp や norm_num を証明の中で使ったり，これと対のコマンドを簡単な確認のために使ったりするのも良いでしょう．

#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`

正方行列に対する次の重要な操作は逆行列です．Leanにおいて数値の除法が常に定義され，0による除算では人為的に0を返すのと同じように，逆行列を求める演算はすべての行列に対して定義され，非可逆行列では零行列を返します．

より正確には，任意の環においてこれを行う一般的な関数 Ring.inverse があり，任意の行列 A に対して， A⁻¹ は Ring.inverse A.det • A.adjugate として定義されます．Cramerのルールによれば，これは A の行列式が0でない場合に A の逆行列となります．

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

もちろん，この定義は可逆な行列に対してのみ有効です．これを記すための一般的な型クラス Invertible があります．例えば，次の例の simp の呼び出しは補題 inv_mul_of_invertible を使用しますが，この補題は Invertible という型クラスの仮定を有します．ここでは 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

これの完全に具体的なケースでは， norm_num という機構と，最後の行を探すために apply? を使うこともできます：

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

上記のすべての具体的な行列は，ある n に対して行と列のインデックスが Fin n でした（行と列が同じとは限りません）．しかし，任意の有限型を使って行列にインデックスを付けた方が便利な場合もあります．例えば，有限グラフの隣接行列は，行と列がグラフの頂点によって自然に添字付けられます．

実は，行列に対する演算を定義せずに行列を定義したい場合，インデックスの型の有限性は必要なく，係数は代数的な構造なしに任意の型を持つことができます．そのため，Mathlibは Matrix m n α を m ， n ， α の型に対してただ m → n → α とだけ定義しており，これまで使ってきた行列は Matrix (Fin 2) (Fin 2) ℝ のような型を持っていました．もちろん，代数演算には m ， n ， α により仮定を置く必要があります．

m → n → α を直接使用しない主な理由は，型クラスシステムが利用者が必要なものを理解できるようにするためです．例えば，環 R の場合，型 n → R は点ごと単位の乗算演算を持つのと同様に， m → n → R も同じ演算を持っており，これは行列に対して欲しい乗算 ではありません ．

以下の最初の例では，Leanに Matrix の定義を見破らせ，この文を意味のあるものとして受け入れさせ，すべての要素をチェックすることで証明しています．

しかし，その次の2つの例からは，Leanは Fin 2 → Fin 2 → ℤ の点ごとの乗算ではなく 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

型クラス合成のための Matrix の利点を失うことなく，行列を関数として定義するために，関数と行列の間の等価性 Matrix.of を使用することができます．この等価性は Equiv.refl によって密かに定義されています．

例えば，ベクトル v に対応するVandermonde行列を定義することができます．

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

9.4.2. 基底

ここでベクトル空間の基底について議論したいと思います．非形式的にこの概念を定義する方法はたくさんあります．一方で普遍性を使うこともできます．また線形独立で空間を張るベクトルの族であるということもできます．あるいはこれらの性質を組み合わせて，基底とはすべてのベクトルが基底ベクトルの線形結合として一意に書けるようなベクトルの族であると直接言うこともできます．さらに別の言い方をすると，基底は K 上のベクトル空間として見たときに，基底の体 K のべき乗と線形同型を提供します．

この同型バージョンがMathlibにて実際に定義として採用されているもので，他の特徴づけはここから証明されます．無限基底の場合，「 K のべき乗」という考え方に少し注意が必要です．実際，この代数的な文脈で意味を持つのは有限の線形結合の場合だけです．したがって，参照するベクトル空間として必要なのは K のコピーの直積ではなく直和です．これのために基底の添字としてある型 ι によって ⨁ i : ι, K を使うことも可能ですが，こちらではなくより特殊化した ι →₀ K という書き方を使います．これは「有限台を持つ ι から K への関数」，つまり ι の有限集合（この有限集合は固定ではなく，関数に依存します）の外側で消える関数を意味します．このような関数を規定 B からベクトル v と i : ι で評価すると， i 番目の基底ベクトル v の成分（または座標）が返されます．

K ベクトル空間としての V の型 ι を添字とする基底の型は Basis ι K V です．この同型を Basis.repr と呼びます．

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

section

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

-- ``i`` 番目の基底ベクトル
#check (B i : V)

-- ``B`` から与えられるモデル空間の線形同型
#check (B.repr : V ≃ₗ[K] ι →₀ K)

-- ``v`` の成分の関数
#check (B.repr v : ι →₀ K)

-- ``i`` 番目の ``v`` の成分
#check (B.repr v i : K)

このような同型から始める代わりに，線形独立で空間を張るベクトルの族 b から始めることができ，これは Basis.mk と名付けられています．

この族が空間を張るという仮定は ⊤ ≤ Submodule.span K (Set.range b) として記述されます．ここで ⊤ は V の最上位の部分加群，つまり V をそれ自身の部分加群として見たものです．この書き方は少し面倒に見えるでしょうが，以下で見るようにこれはより読みやすい ∀ v, v ∈ Submodule.span K (Set.range b) と定義上ほぼ等しいです（以下のコード片中のアンダースコアは有益ではない情報 v ∈ ⊤ を意味しています）．

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)

-- 上記の基底の台となるベクトルの族が実際に ``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

特に，モデルベクトル空間 ι →₀ K はいわゆる正準基底を持っており，任意のベクトル上で評価される repr 関数は恒等同型です．これは Finsupp.basisSingleOne と呼ばれ，ここで Finsupp は有限台の関数を意味し， basisSingleOne は基底ベクトルが1つの入力値に対して消える関数であることを意味します．より正確には， i : ι で添字付けられる基底ベクトルは Finsupp.single i 1 であり，これは i で値 1 を取り，それ以外の場所では 0 を取る有限台の関数です．

variable [DecidableEq ι]

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

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

添字の型が有限の場合，有限台の関数の話は不要です．この場合，より単純な Pi.basisFun を使うことができ，これは ι → K 全体の基底を与えます．

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

抽象ベクトル空間の基底の一般的なケースに戻ると，任意のベクトルを基底ベクトルの線形結合として表現することができます．まずは有限基底の簡単な場合を見てみましょう．

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

ι が有限でない場合，上の文は先験的に意味を為しません：すなわち ι 上で和を取れません．しかし，和の対象となる関数の台は有限です（ B.repr v の台です）．ただし，そのためにはこれを考慮した構成を適用する必要があります．ここでMathlibは取っつき辛い特殊な関数を使います： Finsupp.linearCombination （これはより一般的な Finsupp.sum の上に構築されています）．ある型 ι から基底の体 K への有限台の関数 c と ι から V への任意の関数 f が与えられた時， Finsupp.linearCombination K f c はスカラー倍 c • f の c の台の上の和です．特に， 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

また， f が有限台であると仮定しても，well-definedな和を得ることができます．しかし， Finsupp.linearCombination による選択は， Basis.sum_repr の一般化を記述することができるため，基底の議論に関連します．

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

K は c の型から推測できるにもかかわらず，なぜここで明示的な引数になっているのか不思議に思われるかもしれません．ポイントは，部分適用される Finsupp.linearCombination K f 自体が興味深い対象であるということです．これは ι →₀ K から V へのただの関数ではなく， K の線形写像です．

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

上記の微妙な点は， Finsupp.linearCombination K f c の代わりにドット記法で c.linearCombination K f と書けないことの理由にもなります．実際， Finsupp.linearCombination は c を引数に取らず， Finsupp.linearCombination K f は関数型に強制され，この関数は c を引数に取ります．

数学的な議論に戻ると，ベクトルを基底で表現することは形式化された数学では思ったより役に立たないということを理解することが重要です．実際，基底のより抽象的な性質を直接利用する方が効率的な場合が多いです．特に，代数学における他の自由な対象に接続する基底の普遍性は，基底ベクトルの像を指定することによって線形写像を構成することを可能にします．これが Basis.constr です．任意の K ベクトル空間 W に対して，基底 B は ι → W から V →ₗ[K] W への線形同型 Basis.constr B K を与えます．この同型は，任意の関数 u : ι → W を，あらゆる i : ι に対して，基底ベクトル B i を u 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

線形写像は基底の上の値によって決定されるため，この性質は実に特徴的です：

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

もし対象の空間にも基底 B があれば，線形写像と行列を同定することができます．この同定は 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 -- get access to the ``*ᵥ`` notation for multiplication between matrices and vectors.

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

この話題の演習として，自己準同型がwell-definedな行列式を持つことを保証する定理の一部を証明します．すなわち，2つの基底が同じ型によって添字付けられる時，それらのどのような自己準同型に対応する行列も同じ行列式を持つことを証明しましょう．これは完全な結果を得るためには，すべての基底が同型の添字型を持つことを利用して補完する必要があります．

もちろんMathlibはこの事実をすでに知っており， simp はすぐにゴールを閉じることができるため，早急に用いず，代わりに補題を用いましょう．

open Module LinearMap Matrix

-- `LinearMap.toMatrix` が代数の射であることから導かれるいくつかの補題
#check toMatrix_comp
#check id_comp
#check comp_id
#check toMatrix_id

-- ``Matrix.det`` が乗法的モノイド射であることから導かれるいくつかの補題
#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

9.4.3. 次元

単一のベクトル空間の場合に戻ると，基底は次元の概念を定義するのにも便利です．ここでもまた，有限次元ベクトル空間のための初歩的なケースがあります．このような空間では，自然数である次元が期待されます．これが Module.finrank です．これは基底の体を明示的な引数として取ります．というのも与えられた可換群は異なる体上のベクトル空間になりうるからです．

section
#check (Module.finrank K V : ℕ)

-- `Fin n → K` は `K` 上の次元 `n` の典型的な空間です．
example (n : ℕ) : Module.finrank K (Fin n → K) = n :=
  Module.finrank_fin_fun K

-- それ自身をベクトル空間と見なすと， `ℂ` は1次元です．
example : Module.finrank ℂ ℂ = 1 :=
  Module.finrank_self ℂ

-- しかし，実数ベクトル空間では2次元です．
example : Module.finrank ℝ ℂ = 2 :=
  Complex.finrank_real_complex

Module.finrank は任意のベクトル空間に対して定義されることに注意してください．0による除算が0を返すように，無限次元のベクトル空間では0を返します．

もちろん，多くの補題は有限次元の仮定を必要とします．これが FiniteDimensional 型クラスの役割です．例えば，次の例がこの仮定なしでどのように失敗するか考えてみましょう．

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

上記の文において， Nontrivial V は V が少なくとも2つの異なる要素を持つことを意味します． Module.finrank_pos_iff には明示的な引数が無いことに注意してください．これは左から右へ使う場合には問題ありませんが，右から左へ使う場合には問題があります．というのも，Leanは Nontrivial V という文から K を推測することができないからです．このような場合，補題が R という名前の環の上で述べられていることを確認した後，名前引数の構文を使うことが便利です．従って以下のように書くことができます：

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

上記の書き方は奇妙です．というのもすでに仮定として h があるため，完全な証明である Module.finrank_pos_iff.1 h を与えることができるためです．とはいえ，より複雑なケースのために知っておいて損はないでしょう．

定義より， FiniteDimensional K V は任意の基底からも読むことができます．

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

example [Finite ι] : FiniteDimensional K V := FiniteDimensional.of_fintype_basis B

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

線形部分空間に対応する部分型がベクトル空間構造を持つことを利用して，部分空間の次元について話すことができます．

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

上記の最初の文では，型を明記するの目的は Type* への強制が早く発動しすぎないようにすることです．

これで finrank と部分空間についての演習の準備が整いました．

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

ここで次元論について一般的なケースに移りましょう．この場合， finrank は役に立ちませんが，同じベクトル空間の任意の2つの基底に対して，それらの基底を添字付ける型の間に全単射が存在することに変わりはありません．したがって，ランクを濃度，つまり「全単射の同値関係が存在する場合の型の集合の商」の要素として定義することが望めます．

濃度を論じるとき，本書の他のあらゆるところでそうしているように，ラッセルのパラドックスにまつわる基礎的な問題を無視することは難しくなります．論理的矛盾につながるため，すべての型の型は存在しません．この問題は，通常無視しようとしている宇宙の階層によって解決されます．

各型には宇宙レベルがあり，それらのレベルは自然数と同じように振る舞います．特に，0番目のレベルが存在し，対応する宇宙 Type 0 は単に Type を表記されます．この宇宙は古典数学のほとんどすべてを保持するのに十分です．例えば， ℕ と ℝ は Type 型を持ちます．各レベル u は u + 1 で示される後続を持ち， Type u は Type (u+1) 型を持ちます．

しかし，宇宙レベルは自然数ではなく，実際に異なる性質を持っており，また型を持ちません．特に， u ≠ u + 1 おようなことをLeanで述べることはできません．シンプルにこのようなことを表現する場所となる方が無いのです． Type u と Type (u+1) は型が異なるため， Type u ≠ Type (u+1) と書いたとしても意味を為さないのです．

Type* と書くと，Leanは u_n （ n は数値）という名前の宇宙レベルの変数を挿入します．これにより，定義や文がすべての宇宙で存在できるようになります．

ある宇宙レベル u が与えられると， Type u に対して2つの型 α と β の間に全単射があれば等価であるという同値関係を定義することができます．商の型 Cardinal.{u} は Type (u+1) の中に存在します．波括弧は宇宙変数を表します．この商における α : Type u の像は Cardinal.mk α : Cardinal.{u} です．

しかし，異なる宇宙の濃度を直接比較することはできません．したがって技術的にはベクトル空間 V のランクを V の基底を添字付けるすべての型の濃度として定義することはできません．そのため，代わりに V におけるすべての線形独立集合の濃度の上限 Module.rank K V として定義します． V が宇宙レベル u を持つ場合，そのランクは Cardinal.{u} 型を持ちます．

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

この定義を基底に関連付けることもできます．実際，宇宙レベルには可換な演算 max も存在し，2つの宇宙レベル u と v が与えられると共通の宇宙に濃度を置くことができる演算 Cardinal.lift.{u, v} : Cardinal.{v} → Cardinal.{max v u} が存在し，次元についての定理を述べることができます．

universe u v -- `u` and `v` will denote universe levels

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

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

自然数から有限濃度（正確には Cardinal.{v} に存在する有限濃度で， v は V の宇宙レベル）への強制を使って，有限次元のケースをこの議論に関連づけることができます．

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