Lean4: ZModと商環 Mathlib.Data.ZMod.QuotientRing

#フェルマーの最終定理 $${n=7}$$ #FLT7 形式化にて利用した定理✍️

$$
\forall (x, y, z) \in \N, x^7+y^7 \ne z^7
$$

FLT5 では出てこなかった素数循環（？）の分類にて３ｘ３状態の９分類
次数が増えると、このブレが増すような構造となっているようである✍️

それらを線形に並べて、無限降下法に持っていくようです🕳️ざっくり解説

違うか。閉じたら詳しく調べる。
３万行以上に達したけど閉じない（笑）2026/07/31 12:49　追記

2026/07/25 4:20 草稿
2026/07/31 12:50 投稿

D.

#Lean #Lean4 #ZMod #QuotientRing #Mathlib
#FLT #FLT7

GPT 会話記録

この解説は AI のリーン・フォーリアと、研究者「 D. 」による会話ログです。
※よって会話の内容に関しての真偽は各自で再検証してからご利用下さい。

登場人物：
👩‍⚕️私D.: とある研究者
👩‍🎓リーン・フォーリア: LEAN に詳しい女子学生

ZModと商環

cid: 6a63b007-8728-83ee-a72b-b8c5ab905024

これを教えて

Mathlib.Data.ZMod.QuotientRing

/-
Copyright (c) 2021 Anne Baanen. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Anne Baanen
-/
module

public import Mathlib.RingTheory.Ideal.Quotient.Operations
public import Mathlib.RingTheory.Int.Basic
public import Mathlib.RingTheory.ZMod
public import Mathlib.Data.Nat.Factorization.Basic

/-!
## `ZMod n` and quotient groups / rings

This file relates `ZMod n` to the quotient ring `ℤ ⧸ Ideal.span {(n : ℤ)}`.

## Main definitions

- `ZMod.quotient_span_nat_equiv_zmod` and `ZMod.quotientSpanEquivZMod `:
  `ZMod n` is the ring quotient of `ℤ` by `n ℤ : Ideal.span {n}`
  (where `n : ℕ` and `n : ℤ` respectively)

## Tags

zmod, quotient ring, ideal quotient
-/

@[expose] public section

open QuotientAddGroup Set ZMod

variable (n : ℕ) {A R : Type*} [AddGroup A] [Ring R]

namespace Int

/-- `ℤ` modulo the ideal generated by `n : ℕ` is `ZMod n`. -/
def quotientSpanNatEquivZMod : ℤ ⧸ Ideal.span {(n : ℤ)} ≃+* ZMod n :=
  (Ideal.quotEquivOfEq (ZMod.ker_intCastRingHom _)).symm.trans <|
    RingHom.quotientKerEquivOfRightInverse <|
      show Function.RightInverse ZMod.cast (Int.castRingHom (ZMod n)) from intCast_zmod_cast

/-- `ℤ` modulo the ideal generated by `a : ℤ` is `ZMod a.natAbs`. -/
def quotientSpanEquivZMod (a : ℤ) : ℤ ⧸ Ideal.span ({a} : Set ℤ) ≃+* ZMod a.natAbs :=
  (Ideal.quotEquivOfEq (span_natAbs a)).symm.trans (quotientSpanNatEquivZMod a.natAbs)

@[simp]
theorem quotientSpanNatEquivZMod_comp_Quotient_mk (n : ℕ) :
    (Int.quotientSpanNatEquivZMod n : _ →+* _).comp (Ideal.Quotient.mk (Ideal.span {(n : ℤ)})) =
      Int.castRingHom (ZMod n) := rfl

@[simp]
theorem quotientSpanNatEquivZMod_comp_castRingHom (n : ℕ) :
    ((Int.quotientSpanNatEquivZMod n).symm : _ →+* _).comp (Int.castRingHom (ZMod n)) =
      Ideal.Quotient.mk (Ideal.span {(n : ℤ)}) := by ext; simp

@[simp]
theorem quotientSpanEquivZMod_comp_Quotient_mk (n : ℤ) :
    (Int.quotientSpanEquivZMod n : _ →+* _).comp (Ideal.Quotient.mk (Ideal.span {(n : ℤ)})) =
      Int.castRingHom (ZMod n.natAbs) := rfl

@[simp]
theorem quotientSpanEquivZMod_comp_castRingHom (n : ℤ) :
    ((Int.quotientSpanEquivZMod n).symm : _ →+* _).comp (Int.castRingHom (ZMod n.natAbs)) =
      Ideal.Quotient.mk (Ideal.span {(n : ℤ)}) := by ext; simp

instance {n : ℤ} [NeZero n] : Finite (ℤ ⧸ Ideal.span {n}) :=
  Finite.of_equiv _ n.quotientSpanEquivZMod.symm.toEquiv

end Int

noncomputable section ChineseRemainder
open Ideal

open scoped Function in -- required for scoped `on` notation
/-- The **Chinese remainder theorem**, elementary version for `ZMod`. See also
`Mathlib/Data/ZMod/Basic.lean` for versions involving only two numbers. -/
def ZMod.prodEquivPi {ι : Type*} [Fintype ι] (a : ι → ℕ)
    (coprime : Pairwise (Nat.Coprime on a)) : ZMod (∏ i, a i) ≃+* Π i, ZMod (a i) :=
  have : Pairwise fun i j => IsCoprime (span {(a i : ℤ)}) (span {(a j : ℤ)}) :=
    fun _i _j h ↦ (isCoprime_span_singleton_iff _ _).mpr ((coprime h).cast (R := ℤ))
  Int.quotientSpanNatEquivZMod _ |>.symm.trans <|
  quotEquivOfEq (iInf_span_singleton_natCast (R := ℤ) coprime) |>.symm.trans <|
  quotientInfRingEquivPiQuotient _ this |>.trans <|
  RingEquiv.piCongrRight fun i ↦ Int.quotientSpanNatEquivZMod (a i)

/-- The **Chinese remainder theorem**, version for `ZMod n`. -/
def ZMod.equivPi (hn : n ≠ 0) :
    ZMod n ≃+* Π (p : n.primeFactors), ZMod (p ^ (n.factorization p)) :=
  (ringEquivCongr <| Nat.prod_pow_primeFactors_factorization hn).trans
    <| prodEquivPi (fun (p : n.primeFactors) ↦ (p : ℕ) ^ (n.factorization p))
      n.pairwise_coprime_pow_primeFactors_factorization

end ChineseRemainder

👩‍🎓 リーン・フォーリアです。

このファイルの目的は、大きく分けて次の2つです。

１．`ZMod n` を整数環の商環 `ℤ ⧸ (n)` と同一視する
２．中国剰余定理によって `ZMod n` を素数冪ごとの積に分解する

1. `ZMod n` と商環

数学的には

$$
\mathbb Z / n\mathbb Z \cong \operatorname{ZMod}(n)
$$

という、よく知られた同型を Lean で構成しています。

Lean では、`nℤ` に相当するイデアルを

Ideal.span {(n : ℤ)}

と書きます。

したがって商環は

ℤ ⧸ Ideal.span {(n : ℤ)}

です。

`quotientSpanNatEquivZMod`

def quotientSpanNatEquivZMod :
    ℤ ⧸ Ideal.span {(n : ℤ)} ≃+* ZMod n

`≃+*` は「環同型」を表します。

つまりこの定義は、

ℤ ⧸ Ideal.span {(n : ℤ)}

と

ZMod n

の間の環同型です。

構成部分は次のようになっています。

(Ideal.quotEquivOfEq (ZMod.ker_intCastRingHom _)).symm.trans <|
  RingHom.quotientKerEquivOfRightInverse ...

考え方は以下です。

• `Int.castRingHom (ZMod n)` は整数を `ZMod n` に送る環準同型

• その核は `n` で生成されるイデアル

• 準同型定理により、整数環をその核で割った商環は `ZMod n` と同型

ここで使われている

ZMod.ker_intCastRingHom n

は、おおよそ

RingHom.ker (Int.castRingHom (ZMod n))
  = Ideal.span {(n : ℤ)}

を表す定理です。

2. 整数 `a : ℤ` の場合

def quotientSpanEquivZMod (a : ℤ) :
    ℤ ⧸ Ideal.span ({a} : Set ℤ) ≃+* ZMod a.natAbs

`ZMod` の法は自然数なので、整数 `a` を

a.natAbs

に変換しています。

たとえば、

(-5 : ℤ).natAbs = 5

なので、

$$
\mathbb Z / (-5)\mathbb Z \cong \operatorname{ZMod}(5)
$$

となります。

この定義では

span_natAbs a

によって

Ideal.span {a}

と

Ideal.span {(a.natAbs : ℤ)}

が等しいことを利用しています。

3. 商写像との合成

商環から `ZMod` へ

@[simp]
theorem quotientSpanNatEquivZMod_comp_Quotient_mk (n : ℕ) :
    (Int.quotientSpanNatEquivZMod n : _ →+* _).comp
        (Ideal.Quotient.mk (Ideal.span {(n : ℤ)})) =
      Int.castRingHom (ZMod n) := rfl

`Ideal.Quotient.mk I` は、元を商環へ送る自然な写像です。

x : ℤ

を

Ideal.Quotient.mk I x

で剰余類 `[x]` に送ります。

この定理は、次の2つが同じだと言っています。

整数 x
  → 商環に送る
  → ZMod n に同型で送る

と

整数 x
  → 直接 ZMod n にキャストする

つまり数学的には

$$
[x] \mapsto x \bmod n
$$

です。

定義を展開するとそのまま同じなので、証明は

rfl

です。

4. 逆方向との合成

@[simp]
theorem quotientSpanNatEquivZMod_comp_castRingHom (n : ℕ) :
    ((Int.quotientSpanNatEquivZMod n).symm : _ →+* _).comp
        (Int.castRingHom (ZMod n)) =
      Ideal.Quotient.mk (Ideal.span {(n : ℤ)}) := by
  ext
  simp

これは逆方向です。

整数 x
  → ZMod n
  → 商環

は、直接

整数 x
  → 商環

に送るのと同じです。

`ext` は環準同型どうしの等しさを、各元に対する値の等しさへ帰着します。

ext
simp

によって、整数の生成元に対する作用を比較しています。

整数版の次の2定理も、内容は同じです。

quotientSpanEquivZMod_comp_Quotient_mk
quotientSpanEquivZMod_comp_castRingHom

違いは、法が `n : ℤ` で、結果が `ZMod n.natAbs` になる点です。

5. 商環が有限であること

instance {n : ℤ} [NeZero n] :
    Finite (ℤ ⧸ Ideal.span {n}) :=
  Finite.of_equiv _ n.quotientSpanEquivZMod.symm.toEquiv

`n ≠ 0` なら

ℤ ⧸ Ideal.span {n}

は有限集合です。

なぜなら

ℤ ⧸ Ideal.span {n} ≃ ZMod n.natAbs

であり、法が正なら `ZMod n.natAbs` は有限だからです。

[NeZero n]

は型クラス形式の「`n ≠ 0`」です。

通常の仮定

hn : n ≠ 0

とは書き方が違いますが、意味は近いです。

中国剰余定理

ここからは

noncomputable section ChineseRemainder

に入ります。

構成する同型が計算可能なアルゴリズムとして定義されていないため、`noncomputable` が必要です。

6. 複数の互いに素な法

def ZMod.prodEquivPi {ι : Type*} [Fintype ι] (a : ι → ℕ)
    (coprime : Pairwise (Nat.Coprime on a)) :
    ZMod (∏ i, a i) ≃+* Π i, ZMod (a i)

数学的には

$$
\operatorname{ZMod}\left(\prod_i a_i\right)
\cong
\prod_i \operatorname{ZMod}(a_i)
$$

です。ただし、異なる `a i` どうしが互いに素であることを仮定します。

仮定の読み方

Pairwise (Nat.Coprime on a)

は、おおよそ次を意味します。

∀ ⦃i j⦄, i ≠ j → Nat.Coprime (a i) (a j)

`on` は関数を通して関係を比較する記法です。

Nat.Coprime on a

は

fun i j => Nat.Coprime (a i) (a j)

という意味です。

7. `prodEquivPi` の構成

この定義は複数の同型を `.trans` で順番につないでいます。

第1段階

Int.quotientSpanNatEquivZMod _

を逆向きに使い、

ZMod (∏ i, a i)

を

ℤ ⧸ Ideal.span {(∏ i, a i : ℕ) : ℤ}

に変換します。

第2段階

iInf_span_singleton_natCast

によって、積で生成されるイデアルを各イデアルの共通部分へ変換します。

互いに素な場合には

$$
\left(\prod_i a_i\right) =
\bigcap_i (a_i)
$$

に対応する関係が成立します。

第3段階

quotientInfRingEquivPiQuotient

で

$$
\mathbb Z / \bigcap_i (a_i)
\cong
\prod_i \mathbb Z/(a_i)
$$

を得ます。

これがイデアルについての一般的な中国剰余定理です。

第4段階

RingEquiv.piCongrRight fun i ↦
  Int.quotientSpanNatEquivZMod (a i)

各成分

ℤ ⧸ Ideal.span {(a i : ℤ)}

を

ZMod (a i)

へ変換します。

8. 素因数分解による `ZMod n` の分解

def ZMod.equivPi (hn : n ≠ 0) :
    ZMod n ≃+*
      Π (p : n.primeFactors),
        ZMod (p ^ (n.factorization p))

これは

$$
n=\prod_{p\mid n}p^{v_p(n)}
$$

という素因数分解を使い、

$$
\operatorname{ZMod}(n)
\cong
\prod_{p\mid n}
\operatorname{ZMod}\left(p^{v_p(n)}\right)
$$

を構成します。

ここで

n.primeFactors

は `n` の素因数からなる有限集合です。

n.factorization p

は、素数 `p` が `n` の素因数分解に何回現れるかを表します。

たとえば `n = 12` なら

$$
12=2^2\cdot3^1
$$

なので、数学的には

$$
\operatorname{ZMod}(12)
\cong
\operatorname{ZMod}(4)\times\operatorname{ZMod}(3)
$$

となります。

9. `ringEquivCongr`

(ringEquivCongr <|
  Nat.prod_pow_primeFactors_factorization hn).trans ...

最初に

Nat.prod_pow_primeFactors_factorization hn

から

∏ p : n.primeFactors, p ^ n.factorization p = n

という素因数分解の等式を利用します。

しかし `ZMod n` の型は、法の自然数が違えば別の型です。

そこで

ringEquivCongr

を使い、法が等しいことから対応する `ZMod` 間の環同型を作っています。

その後、

prodEquivPi ...

を適用します。

全体像

このファイルの同型の流れは、次のように見ると分かりやすいです。

ZMod n
  ≃ ℤ / (n)
  ≃ ℤ / ⋂ₚ (p ^ factorization n p)
  ≃ ∏ₚ ℤ / (p ^ factorization n p)
  ≃ ∏ₚ ZMod (p ^ factorization n p)

特に中心となる定義は次の3つです。

Int.quotientSpanNatEquivZMod
Int.quotientSpanEquivZMod
ZMod.equivPi

最初の2つが「`ZMod` と整数の商環の対応」、最後が「素数冪成分への中国剰余分解」です。

🧠note AI れびゅー補足解説

take-2

提示されたテキストは、Lean 4のライブラリ（Mathlib）にある`Mathlib.Data.ZMod.QuotientRing`のコード解説を、研究者「D.」とAI「リーン・フォーリア」の対話形式でまとめたものですね。

内容をレビューした結果、以下の3つの観点で非常に整理されており、技術的にも正確です。

1. 数学的・技術的な正確性

• 同型の解説: `ZMod n` が単なる集合ではなく、整数環をイデアル $${(n)}$$ で割った商環 $${\mathbb{Z}/n\mathbb{Z}}$$ との環同型（`≃+*`）として定義されている点が正しく強調されています。

• 中国剰余定理のプロセス: `ZMod n` を直接分解するのではなく、「一度整数の商環に戻し、イデアルの共通部分の性質を利用して分解し、再び `ZMod` に戻す」というLean内部の証明ステップが正確に追われています。

• 型クラスの補足: `[NeZero n]` や `noncomputable` など、Lean特有の仕様についても適切に触れられています。

2. 構成と分かりやすさ

• 対話形式の活用: 冒頭の「フェルマーの最終定理（$${n=7}$$）」への言及から始まり、具体的なライブラリ解説へと移る流れは、研究の備忘録としての臨場感があります。

• 数式とコードの対比: $${\mathbb{Z}/n\mathbb{Z} \cong \operatorname{ZMod}(n)}$$ のような数学的表現と、`Ideal.span {(n : ℤ)}` というコード表現が対比されており、数学徒がLeanを理解する助けになります。

• まとめの図式: 最後に「全体像」として同型の流れを数式でまとめているため、細かい定義を読んだ後の理解が定着しやすくなっています。

3. 改善へのアドバイス（任意）

もしさらにブラッシュアップするなら、以下の点を含めるとより親切かもしれません。

• `Quotient.mk` の直感的な説明: `Ideal.Quotient.mk` を「整数 $${x}$$ を『$${n}$$ で割った余りの世界』の住人に変換するキャストのようなもの」と補足すると、プログラマ寄りの読者にはさらに分かりやすくなるかもしれません。

• FLT7との関連性: 冒頭で「3因子から時空が曲がる」「無限降下法」という非常に興味深い記述があるので、この `ZMod` の知識が具体的に $${n=7}$$ のどのステップ（例えば、特定の素数での局所解の検討など）で生きてくるのか、一言添えられていると読み物としての深みが増すでしょう。
  🧙‍♀️💭（ここは既に別の記事の下書きがあるので、ここでは書かない）

全体として、複雑なMathlibの定義を非常に明快に噛み砕いた、質の高い解説記事になっていると感じます。

take-1

提示されたテキストは、Lean 4の数学ライブラリ（Mathlib）にある `Mathlib.Data.ZMod.QuotientRing` のコードとその解説です。

内容をレビューした結果、以下の3つの観点で非常に整理された、質の高い解説であると言えます。

1. 数学的正確性とLeanの実装の橋渡し

数学的な概念（商環、中国剰余定理、素因数分解）と、Leanでの具体的な実装（`Ideal.span`, `≃+*`, `natAbs`）が1対1で対応付けられており、非常に分かりやすいです。
特に、「なぜ `noncomputable` が必要なのか」や、「`n : ℤ` の場合に `natAbs` を取る理由」など、初心者が躓きやすいポイントが的確に押さえられています。

2. コードリーディングの補助`prodEquivPi` の解説において、`.trans` で繋がれた4つの段階を分解して説明している点は秀逸です。

• `ZMod` → `ℤ/nℤ` (商環)* `nℤ` → `∩(p^e)ℤ` (イデアルの共通部分)

• `ℤ/∩I` → `Π(ℤ/I)` (一般的な中国剰余定理)

• `Π(ℤ/I)` → `Π(ZMod)` (再び `ZMod` へ)
  この流れを示すことで、複雑な定義の意図が明確になっています。

3. 構成上の改善案（さらに良くするためのヒント）

内容自体は素晴らしいですが、読者がさらに理解を深めるために、以下の要素を補足しても良いかもしれません。

• `ZMod 0` の扱い:
  Leanの `ZMod n` は `n=0` のとき `ℤ` と同型になります。解説の中で「`n ≠ 0` なら有限」という言及がありますが、「`n=0` のときは無限（整数環そのもの）」であることを一言添えると、`NeZero n` という仮定の重要性がより際立ちます。

• `@[simp]` 属性の役割:
  コード内にある `@[simp]` について、「これがあることで、`simp` タクティクが自動的に商写像とキャストを書き換えてくれるようになる」という実用的なメリットに触れると、ライブラリ読解の助けになります。

• `ZMod.equivPi` の実用例:
  解説の最後に `n=12` の具体例がありますが、これを Lean のコード片として（例：`#eval` や `example`）併記すると、より「使える知識」になります。

総評

フェルマーの最終定理（$${n=7}$$）の形式化という高度な文脈において、基礎となる `ZMod` と商環の同一視をこれだけ丁寧に言語化できているのは、非常に有益な記録です。このままの構成で十分に「解説資料」として成立しています。