8. 群と環
Section 2.2 にて群や環の演算を推論する方法を見ました．その後， Section 6.2 では群構造などの抽象的な代数構造や，ガウス整数上の環構造のような具体的な例を定義する方法を説明しました． Chapter 7 ではMathlibにおいて抽象的な構造がどのように階層付けられるかを説明しました．
この章では群と環をより詳しく扱います．Mathlibにおけるこれらのトピックの扱いについてすべての面をカバーすることはできません．というのもMathlibは常に成長しているからです．しかし，ライブラリへの入口を提供し，重要な概念がどのように使われているかを紹介します． Chapter 7 の議論と重なる部分もありますが，ここではトピックの扱い方の背後にある設計の理由ではなく，Mathlibの使い方に焦点を当てます．そのため，いくつかの例を理解するためには Chapter 7 の背景を復習する必要があるかもしれません．
8.1. モノイドと群
8.1.1. モノイドとその射
抽象代数の講義は群から始まり，環，体，ベクトル空間へと進んでいくことが多いです．環上の乗算を論じる際には乗算の演算が群構造に由来しないため若干のゆがみが生じますが，証明の多くは群論からこの新しい設定にそのまま引き継がれます．この歪みについてペンと紙を使って数学をする場合の最も一般的な修正は，これらの証明を演習問題として残すことです．効率は悪いですが，より安全で形式化しやすい方法はモノイドを使うことです．型 M 上の モノイド （monoid）構造とは，結合的であり，中立的な要素を持つ内部合成法則のことです．モノイドは主に群と環の情報構造の両方に対応するために使われます．しかし，自然な例も数多くあります；例えば，加算を備えた自然数の集合はモノイドを形成します．
Mathlibを使う際には実用的な観点としてモノイドはほとんど無視できます．しかし，Mathlibのファイルを眺めて補題を探す際にはモノイドの存在を知っておく必要があります．そうでなければ，探しているある文について元が可逆である必要が無い場合，本当はモノイドのファイルで見つかるはずであるのに，群論のファイルを探してしまう事態になりかねません．
型 M 上のモノイド構造の型は Monoid M と表記します．関数 Monoid は型クラスであるため，ほとんどの場合インスタンスの暗黙の引数として（つまり角括弧の中）現れます．デフォルトでは Monoid は乗法で演算を行います；加法で演算を行う場合は AddMonoid を使用してください．これらの構造体の可換バージョンは Monoid の前に接頭辞 Comm をつけます．
example {M : Type*} [Monoid M] (x : M) : x * 1 = x := mul_one x
example {M : Type*} [AddCommMonoid M] (x y : M) : x + y = y + x := add_comm x y
AddMonoid はライブラリにありはしますが，可換ではない演算で加法表記を使うのは一般的に混乱を招く点に留意してください．
モノイド M と N の間の射の型を MonoidHom M N と呼び， M →* N と書きます．Leanはこのような射を M の要素に適用すると，自動的に M から N への関数として見るようになります．これの加法バージョンは AddMonoidHom と呼ばれ， M →+ N と書かれます．
example {M N : Type*} [Monoid M] [Monoid N] (x y : M) (f : M →* N) : f (x * y) = f x * f y :=
f.map_mul x y
example {M N : Type*} [AddMonoid M] [AddMonoid N] (f : M →+ N) : f 0 = 0 :=
f.map_zero
これらの射は束縛写像，つまり写像とその性質をパッケージしたものです．束縛写像については Section 7.2 にて説明しています；ここでは，写像を合成するにあたって通常の関数合成を使うことができないという少し残念な結果を記させていただきます．この代わりに， MonoidHom.comp と AddMonoidHom.comp を使う必要があります．
example {M N P : Type*} [AddMonoid M] [AddMonoid N] [AddMonoid P]
(f : M →+ N) (g : N →+ P) : M →+ P := g.comp f
8.1.2. 群とその射
すべての元が逆元を持つという特別な性質を有するモノイドである群について，さらに多くのことを語ることになるでしょう．
example {G : Type*} [Group G] (x : G) : x * x⁻¹ = 1 := mul_inv_cancel x
以前見た ring タクティクと同様に，任意の群で成り立つあらゆる等式を証明する group タクティクが存在します．（これは同様に，自由群成り立つ等式も証明します．）
example {G : Type*} [Group G] (x y z : G) : x * (y * z) * (x * z)⁻¹ * (x * y * x⁻¹)⁻¹ = 1 := by
group
また可換加法群の等式用として abel というタクティクがあります．
example {G : Type*} [AddCommGroup G] (x y z : G) : z + x + (y - z - x) = y := by
abel
興味深いことに，群の射は群の間におけるモノイドの射にほかなりません．そのため，先ほどの例の1つをコピペして Monoid を Group に置き換えることができます．
example {G H : Type*} [Group G] [Group H] (x y : G) (f : G →* H) : f (x * y) = f x * f y :=
f.map_mul x y
もちろん群の射について，次のような新しい性質もあります：
example {G H : Type*} [Group G] [Group H] (x : G) (f : G →* H) : f (x⁻¹) = (f x)⁻¹ :=
f.map_inv x
もしかしたら群の射を構成するにあたって不要な作業が必要になることを憂慮するかもしれません．というのも，モノイドの射の定義では，中立元は中立元に送られることを要求しますが，群の射の場合は自動的に満たされるからです．実際にはこの余分な作業は難しくはありませんが，これを避けるために群の間の関数から，合成法則を保ちつつ群の射を作る関数があります．
example {G H : Type*} [Group G] [Group H] (f : G → H) (h : ∀ x y, f (x * y) = f x * f y) :
G →* H :=
MonoidHom.mk' f h
また，群（またはモノイド）の同型についての型 MulEquiv が用意されており， ≃* と表記されます（そして加法表記については AddEquiv にて ≃+ と表記します）． f : G ≃* H の逆射は MulEquiv.symm f : H ≃* G ， f と g の合成は MulEquiv.trans f g ，そして G についての恒等な同型は M̀ulEquiv.refl G をそれぞれ用います．匿名の射影記法を用いると，最初の2つはそれぞれ f.symm と f.trans g と書くことができます．この型の要素は必要に応じて自動的に射や関数に強制されます．
example {G H : Type*} [Group G] [Group H] (f : G ≃* H) :
f.trans f.symm = MulEquiv.refl G :=
f.self_trans_symm
MulEquiv.ofBijective を使うことで，全単射の射から同型を作ることができます．これにより逆関数は計算不可能になります．
noncomputable example {G H : Type*} [Group G] [Group H]
(f : G →* H) (h : Function.Bijective f) :
G ≃* H :=
MulEquiv.ofBijective f h
8.1.3. 部分群
群の射が束縛されるように， G の部分群も G の集合とそれに関連する閉性を束縛した構造です．
example {G : Type*} [Group G] (H : Subgroup G) {x y : G} (hx : x ∈ H) (hy : y ∈ H) :
x * y ∈ H :=
H.mul_mem hx hy
example {G : Type*} [Group G] (H : Subgroup G) {x : G} (hx : x ∈ H) :
x⁻¹ ∈ H :=
H.inv_mem hx
上の例では， Subgroup G は G の部分群の型であり， IsSubgroup H という述語（ここで H は Set G の要素）ではないことを理解することが重要です． Subgroup G は Set G に対する強制子と G に対する帰属についての述語を持ちます．この方法と理由については Section 7.3 を参照してください．
もちろん，2つの部分群が同じであるのは，それらが同じ要素を持つ場合だけです．この事実は ext タクティクで使用するために登録されており，2つの集合が等しいことを証明するためと同じ使用方法で，2つの部分群が等しいことを証明するために用いることができます．
例えば， ℤ が ℚ の加法部分群であることを記述・証明するには， Set ℚ への射影が ℤ （より正確には ℚ での ℤ の像）である AddSubGroup ℚ 型の項を作る必要があります．
example : AddSubgroup ℚ where
carrier := Set.range ((↑) : ℤ → ℚ)
add_mem' := by
rintro _ _ ⟨n, rfl⟩ ⟨m, rfl⟩
use n + m
simp
zero_mem' := by
use 0
simp
neg_mem' := by
rintro _ ⟨n, rfl⟩
use -n
simp
型クラスを使って，Mathlibは群の部分群が群構造を継承することを知っています．
example {G : Type*} [Group G] (H : Subgroup G) : Group H := inferInstance
この例は微妙です．オブジェクト H は型ではありませんが，Leanはこれを G の部分型と解釈することで自動的に型に強制します．つまり，上の例はより明確には次のように言い換えることができます：
example {G : Type*} [Group G] (H : Subgroup G) : Group {x : G // x ∈ H} := inferInstance
述語 IsSubgroup : Set G → Prop の代わりに Subgroup G 型を持つことの重要な利点は， Subgroup G に追加の構造を簡単に付与できることです．重要なのは，包含に関して完備束の構造を持つことです．例えば， G の2つの部分群の共通部分が再び部分群であるという補題を持つ代わりに，束の演算 ⊓ を使って共通部分を構成しました．そして，束に関する任意の補題をこの構成に適用することができます．
ここで，2つの部分群の下限の台集合が定義上，本当にそれらの共通部分であることを確認しましょう．
example {G : Type*} [Group G] (H H' : Subgroup G) :
((H ⊓ H' : Subgroup G) : Set G) = (H : Set G) ∩ (H' : Set G) := rfl
台集合の共通部分に相当するものに対して，異なる表記をするのは奇妙に見えるかもしれませんが，部分群の和は一般的に部分群ではないため，この対応は上限の演算や集合の合併には引き継がれません．その代わりに，合併から生成される部分群を使用する必要があり，これは Subgroup.closure を使用して得られます．
example {G : Type*} [Group G] (H H' : Subgroup G) :
((H ⊔ H' : Subgroup G) : Set G) = Subgroup.closure ((H : Set G) ∪ (H' : Set G)) := by
rw [Subgroup.sup_eq_closure]
もう一つの微妙な点は， G 自身は Subgroup G という型を持たないため， G の部分群として見た G について語る方法が必要だということです．これもまた束の構造から得られます：完全部分群はこの束の一番上の要素です．
example {G : Type*} [Group G] (x : G) : x ∈ (⊤ : Subgroup G) := trivial
同様に，この束の一番下の要素は中立元のみを持つ部分群です．
example {G : Type*} [Group G] (x : G) : x ∈ (⊥ : Subgroup G) ↔ x = 1 := Subgroup.mem_bot
群や部分群の操作についての演習問題として，ベースの群の元による部分群の共役を定義してみましょう．
def conjugate {G : Type*} [Group G] (x : G) (H : Subgroup G) : Subgroup G where
carrier := {a : G | ∃ h, h ∈ H ∧ a = x * h * x⁻¹}
one_mem' := by
dsimp
sorry
inv_mem' := by
dsimp
sorry
mul_mem' := by
dsimp
sorry
以前の2つのトピックを結び付けると，群の射を使って部分群を押し出したり引き戻したりすることができます．Mathlibの命名規則では，これらの操作を map と comap と呼んでいます．これらは一般的な数学用語ではありませんが，「押し出し（pushforward）」や「順像（direct image）」よりも短いという利点があります．
example {G H : Type*} [Group G] [Group H] (G' : Subgroup G) (f : G →* H) : Subgroup H :=
Subgroup.map f G'
example {G H : Type*} [Group G] [Group H] (H' : Subgroup H) (f : G →* H) : Subgroup G :=
Subgroup.comap f H'
#check Subgroup.mem_map
#check Subgroup.mem_comap
特に，射 f のもとでのボトムの部分群による逆像は f の 核 （kernel）と呼ばれる部分群であり， f のrangeも部分群となります．
example {G H : Type*} [Group G] [Group H] (f : G →* H) (g : G) :
g ∈ MonoidHom.ker f ↔ f g = 1 :=
f.mem_ker
example {G H : Type*} [Group G] [Group H] (f : G →* H) (h : H) :
h ∈ MonoidHom.range f ↔ ∃ g : G, f g = h :=
f.mem_range
群の射と部分群の操作についての演習問題として，いくつかの初歩的な性質を証明しましょう．これらの性質はMathlibですでに証明されているため，演習の効能を得たいのであれば， exact? に頼るのはなるべく後にしましょう．
section exercises
variable {G H : Type*} [Group G] [Group H]
open Subgroup
example (φ : G →* H) (S T : Subgroup H) (hST : S ≤ T) : comap φ S ≤ comap φ T := by
sorry
example (φ : G →* H) (S T : Subgroup G) (hST : S ≤ T) : map φ S ≤ map φ T := by
sorry
variable {K : Type*} [Group K]
-- 部分群の同値を証明するために `ext` タクティクを使えることを覚えておいてください．
example (φ : G →* H) (ψ : H →* K) (U : Subgroup K) :
comap (ψ.comp φ) U = comap φ (comap ψ U) := by
sorry
-- ある部分群をある準同型に沿って押し出し，さらに別の準同型に沿って押し出すことは
-- その準同型の合成に沿って押し出すことと同じである
example (φ : G →* H) (ψ : H →* K) (S : Subgroup G) :
map (ψ.comp φ) S = map ψ (S.map φ) := by
sorry
end exercises
Mathlibでの部分群の紹介の締めくくりとして，2つの非常に古典的な結果を紹介しましょう．Lagrangeの定理はある有限群の濃度をその部分群の濃度が割り切るというものです．Sylowの第一定理は，Lagrangeの定理の部分的な逆として有名です．
Mathlibのこのコーナーでは計算可能なように部分的に設定されていますが，次の open scoped コマンドを使えば，Leanに非構造的な論理を使うように指示することができます．
open scoped Classical
example {G : Type*} [Group G] (G' : Subgroup G) : Nat.card G' ∣ Nat.card G :=
⟨G'.index, mul_comm G'.index _ ▸ G'.index_mul_card.symm⟩
open Subgroup
example {G : Type*} [Group G] [Finite G] (p : ℕ) {n : ℕ} [Fact p.Prime]
(hdvd : p ^ n ∣ Nat.card G) : ∃ K : Subgroup G, Nat.card K = p ^ n :=
Sylow.exists_subgroup_card_pow_prime p hdvd
次の2つの演習問題はLagrangeの補題の系を導くものです．（これもすでにMathlibにあるので，すぐには exact? を使わないこと．）
lemma eq_bot_iff_card {G : Type*} [Group G] {H : Subgroup G} :
H = ⊥ ↔ Nat.card H = 1 := by
suffices (∀ x ∈ H, x = 1) ↔ ∃ x ∈ H, ∀ a ∈ H, a = x by
simpa [eq_bot_iff_forall, Nat.card_eq_one_iff_exists]
sorry
#check card_dvd_of_le
lemma inf_bot_of_coprime {G : Type*} [Group G] (H K : Subgroup G)
(h : (Nat.card H).Coprime (Nat.card K)) : H ⊓ K = ⊥ := by
sorry
8.1.4. 具体的な群
Mathlibでは具体的な群を走査することもできますが，これは抽象的な理論を扱うよりも複雑です．例えば，任意の型 X が与えられた時， X の置換群は Equiv.Perm X です．特に，対称群 \(\mathfrak{S}_n\) は Equiv.Perm (Fin n) となります．この群について抽象的な結果を述べることができます．例えば， X が有限である場合， Equiv.Perm X は巡回置換によって生成されます．
open Equiv
example {X : Type*} [Finite X] : Subgroup.closure {σ : Perm X | Perm.IsCycle σ} = ⊤ :=
Perm.closure_isCycle
完全に具体化して巡回置換の実際の積を計算することもできます．以下では与えらえた式に simp タクティクを呼び出す #simp コマンドを使用します． c[] という記法を用いて巡回置換を定義しています．この例では，結果は ℕ の置換です．最初に現れる数に (1 : Fin 5) のような型アスクリプションを使用することで， Perm (Fin 5) の計算が可能になります．
#simp [mul_assoc] c[1, 2, 3] * c[2, 3, 4]
具体的な群を扱うもう一つの方法は，自由群と群の表示を用いることです．型 α の自由群は FreeGroup α であり，包含写像は FreeGroup.of : α → FreeGroup α です．例えば， a ， b ， c と書かれる3つの元からなる型 S と，これに対応する自由群に含まれる元 ab⁻¹ を定義しましょう．
section FreeGroup
inductive S | a | b | c
open S
def myElement : FreeGroup S := (.of a) * (.of b)⁻¹
Leanが .of が FreeGroup.of を意味することが分かるように，定義に期待される型を与えていることに注意してください．
自由群の普遍性は同値 FreeGroup.lift として具現化されます．例えば， a を c[1, 2, 3] に， b を c[2, 3, 1] に， c を c[2, 3] に送る FreeGroup S から Perm (Fin 5) への群の射を定義しましょう．
def myMorphism : FreeGroup S →* Perm (Fin 5) :=
FreeGroup.lift fun | .a => c[1, 2, 3]
| .b => c[2, 3, 1]
| .c => c[2, 3]
最後の具体例として，3乗すると1になる単一の元から生成された群（このためこの群は \(\mathbb{Z}/3\) と同型になります）を定義し，この群から Perm (Fin 5) への射を構築する方法を見てみましょう．
要素を1つだけ持つ型として，ここでは唯一の要素を () で表す Unit を使用します．関数 PresentedGroup は関係の集合（つまりある自由群の元の集合）を受け取り，この自由群の関係によって生成される正規部分群による商群を返します．（より一般的な商の扱い方は Section 8.1.6 で説明します．）これは定義に隠れてしまうため， deriving Group を使って myGroup に群のインスタンスを作成します．
def myGroup := PresentedGroup {.of () ^ 3} deriving Group
群の表示の普遍性から，この群からの射が関係を対象の群の中立元に送る関数から構築できることを保証します．そこで，そのような関数とその条件が成り立つことの証明が必要になります．そしてこの証明を PresentedGroup.toGroup に与えることで，目的の群の射を得ることができます．
def myMap : Unit → Perm (Fin 5)
| () => c[1, 2, 3]
lemma compat_myMap :
∀ r ∈ ({.of () ^ 3} : Set (FreeGroup Unit)), FreeGroup.lift myMap r = 1 := by
rintro _ rfl
simp
decide
def myNewMorphism : myGroup →* Perm (Fin 5) := PresentedGroup.toGroup compat_myMap
end FreeGroup
8.1.5. 群作用
群論が数学の他の分野と相互作用する重要な方法の一つに群作用があります．ある型 X に対する群 G の作用は G から Equiv.Perm X への射にほかなりません．したがってある意味において，群作用はすでに以前の議論で網羅されています．しかし，この射を持ち歩きたくはありません；その代わりにできるだけLeanによって自動的に推論されるようにしたいです．そこで，このために MulAction G X という型クラスが用意されています．この構成の欠点は，同じ型に同じ群の複数の作用を持つ場合，それぞれを異なる型クラスのインスタンスが割り当てられるよう型シノニムを定義するなどの工夫が必要になることです．
これによって特に，ある点 x に対する群の元の作用を表すのに g • x を使うことができます．
noncomputable section GroupActions
example {G X : Type*} [Group G] [MulAction G X] (g g': G) (x : X) :
g • (g' • x) = (g * g') • x :=
(mul_smul g g' x).symm
これには AddAction という加法群版もあり，この作用は +ᵥ で表されます．これは例えばアフィン空間の定義で使われます．
example {G X : Type*} [AddGroup G] [AddAction G X] (g g' : G) (x : X) :
g +ᵥ (g' +ᵥ x) = (g + g') +ᵥ x :=
(add_vadd g g' x).symm
この作用に対応する群の射は MulAction.toPermHom と呼ばれます．
open MulAction
example {G X : Type*} [Group G] [MulAction G X] : G →* Equiv.Perm X :=
toPermHom G X
例として，任意の群 G の置換群，すなわち Perm G への埋め込みをケイリー同型に定義する方法を見てみましょう．
def CayleyIsoMorphism (G : Type*) [Group G] : G ≃* (toPermHom G G).range :=
Equiv.Perm.subgroupOfMulAction G G
以前とは異なり，上記の定義おいてはモノイド（あるいは乗算演算を持つ任意の型）ではなく，群であることを要求していることに注意してください．
群の条件は X を軌道に類別したいときに本当に重要になります．これに対応する X 上の同値関係は MulAction.orbitRel と呼ばれます．これはグローバルのインスタンスとして宣言されていません．
example {G X : Type*} [Group G] [MulAction G X] : Setoid X := orbitRel G X
これを用いて X は G の作用の下で軌道に類別されます．より正確には， X と依存積 (ω : orbitRel.Quotient G X) × (orbit G (Quotient.out' ω)) の間の全単射を得ることができます．ここで Quotient.out' ω は単に ω に射影する要素を選ぶだけです．この依存積の要素はペア ⟨ω, x⟩ であり，ここで x の orbit G (Quotient.out' ω) 型は ω に依存することを思い出してください．
example {G X : Type*} [Group G] [MulAction G X] :
X ≃ (ω : orbitRel.Quotient G X) × (orbit G (Quotient.out' ω)) :=
MulAction.selfEquivSigmaOrbits G X
特にXが有限である場合， Fintype.card_congr と Fintype.card_sigma を組み合わせることで， X の濃度は軌道の濃度の和であることを導くことができます．さらに，軌道は左移動作用による固定部分群の作用の下での G の商と全単射となります．この左移動作用による部分群の作用は， / という表記の部分群による商を定義するのに用いられるため，以下の簡潔な文を使うことができます．
example {G X : Type*} [Group G] [MulAction G X] (x : X) :
orbit G x ≃ G ⧸ stabilizer G x :=
MulAction.orbitEquivQuotientStabilizer G x
上記の2つの結果を組み合わせた重要な特殊ケースは， X が移動作用による部分群 H の作用を備えた群 G である場合です．この場合，すべての固定部分群は自明であるため，すべての軌道は H と全単射になり，次を得ます：
example {G : Type*} [Group G] (H : Subgroup G) : G ≃ (G ⧸ H) × H :=
groupEquivQuotientProdSubgroup
これは上で見たLagrangeの定理の概念上の別バージョンです．このバージョンでは有限性の仮定が無いことに注意してください．
この節の演習問題として，前の演習問題の conjugate の定義を使って，共役による部分群への群作用を構築してみましょう．
variable {G : Type*} [Group G]
lemma conjugate_one (H : Subgroup G) : conjugate 1 H = H := by
sorry
instance : MulAction G (Subgroup G) where
smul := conjugate
one_smul := by
sorry
mul_smul := by
sorry
end GroupActions
8.1.6. 商群
上記の群に作用する部分群の議論では，商 G ⧸ H が登場しました．一般的にはこれは単なる型です． H が正規部分群である場合に限り，商写像が群の射となるような群構造を与えることができます（そしてこの群構造は一意です）．
正規性の仮定は型クラス Subgroup.Normal であり，これによって型クラス推論が商の群構造を導き出すことができます．
noncomputable section QuotientGroup
example {G : Type*} [Group G] (H : Subgroup G) [H.Normal] : Group (G ⧸ H) := inferInstance
example {G : Type*} [Group G] (H : Subgroup G) [H.Normal] : G →* G ⧸ H :=
QuotientGroup.mk' H
商群の普遍性には QuotientGroup.lift を使ってアクセスすることができます：群の射 φ はその核が N を含むとすぐに G ⧸ N に誘導されます．
example {G : Type*} [Group G] (N : Subgroup G) [N.Normal] {M : Type*}
[Group M] (φ : G →* M) (h : N ≤ MonoidHom.ker φ) : G ⧸ N →* M :=
QuotientGroup.lift N φ h
上記のコード片で対象の群が M と呼ばれているのは， M にモノイド構造があれば十分であることを示唆しています．
重要な特殊ケースは N = ker φ の場合です．この場合，誘導された射は単射であり，その像に対して群同型を得ます．この結果はしばしば第一同型定理と呼ばれます．
example {G : Type*} [Group G] {M : Type*} [Group M] (φ : G →* M) :
G ⧸ MonoidHom.ker φ →* MonoidHom.range φ :=
QuotientGroup.quotientKerEquivRange φ
射 φ : G →* G' と商群の射影 Quotient.mk' N' との合成に普遍性を適用すると， G ⧸ N から G' ⧸ N' への射を求めることもできます．通常， φ に要求される条件は，「 φ は N の中に N を送るべきである」という形で形式化されます．しかし，これは φ が N を N の上に引き戻すべきであるということと等価であり，引き戻しの定義には存在量化子が含まれないため後者の条件の方が扱いやすいです．
example {G G': Type*} [Group G] [Group G']
{N : Subgroup G} [N.Normal] {N' : Subgroup G'} [N'.Normal]
{φ : G →* G'} (h : N ≤ Subgroup.comap φ N') : G ⧸ N →* G' ⧸ N':=
QuotientGroup.map N N' φ h
1つ気に留めるべき微妙な点は型 G ⧸ N は N に（定義上の等しさを除いて）本当に依存しているということであり，そのため2つの正規部分群 N と M が等しいことを証明するだけでは対応する商を等しくすることができません．しかし，普遍性はこの場合に同型を与えます．
example {G : Type*} [Group G] {M N : Subgroup G} [M.Normal]
[N.Normal] (h : M = N) : G ⧸ M ≃* G ⧸ N := QuotientGroup.quotientMulEquivOfEq h
本節の最後の演習問題として，もし H と K が有限群 G のdisjointな正規部分群であり，それらの濃度の積が G の濃度と等しい場合， G は H × K と同型であることを証明します．この文脈でのdisjointとは H ⊓ K = ⊥ を意味します．
まずは部分群について正規であることとdisjointであることを仮定せずにLagrangeの補題を少し使ってみましょう．
section
variable {G : Type*} [Group G] {H K : Subgroup G}
open MonoidHom
#check Nat.card_pos -- The nonempty argument will be automatically inferred for subgroups
#check Subgroup.index_eq_card
#check Subgroup.index_mul_card
#check Nat.eq_of_mul_eq_mul_right
lemma aux_card_eq [Finite G] (h' : Nat.card G = Nat.card H * Nat.card K) :
Nat.card (G ⧸ H) = Nat.card K := by
sorry
これ以降，部分群は正規かつdisjointであると仮定し，濃度の条件を仮定します．ここで，目的の同型の最初の構成要素を構築します．
variable [H.Normal] [K.Normal] [Fintype G] (h : Disjoint H K)
(h' : Nat.card G = Nat.card H * Nat.card K)
#check Nat.bijective_iff_injective_and_card
#check ker_eq_bot_iff
#check restrict
#check ker_restrict
def iso₁ [Fintype G] (h : Disjoint H K) (h' : Nat.card G = Nat.card H * Nat.card K) : K ≃* G ⧸ H := by
sorry
これで2つ目の構成要素を定義できます．ここでは MonoidHom.prod が必要であり，これは G₀ から G₁ × G₂ への射を G₀ から G₁ と G₂ への射に変換します．
def iso₂ : G ≃* (G ⧸ K) × (G ⧸ H) := by
sorry
これですべてをまとめる準備ができました．
#check MulEquiv.prodCongr
def finalIso : G ≃* H × K :=
sorry
8.2. 環
8.2.1. 環，単位元，射，部分間
型 R 上の環構造の型は Ring R です．乗法が可換であることを仮定するバージョンは CommRing R です．これまですでに， ring タクティクによって可換環の公理から導かれるあらゆる等式を証明することを見てきました．
example {R : Type*} [CommRing R] (x y : R) : (x + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y := by ring
より独特な変種として， R 上の足し算が群を形成する必要がなく，加法的なモノイドであるようなものがあります．これに対応する型クラスは Semiring R と CommSemiring R です．自然数の型は CommSemiring R の重要な例であり，自然数に値を取る関数の型も同様にこれに属します．もう一つの重要な例は，後述する環のイデアルの型です． ring タクティクという名前は二重にミスリーディングを生んでいます．というのも，これは可換性を仮定していますが，半環でも機能するからです．言い換えればこのタクティクはどんな CommSemiring に対しても適用できます．
example (x y : ℕ) : (x + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y := by ring
また乗法について単位元の存在や結合性を仮定しない環や半環のクラスもあります．ここではそれらについては触れません．
環論の入門として伝統的に教えられているいくつかの概念は，実はその根底にある乗法的モノイドに関するものです．顕著な例は環の単位元の定義です．すべての（乗法的）モノイド M は左右の逆元の存在を保証する述語 IsUnit : M → Prop と， Mˣ という表記で M に強制される単位元の型 Units M を持ちます．型 Units M は可逆元とその逆元を束ねたものであり，それぞれが実際にお互いの逆元であることを保証する性質でもあります．この実装の詳細は主に計算可能な関数を定義する時に関係します．ほとんどの場合， IsUnit.unit {x : M} : IsUnit x → Mˣ を使って単位元を作ることができます．可換の場合は， Units.mkOfMulEqOne (x y : M) : x * y = 1 → Mˣ で x を単位元と見なして利用することもできます．
example (x : ℤˣ) : x = 1 ∨ x = -1 := Int.units_eq_one_or x
example {M : Type*} [Monoid M] (x : Mˣ) : (x : M) * x⁻¹ = 1 := Units.mul_inv x
example {M : Type*} [Monoid M] : Group Mˣ := inferInstance
二つの（半）環 R と S の間の環の射の型は RingHom R S であり， R →+* S と表記されます．
example {R S : Type*} [Ring R] [Ring S] (f : R →+* S) (x y : R) :
f (x + y) = f x + f y := f.map_add x y
example {R S : Type*} [Ring R] [Ring S] (f : R →+* S) : Rˣ →* Sˣ :=
Units.map f
これの同型版は RingEquiv で， ≃+* と表記されます．
部分モノイドや部分群と同様に，環 R の部分環を表す Subring R 型が存在しますが，この部分環によって環の商を取ることができないため，部分群の型よりもはるかに使い勝手が悪いです．
example {R : Type*} [Ring R] (S : Subring R) : Ring S := inferInstance
また RingHom.range が部分環を生成することにも注目してください．
8.2.2. イデアルと商
歴史的な理由から，Mathlibには可換環のイデアルの理論しかありません．（環のライブラリはもともと現代の代数幾何学の基礎用として急ピッチで開発されたものです．）そのため本節では可換環を取り扱うこととします． R のイデアルは R の部分加群として定義されます．加群はのちに線形代数の章で扱われますが，イデアルの特別な文脈において関連する補題の（全てではありませんが）ほとんどが再述されるため，この実装の詳細はほとんど無視しても大丈夫です．しかし，匿名の射影記法は常に期待通りに機能するわけではありません．例えば，以下のコード片では Ideal.Quotient.mk I を I.Quotient.mk で置き換えることはできません．というのもここでは . が2つあるため，これは (Ideal.Quotient I).mk とパースされてしまい， Ideal.Quotient 自体は存在しないからです．
example {R : Type*} [CommRing R] (I : Ideal R) : R →+* R ⧸ I :=
Ideal.Quotient.mk I
example {R : Type*} [CommRing R] {a : R} {I : Ideal R} :
Ideal.Quotient.mk I a = 0 ↔ a ∈ I :=
Ideal.Quotient.eq_zero_iff_mem
商環の普遍性は Ideal.Quotient.lift です．
example {R S : Type*} [CommRing R] [CommRing S] (I : Ideal R) (f : R →+* S)
(H : I ≤ RingHom.ker f) : R ⧸ I →+* S :=
Ideal.Quotient.lift I f H
特に，これは環についての第一同型定理を導きます．
example {R S : Type*} [CommRing R] [CommRing S](f : R →+* S) :
R ⧸ RingHom.ker f ≃+* f.range :=
RingHom.quotientKerEquivRange f
イデアルは包含関係において完備束構造を形成し，また半環構造も持ちます．この2つの構造はうまく相互作用します．
variable {R : Type*} [CommRing R] {I J : Ideal R}
example : I + J = I ⊔ J := rfl
example {x : R} : x ∈ I + J ↔ ∃ a ∈ I, ∃ b ∈ J, a + b = x := by
simp [Submodule.mem_sup]
example : I * J ≤ J := Ideal.mul_le_left
example : I * J ≤ I := Ideal.mul_le_right
example : I * J ≤ I ⊓ J := Ideal.mul_le_inf
イデアルを押し出したり引き戻したりするにはそれぞれ Ideal.map と Ideal.comap を使います．いつものように，後者の方が存在量化子を伴わないため便利です．そのため，これは商環の間の射を構築するための条件として用いられています．
example {R S : Type*} [CommRing R] [CommRing S] (I : Ideal R) (J : Ideal S) (f : R →+* S)
(H : I ≤ Ideal.comap f J) : R ⧸ I →+* S ⧸ J :=
Ideal.quotientMap J f H
微妙な点として，型 R ⧸ I は実際に I に（定義上の等しさを除いて）依存するため，2つのイデアル I と J が等しいことを証明するだけでは対応する商を等しくすることができません．しかし，普遍性はこの場合に同型性を提供します．
example {R : Type*} [CommRing R] {I J : Ideal R} (h : I = J) : R ⧸ I ≃+* R ⧸ J :=
Ideal.quotEquivOfEq h
ここで中国の剰余における同型を紹介しましょう．添字付けられた上限記号 ⨅ と型についての大きな積記号 Π の違いに注意してください．フォントによっては区別が難しいかもしれません．
example {R : Type*} [CommRing R] {ι : Type*} [Fintype ι] (f : ι → Ideal R)
(hf : ∀ i j, i ≠ j → IsCoprime (f i) (f j)) : (R ⧸ ⨅ i, f i) ≃+* Π i, R ⧸ f i :=
Ideal.quotientInfRingEquivPiQuotient f hf
ZMod に関する記述としての初等版である中国の剰余定理は前のものから簡単に導くことができます．
open BigOperators PiNotation
example {ι : Type*} [Fintype ι] (a : ι → ℕ) (coprime : ∀ i j, i ≠ j → (a i).Coprime (a j)) :
ZMod (∏ i, a i) ≃+* Π i, ZMod (a i) :=
ZMod.prodEquivPi a coprime
一連の演習問題として，中国の剰余定理を一般的なケースで再現します．
まず商環の普遍性を用いて，定理に登場する写像を環の射として定義する必要があります．
variable {ι R : Type*} [CommRing R]
open Ideal Quotient Function
#check Pi.ringHom
#check ker_Pi_Quotient_mk
/-- ``R ⧸ ⨅ i, I i`` から ``Π i, R ⧸ I i`` への準同型は中国の剰余定理によって特徴づけられる -/
def chineseMap (I : ι → Ideal R) : (R ⧸ ⨅ i, I i) →+* Π i, R ⧸ I i :=
sorry
次の2つの補題が rfl で証明できることを確認してください．
lemma chineseMap_mk (I : ι → Ideal R) (x : R) :
chineseMap I (Quotient.mk _ x) = fun i : ι ↦ Ideal.Quotient.mk (I i) x :=
sorry
lemma chineseMap_mk' (I : ι → Ideal R) (x : R) (i : ι) :
chineseMap I (mk _ x) i = mk (I i) x :=
sorry
次の補題はイデアルの族を仮定することなく，中国の剰余定理の半分のうち簡単なほうを証明します．証明は1行にも満たないものになります．
#check injective_lift_iff
lemma chineseMap_inj (I : ι → Ideal R) : Injective (chineseMap I) := by
sorry
これで chineseMap の全射性を示す定理の核心に入る準備が整いました．まず，互いに素（co-maximality仮定とも呼ばれます）を表すさまざまな方法を知っておく必要があります．以下では最初の2つだけが必要です．
#check IsCoprime
#check isCoprime_iff_add
#check isCoprime_iff_exists
#check isCoprime_iff_sup_eq
#check isCoprime_iff_codisjoint
この機会に Finset に対する帰納法を使ってみることにしましょう．以下は Finset に関連する補題です． ring タクティクは半環にも機能し，環のイデアルは半環を形成することを思い出してください．
#check Finset.mem_insert_of_mem
#check Finset.mem_insert_self
theorem isCoprime_Inf {I : Ideal R} {J : ι → Ideal R} {s : Finset ι}
(hf : ∀ j ∈ s, IsCoprime I (J j)) : IsCoprime I (⨅ j ∈ s, J j) := by
classical
simp_rw [isCoprime_iff_add] at *
induction s using Finset.induction with
| empty =>
simp
| @insert i s _ hs =>
rw [Finset.iInf_insert, inf_comm, one_eq_top, eq_top_iff, ← one_eq_top]
set K := ⨅ j ∈ s, J j
calc
1 = I + K := sorry
_ = I + K * (I + J i) := sorry
_ = (1 + K) * I + K * J i := sorry
_ ≤ I + K ⊓ J i := sorry
これで中国の剰余定理に登場する写像の全射性を証明することができます．
lemma chineseMap_surj [Fintype ι] {I : ι → Ideal R}
(hI : ∀ i j, i ≠ j → IsCoprime (I i) (I j)) : Surjective (chineseMap I) := by
classical
intro g
choose f hf using fun i ↦ Ideal.Quotient.mk_surjective (g i)
have key : ∀ i, ∃ e : R, mk (I i) e = 1 ∧ ∀ j, j ≠ i → mk (I j) e = 0 := by
intro i
have hI' : ∀ j ∈ ({i} : Finset ι)ᶜ, IsCoprime (I i) (I j) := by
sorry
sorry
choose e he using key
use mk _ (∑ i, f i * e i)
sorry
これですべてのピースを次のようにまとめます：
noncomputable def chineseIso [Fintype ι] (f : ι → Ideal R)
(hf : ∀ i j, i ≠ j → IsCoprime (f i) (f j)) : (R ⧸ ⨅ i, f i) ≃+* Π i, R ⧸ f i :=
{ Equiv.ofBijective _ ⟨chineseMap_inj f, chineseMap_surj hf⟩,
chineseMap f with }
8.2.3. 代数と多項式
ある可換（半）環 R が与えられた時， R 上の代数 （algebra over R ）は，半環 A と A の各元に対して像が可換になる環の射からなります．これは型クラス Algebra R A としてエンコードされます． R から A への射は構造写像と呼ばれ， algebraMap R A : R →+* A と表記されます．ある r : R について a : A と algebraMap R A r の乗算は a と r のスカラー倍と呼ばれ， r • a と表記されます．このような代数の概念は，より一般的な代数の概念の存在を強調するために 結合的単位代数 （associative unital algebra）と呼ばれることがあります．
algebraMap R A が環の射であるという事実には以下のようなスカラー倍の多くの性質が内臓されています：
example {R A : Type*} [CommRing R] [Ring A] [Algebra R A] (r r' : R) (a : A) :
(r + r') • a = r • a + r' • a :=
add_smul r r' a
example {R A : Type*} [CommRing R] [Ring A] [Algebra R A] (r r' : R) (a : A) :
(r * r') • a = r • r' • a :=
mul_smul r r' a
2つの R 代数 A と B の間の射は， R の要素によるスカラー倍について可換な環の射です．これらは AlgHom R A B 型を持つ束縛射であり， A →ₐ[R] B と表記されます．
非可換環の重要な例として，自己準同型の代数と正方行列の代数が挙げられますが，これらは線形代数の章で扱います．本章では可換環論の最も重要な例で，すなわち多項式代数について述べます．
R に係数を持つ一変数多項式の代数は Polynomial R と呼ばれ， Polynomial 名前空間を開くだけで R[X] と書くことができます． R から R[X] への代数構造写像は C と表記されます．これは対応する多項式関数が常に定数関数になることから「定数（constant）」を意味しています．不定元は X で表されます．
open Polynomial
example {R : Type*} [CommRing R] : R[X] := X
example {R : Type*} [CommRing R] (r : R) := X - C r
上記の最初の例では定義の本体から型を決定することができないため，Leanに期待される型を与えることが重要です．二つ目の例では， r の型がわかっているため， C r の使用から大昌となる多項式代数を推測することができます．
C は R から R[X] への環の射であるため，環 R[X] で計算をする前に map_zero や map_one ， map_mul ， map_pow などの環の射についての補題を使うことができます．例えば：
example {R : Type*} [CommRing R] (r : R) : (X + C r) * (X - C r) = X ^ 2 - C (r ^ 2) := by
rw [C.map_pow]
ring
係数にアクセスするには Polynomial.coeff を使うことができます．
example {R : Type*} [CommRing R] (r:R) : (C r).coeff 0 = r := by simp
example {R : Type*} [CommRing R] : (X ^ 2 + 2 * X + C 3 : R[X]).coeff 1 = 2 := by simp
多項式の次数の定義は零多項式という特殊なケースがあるため常に厄介です．Mathlibには2つのバリエーションがあります： Polynomial.natDegree : R[X] → ℕ は零多項式に次数 0 を割り当てたもの，そして Polynomial.degree : R[X] → WithBot ℕ は ⊥ を割り当てたものです．後者では， WithBot ℕ は ℕ ∪ {-∞} と見なすことができますが， -∞ は ⊥ と表記されます．この特別な値は零多項式の次数として使われ，加法について吸収的です．（掛け算に対しては ⊥ * 0 = 0 を除いてほぼ吸収的です．）
理屈上は degree のバージョンが正しいです．例えば，積の次数について（ベースの環が零因子を持たないと仮定した場合に）期待される公式を述べることができます．
example {R : Type*} [Semiring R] [NoZeroDivisors R] {p q : R[X]} :
degree (p * q) = degree p + degree q :=
Polynomial.degree_mul
一方， natDegree 用のバージョンでは非零多項式を仮定する必要があります．
example {R : Type*} [Semiring R] [NoZeroDivisors R] {p q : R[X]} (hp : p ≠ 0) (hq : q ≠ 0) :
natDegree (p * q) = natDegree p + natDegree q :=
Polynomial.natDegree_mul hp hq
しかし， ℕ よりも WithBot ℕ の方が使いやすいため，Mathlibでは両方のバージョンを利用できるようにし，両者を変換するための定理を提供しています．また，合成の次数を計算する際には natDegree の方が便利です．多項式の合成は Polynomial.comp であり，次のようになります：
example {R : Type*} [Semiring R] [NoZeroDivisors R] {p q : R[X]} :
natDegree (comp p q) = natDegree p * natDegree q :=
Polynomial.natDegree_comp
多項式は多項式関数を生み出します：任意の多項式は Polynomial.eval を使って R 上で評価することができます．
example {R : Type*} [CommRing R] (P: R[X]) (x : R) := P.eval x
example {R : Type*} [CommRing R] (r : R) : (X - C r).eval r = 0 := by simp
特に，多項式が消失する R 内の要素 r に対して成り立つ IsRoot という述語があります．
example {R : Type*} [CommRing R] (P : R[X]) (r : R) : IsRoot P r ↔ P.eval r = 0 := Iff.rfl
R が零因子を持たないと仮定すると，重根の重複もカウントすると多項式は次数と同じ数の根を持つことになります．しかし，零多項式のケースはまたしても辛いものがあります．そこでMathlibは Polynomial.roots を定義しており，多項式 P を多集合，つまり P が0の場合は空，それ以外の場合は重根も含めた P の根として定義した有限集合に送るようにしています．これはベースの環が始域である場合にのみ定義されます．というのもそうでない場合は定義は良い性質を持たないからです．
example {R : Type*} [CommRing R] [IsDomain R] (r : R) : (X - C r).roots = {r} :=
roots_X_sub_C r
example {R : Type*} [CommRing R] [IsDomain R] (r : R) (n : ℕ):
((X - C r) ^ n).roots = n • {r} :=
by simp
Polynomial.eval と Polynomial.roots はどちらも係数環のみを考慮します． X ^ 2 - 2 : ℚ[X] が ℝ に根を持つ，あるいは X ^ 2 + 1 : ℝ[X] が ℂ に根を持つことを言えません．このため，任意の R 代数において P : R[X] を評価する Polynomial.aeval が必要です．より正確には，半環 A と Algebra R A のインスタンスが与えられた時， Polynomial.aeval は a の各元を a での R 代数の評価射に沿って送ります． AlgHom は関数に対する強制機能を持っているため，多項式に適用をすることができます．しかし， aeval は多項式を引数に取らないため，上記の P.eval のようなドット記法は使うことができません．
example : aeval Complex.I (X ^ 2 + 1 : ℝ[X]) = 0 := by simp
この文脈で roots に対応する関数は aroots であり，これは多項式と代数を受け取り，多集合を出力します（ roots と同じように零多項式についての注意点があります）．
open Complex Polynomial
example : aroots (X ^ 2 + 1 : ℝ[X]) ℂ = {Complex.I, -I} := by
suffices roots (X ^ 2 + 1 : ℂ[X]) = {I, -I} by simpa [aroots_def]
have factored : (X ^ 2 + 1 : ℂ[X]) = (X - C I) * (X - C (-I)) := by
have key : (C I * C I : ℂ[X]) = -1 := by simp [← C_mul]
rw [C_neg]
linear_combination key
have p_ne_zero : (X - C I) * (X - C (-I)) ≠ 0 := by
intro H
apply_fun eval 0 at H
simp [eval] at H
simp only [factored, roots_mul p_ne_zero, roots_X_sub_C]
rfl
-- MathlibはD'Alembert-Gaussの定理を知っています： ``ℂ`` は代数的に閉じています．
example : IsAlgClosed ℂ := inferInstance
より一般的には，環の射 f : R →+* S が与えられると， P : R[X] を S の点で Polynomial.eval₂ によって評価することができます．これは R[X] から S への実際の関数を生成するもので， Algebra R S インスタンスの存在を仮定していないためドット記法は期待通りに機能します．
#check (Complex.ofReal : ℝ →+* ℂ)
example : (X ^ 2 + 1 : ℝ[X]).eval₂ Complex.ofReal Complex.I = 0 := by simp
最後に多変数多項式について簡単に触れておきましょう．可換環 ℝ が与えられた時， R に係数と型 σ で添字付けられた不定元を持つ多項式の R 代数は MVPolynomial σ R です． i : σ が与えられた時，対応する多項式は MvPolynomial.X i です．（いつものように， MVPolynomial 名前空間を開くことでこれを X i と短縮することができます．）例えば，2つの不定元が欲しい場合， Fin 2 を σ として使い， \(\mathbb{R}^2`\) の単位円を定義する多項式を次のように書くことができます．
open MvPolynomial
def circleEquation : MvPolynomial (Fin 2) ℝ := X 0 ^ 2 + X 1 ^ 2 - 1
関数の適用は非常に高い優先度を持つため，上の式は (X 0) ^ 2 + (X 1) ^ 2 - 1 と読めることを思い出してください．これを評価して座標 \((1, 0)\) の点が円上にあることを確認することができます．この ![...] 記法は，引数の数によって決まる自然数 n と引数の型によって決まる X の Fin n → X の要素を表すことを思い出してください．
example : MvPolynomial.eval ![0, 1] circleEquation = 0 := by simp [circleEquation]