7. 階層構造

Chapter 6 では群のクラスを定義し，このクラスのインスタンスを構築する方法，そして可換環クラスのインスタンスを構築する方法について見てきました．しかしもちろんこのような構造間には階層があります: 特に可換環は加法群です．この章では，このような階層の作り方を学んでいきます．このような階層は数学のあらゆる分野に現れますが，この章では代数的な例に重点を置きます．

Leanにもうすでに定義されている階層構造の使い方を学ぶ前に，階層の作り方について議論するのは時期尚早と思われるかもしれません．しかし，階層を使用するためには，階層の基礎となる技術をある程度理解する必要があります．そのため，この章は読むべきではあります，が初見ですべてを覚えようと頑張りすぎず，次の章を読んでからもう一度ここに戻って読むとよいでしょう．

この章では，Mathlibに登場する多くの階層を（簡易的に）再定義するため，添え字を用いてMathlibのものと区別します．例えば， Ring に対して，以下では Ring₁ として定義します．構造の形式化について順を追って強力な方法を説明していくので，これらの添え字は1より大きくなることがあります．

7.1. 基礎

Leanのすべての階層の一番下にはデータを格納するためのクラスが存在します．次のクラスは与えられた型 α が one という名前で識別される要素を保持します．この段階ではこのクラスはなんの性質も持ちません．

class One₁ (α : Type) where
  /-- The element one -/
  one : α

この章ではクラスを頻繁に使用するため， class コマンドが何を行っているか，もう少し詳しく理解する必要があります．まず，上記の class コマンドは， α : Type をパラメータとし，1つのフィールド one を持つ構造体 One₁ を定義します．また，この構造体をクラスとしてマークすることで，ある型 α に対する One₁ α 型の引数は，暗黙のインスタンスとしてマークされている限り，つまり角括弧の間に表示されている限り，インスタンスを解決する手順を使用して推論できるようになります．この2つの効果は structure コマンドで class 属性を指定することで実現することもできます．つまり， @[class] structure のように記述するのです．しかし，classコマンドは， One₁ α が自身のフィールドの暗黙のインスタンスの引数として現れることを保証します．以下の例と比べてみましょう:

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

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

#check One₂.one

2つ目のチェックでは， self : One₂ α が明示的な引数となっていることがわかります．最初のバージョンが本当に明示的な引数なしで使えるか確認してみましょう．

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

注意: 上記の例では，引数 One₁ α を暗黙のインスタンスとしてマークしていますが，これは宣言を する ことにのみ影響し， example コマンドで作成された宣言は使うことができないため少し馬鹿げています．しかし，これによりその引数に名前を避けることができ，さらに重要なことは One₁ α 引数を暗黙のインスタンスとしてマークする良い習慣を身につけ始めることができるでしょう．

もう一つの注意点は，Leanが α がなんであるかを知っている場合にのみ，この操作は機能するという点です．上の例で型アスクリプション : α を省略すると typeclass instance problem is stuck, it is often due to metavariables One₁ (?m.263 α) というようなエラーメッセージが表示されます．ここで ?m.263 α は「 α に依存する何らかの型」を意味します．（263は単に自動生成されたインデックスで，未知のものを区別するのに便利です）この問題を避けるもう一つの方法は，次のように型注釈を使うことです:

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

Section 3.6 で数列の極限の話題において，例えば 0 < 1 を述べようとする際にこの不等式が自然数に関するものなのか実数に関するものなのかLeanに明示していなかった場合，すでにこの問題に遭遇しているかもしれません．

次の目標は One₁.one に記法を割り当てることです．ここでは組み込みの 1 の表記と衝突したくないため， 𝟙 を使用します．これは以下のコマンドで実現されます．1行目ではLeanに One₁.one に関する情報を 𝟙 に関するものとして使用するように指示しています．

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

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

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

次に二項演算を保持するデータ用のクラスを考えてみましょう．現時点では加算と乗算のどちらかを選びたくないため，ひし形を使うことにします．

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

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

One₁ の例と同様に，この演算はこの段階ではなんの性質も持ちません．ここで ⋄ で表現される演算を半群構造のクラスとして定義してみましょう．これにあたってとりあえず， Dia₁ のインスタンスと ⋄ の結合性を保証する Prop -値のフィールド dia_assoc の2つのフィールドを持つ構造体として定義します．

class Semigroup₁ (α : Type) where
  toDia₁ : Dia₁ α
  /-- Diamond is associative -/
  dia_assoc : ∀ a b c : α, a ⋄ b ⋄ c = a ⋄ (b ⋄ c)

dia_assoc を記述する際に，これより上に定義しているフィールド toDia₁ はここでのローカルな文脈にあるため，Leanが Dia₁ α のインスタンスを検索してくれるようになることで，Leanが a ⋄ b の意味を解釈してくれます．しかし，この toDia₁ フィールドは型クラスのインスタンスの情報のデータベースには取り込まれません．したがって， example {α : Type} [Semigroup₁ α] (a b : α) : α := a ⋄ b を実行すると， failed to synthesize instance Dia₁ α というエラーメッセージが表示されて失敗してしまいます．

この問題は後から instance 属性を追加することで解決できます．

attribute [instance] Semigroup₁.toDia₁

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

半群構造を組み上げる前に， toDia₁ のようなフィールドを明示的に記述してインスタンス属性を手で追加するよりも便利な方法で構造体を拡張する方法がほしいところです． class は extends 記法を使ってこれをサポートします:

class Semigroup₂ (α : Type) extends Dia₁ α where
  /-- Diamond is associative -/
  dia_assoc : ∀ a b c : α, a ⋄ b ⋄ c = a ⋄ (b ⋄ c)

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

この構文は structure コマンドでも利用出来ますが，その場合は定義するインスタンスがないため， toDia₁ のようなフィールドを記述する手間を改善するだけです．

さて，ひし形の演算子と区別された1がこの演算子の両サイドで中立となるという公理を組み合わせてみましょう．

class DiaOneClass₁ (α : Type) extends One₁ α, Dia₁ α where
  /-- One is a left neutral element for diamond. -/
  one_dia : ∀ a : α, 𝟙 ⋄ a = a
  /-- One is a right neutral element for diamond -/
  dia_one : ∀ a : α, a ⋄ 𝟙 = a

次の例では， α が DiaOneClass₁ 構造を持つことをLeanに伝え， Dia₁ インスタンスと One₁ インスタンスの両方を使用するプロパティを定めます．Leanがこれらのインスタンスをどのように見つけるかを観察できるように，トレースオプションを設定しています．これで出力されるようになる結果は既定ではかなり簡潔ですが，黒い矢印で終わる行をクリックすることで詳細が展開されます．この中にはLeanがインスタンスの検索を成功するために十分な型情報を得る前に検索を行って失敗した結果もふくまれます．

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

既存のクラスを組み合わせる際に，余分なフィールドを含める必要はないことに注意しましょう．したがって，モノイドを次のように定義することができます．

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

上記の定義は簡単なように見える一方，微妙ですが重要な点が隠されています． Semigroup₁ α と DiaOneClass₁ α のどちらも Dia₁ α を拡張しているので， Monoid₁ α のインスタンスを持つと， α に対して，1つは Monoid₁.toSemigroup₁ から，そしてもう1つは Monoid₁.toDiaOneClass₁ からと2つの無関係なひし形演算が生じてしまうのではないかという懸念が出てきます．

実際，モノイドクラスを明示的に手で作ろうとすると以下のようになります:

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

したがって全く関係のない2つのひし形演算 Monoid₂.toSemigroup₁.toDia₁.dia と Monoid₂.toDiaOneClass₁.toDia₁.dia が得られます．

しかし extends 構文を使って生成されたバージョンにはこの欠陥はありません．

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

つまり class コマンドは私達のためにいくつかの魔法を使ってくれているのです．（そして structure コマンドでも同様でしょう）クラスのフィールドを確認する簡単な方法は，コンストラクタをチェックすることです．以下の2つを比較してみましょう:

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

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

つまり， Monoid₁ は期待される通り Semigroup₁ α を引数として取りますが，重複するはずの DiaOneClass₁ α を引数として取らず，代わりにそれをバラバラにして重複市内部分のみを含めるようにしていることがわかります．また，インスタンス Monoid₁.toDiaOneClass₁ も自動生成されました．これはフィールドではありませんが，利用者から見て2つの拡張クラス Semigroup₁ と DiaOneClass₁ の間の対称性を保存することが期待されるはずで，これに対応した型注釈を持ちます．

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

これで群の定義にかなり近づきました．群にするために，モノイド構造のすべての元に逆元が存在することを保証するフィールドを追加することもできます．しかし，そうするとこれらの逆元にアクセスするための作業が必要になります．実際にはデータとして追加するほうが便利です．再利用性を高めるために，新しいデータ保持クラスを定義し，それにいくつかの表記法を与えることとします．

class Inv₁ (α : Type) where
  /-- The inversion function -/
  inv : α → α

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

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

上記の定義では a⁻¹ が a の左逆であることのみを要求しているため，弱すぎるように思えるかもしれません．しかし，もう一方の逆は自動的に求まります．それを証明するためには別で補題を用意する必要があります．

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

この補題の証明で使っている各事実にはどの階層からのものかを知っておく必要があるため，各事実のフルネームを与えるのはかなり面倒です．これを解決する1つの方法は export コマンドを使ってこれらの事実をルートの名前空間に補題としてコピーすることです．

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

これにより上記の証明を次のように書き換えることができます:

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

次はここまで構築してきた代数的構造について読者が証明を行う番です．

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

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

この段階で環の定義に進みたいところですが，重大な問題が残っています．型上の環構造には加法群構造と乗法モノイド構造の両方がふくまれ，それらの相互作用についていくつかの性質があります．しかし，ここまですべての演算に ⋄ という表記法をハードコードしてしまっています．より基本的な事実として，型クラスシステムはすべての方がそれぞれの型クラスのインスタンスを1つだけ持っていると仮定します．この問題には多くの解決法があります．意外なことに，Mathlibは加法と乗法の理論のすべてを何らかのコード生成されたものを複製するという素朴な方法を採用しています．構造体やクラスは加法・乗法の両方で定義され，属性 to_additive がそれらをリンクします．半群のような多重継承の場合，自動生成される「対称性を保存する」インスタンスにもマークする必要があります．これは少し専門的な話なので，詳細を理解する必要はありません．重要な点は，補題は乗法の記法でのみ記述され， to_additive 属性をマークすることで加法バージョンを自動生成します．例えば left_inv_eq_right_inv' の自動生成される加法バージョンは version left_neg_eq_right_neg' です．この追加バージョンの名前を確認するために， left_inv_eq_right_inv' の上で whatsnew in コマンドを使用しました．

class AddSemigroup₃ (α : Type) extends Add α where
/-- Addition is associative -/
  add_assoc₃ : ∀ a b c : α, a + b + c = a + (b + c)

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

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

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

attribute [to_additive existing] Monoid₃.toMulOneClass

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

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

#check left_neg_eq_right_neg'

この技術を使えば，可換半群，モノイド，群も簡単に定義でき，環も定義できます．

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

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

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

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

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

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

適切な場合には補題に simp タグをつけることを覚えておきましょう．

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

ひし形演算子から標準的な表記に切り替えたため，ここから少し今までやったことを繰り返す必要がありますが，少なくとも to_additive によって乗法表記から加法表記への変換を行ってくれます．

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

なお， to_additive は以下のように補題に simp タグを付け，その属性を加法バージョンに伝搬させるために使うことができます．

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

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

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

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

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

これで環のための準備が整いました．ここでは階層構造の実演が目的なので，足し算が可換であると仮定してすぐに AddCommGroup₃ のインスタンスを提供することはしません．Mathlibでもこのような方針はとりません．第一に，実際にはどの環のインスタンスも簡単なものにならず，またMathlibの代数階層は環と似ていますが加法の逆元のない半環を通るため，以下の証明が機能しないからです．ここで得られるものは，これらの代数構造を見たことがない人にとってのいい練習となること以外にも，親構造といくつかの追加フィールドを提供できる構文を使ったインスタンス構築の例を見られることです．

class Ring₃ (R : Type) extends AddGroup₃ R, Monoid₃ R, MulZeroClass R where
  /-- Multiplication is left distributive over addition -/
  left_distrib : ∀ a b c : R, a * (b + c) = a * b + a * c
  /-- Multiplication is right distributive over addition -/
  right_distrib : ∀ a b c : R, (a + b) * c = a * c + b * c

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

もちろん整数上の環構造などの具体的なインスタンスを構築することもできます．（と言いつつ以下のインスタンスではMathlibですでに定義されているものを使っているだけですが．）

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

ここまで理解できたなら半順序と ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b のような可換モノイド構造を持つ順序付けられた可換モノイドを含む簡単な順序関係の構築は良い演習となるでしょう．これにあたってはもちろん以下のクラスをそのまま使うのではなく，いくつかのフィールドや，場合によっては extends 節を追加する必要があります．

class LE₁ (α : Type) where
  /-- The Less-or-Equal relation. -/
  le : α → α → Prop

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

class Preorder₁ (α : Type)

class PartialOrder₁ (α : Type)

class OrderedCommMonoid₁ (α : Type)

instance : OrderedCommMonoid₁ ℕ where

ここで複数の型から構成される代数的構造について議論したいと思います．代表的なものは環上の加群です．もし加群が何かを知らない場合，これはベクトル空間のことを指し，ここで環としたものがベクトル空間では体だと考えておくといいでしょう．これらの構造は，ある環の要素によるスカラー倍を備えた可換加法群です．

まず，ある型 β 上のある型 α によるスカラー倍の計算を保持する型クラスを定義し，これに右に結合する記法を割り当てます．

class SMul₃ (α : Type) (β : Type) where
  /-- Scalar multiplication -/
  smul : α → β → β

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

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

ここでは興味深い書き方がされています．この定義において R 上の環構造がパラメータであることはそれほど驚くことではありませんが，おそらく SMul₃ R M と同じように AddCommGroup₃ M も extends 節の一部になると思われたのではないでしょうか？試しにそのようにすると次のような謎めいたエラーメッセージが表示されます： cannot find synthesization order for instance Module₁.toAddCommGroup₃ with type (R : Type) → [inst : Ring₃ R] → {M : Type} → [self : Module₁ R M] → AddCommGroup₃ M all remaining arguments have metavariables: Ring₃ ?R @Module₁ ?R ?inst✝ M ．このメッセージを理解するためには，このような extends 節は，インスタンスとしてマークされたフィールド Module₃.toAddCommGroup₃ を導入することを思い出しましょう．このインスタンスはエラーメッセージに表示されている (R : Type) → [inst : Ring₃ R] → {M : Type} → [self : Module₁ R M] → AddCommGroup₃ M という型注釈を持ちます．型クラスのデータベースにこのようなインスタンスがある場合，Leanは M に対して AddCommGroup₃ M インスタンスを探すたびに，メインである Module₁ R M インスタンスの探索を行う前に，完全に未指定の型 R と Ring₃ R インスタンスを探しに行く必要があります．この2つの副次的な探索はエラーメッセージにて ?R と ?inst✝ で示されるメタ変数として言及されます．この Module₃.toAddCommGroup₃ のようなインスタンスはインスタンス解決プロセスにおいて大きな罠となり， class コマンドはこのクラスの設定を拒否します．

では extends SMul₃ R M はどうでしょうか？これは Module₁.toSMul₃ : {R : Type} →  [inst : Ring₃ R] → {M : Type} → [inst_1 : AddCommGroup₃ M] → [self : Module₁ R M] → SMul₃ R M というフィールドを作りますが，最終的な SMul₃ R M で R と M の両方に言及しているためこのフィールドはインスタンスとして安全に使うことができます．このルールを覚えるのは簡単です． extends 節に登場する各クラスは，パラメータに登場するすべての型に言及しなければならないのです．

加群のインスタンスの1つ目を作成しましょう．環は，スカラー倍として乗算を使用するそれ自体の上の加群です．

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

第二の例として，すべてのアーベル群は ℤ 上の加群となります．（これは非可逆なスカラーを許容することでベクトル空間の理論を一般化するための理由の1つです）まず，0と加法を備えた任意の型への整数によるスカラー倍を定義します．ここで n • a は a が n 回現れる a + ⋯ + a として定義されます．ついで (-1) • a = -a を保証することで整数によるスカラー倍に拡張されます．

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

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

これが加群構造を生むことを証明するのは少々面倒で，また今の議論においては面白くないのですべての公理をsorryとします．これらのsorryは 演習問題ではありません ．もしどうしてもこれらのsorryを証明に置き換えたいのであれば， nsmul₁ と zsmul₁ に関するいくつかの中間的な補題を用意してから証明することになるでしょう．

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

より重要な問題は，環 ℤ は自身について2つの加群構造があるということです． abGrpModule ℤ は ℤ がアーベル群であること，そして selfModule ℤ は ℤ が環であることによる加群のインスタンスです．これら2つの加群構造は同じアーベル群構造に対応しますが，スカラー倍が同じであることは自明ではありません．実際には同じなのですが，これは定義上は真ではなく，証明が必要です．これは型クラスのインスタンス解決プロセスにとって非常に悪いニュースであり，この階層を利用するユーザーにとって非常にいらいらする失敗に繋がります．直接インスタンスを見つけることを要求すると，Leanは何か1つ選んできて，それが以下であることを確認できます．

#synth Module₁ ℤ ℤ -- abGrpModule ℤ

しかし，より間接的な文脈では，Leanはこのインスタンスを推測するため，混乱を生じることがあります．このような状況は悪いダイアモンドとして知られています．これは上記で使用したひし形演算子とは関係ないもので， ℤ から Module₁ ℤ への道を AddCommGroup₃ ℤ か Ring₃ ℤ のどちらをも経由できてしまうことを指します．

すべてのダイアモンドが悪いわけではないことを理解することが重要です．実際，Mathlibにはいたるところにダイアモンドがあり，この章にもダイアモンドがあります．すでに冒頭で Monoid₁ α から Semigroup₁ α または DiaOneClass₁ α のどちらかを経由して Dia₁ α に行くことができ， class コマンドのおかげで結果として得られる2つの Dia₁ α インスタンスが定義上等しいことを見ました．特に，一番下に Prop 値のクラスを持つダイアモンドは，同じ文の証明が定義上等しくなることから悪いダイアモンドとなることはありません．

しかし加群で作ったダイアモンドは間違いなく悪いものです．問題なのは証明ではなくデータである smul フィールドで，2つの定義的に等しくない構成を持つことに成ります．この問題を解決する確実な方法は，豊かな構造から貧しい構造への移行がデータの定義によってではなく常にデータを忘れることによって行われることを自覚することです．このよく知られたパターンは「忘却継承」と名付けられ， https://inria.hal.science/hal-02463336 で広く議論されています．

今回のケースでは， AddMonoid₃ の定義を変更して， nsmul データフィールドと，この演算が上記で構成した証明可能なものであることを保証するいくつかの Prop 値フィールドを含めるように修正することができます．これらのフィールドは以下の定義で型の後に := を使ってデフォルト値が与えられている．これらのデフォルト値のおかげで，ほとんどのインスタンスは以前の定義と同じように構築されます．しかし， ℤ の特殊なケースでは，特定の値を指定することができます．

class AddMonoid₄ (M : Type) extends AddSemigroup₃ M, AddZeroClass M where
  /-- Multiplication by a natural number. -/
  nsmul : ℕ → M → M := nsmul₁
  /-- Multiplication by `(0 : ℕ)` gives `0`. -/
  nsmul_zero : ∀ x, nsmul 0 x = 0 := by intros; rfl
  /-- Multiplication by `(n + 1 : ℕ)` behaves as expected. -/
  nsmul_succ : ∀ (n : ℕ) (x), nsmul (n + 1) x = x + nsmul n x := by intros; rfl

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

nsmul に関連するフィールドを提供しなくても積モノイドのインスタンスを構築できることを確認してみましょう．

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

いよいよ ℤ の特殊なケースを扱いましょう．ここでは， ℕ から ℤ への型強制と， ℤ の乗算を使用して nsmul を構築します．特に証明フィールドには上記のデフォルト値よりも多くの作業がふくまれていることに注意してください．

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

問題が解決下かどうか確認してみましょう．Leanにはすでに自然数と整数のスカラー倍の定義があり，またここでは上記で定義したインスタンスが使われることを確認したいため， • 表記は使わず， SMul.mul を呼び出し，上記のインスタンスを明示的に提供します．

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

この話は群の定義に zsmul フィールドを組み込んだり，似たようなトリックを使ったりしながら続きます．これでMathlibのモノイド，群，環，加群の定義を読む準備ができました．これらは巨大な階層の一部であるため，ここで見たものよりも複雑ですが，すべての原理は上で説明したとおりです．

演習として上で構築した順序関係階層に戻り，「未満」記法 <₁ を持つ型クラス LT₁ を組み込み，すべての前順序に ≤₁ から構築されたデフォルト値を持つ <₁ とこれら2つの比較演算子の間の自然な関係を確認する Prop 値フィールドが付属していることを確認しましょう．

7.2. 射

この章ではここまで，数学的構造の階層を作る方法について述べてきました．しかし，構造を定義するには射が必要です．射の定義には2つのアプローチがあります．最も明白なのは，関数に対しての述語を定義することです．

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

この定義では，連言を使うことは少々好ましくありません．特に使う側にとっては，2つの条件にアクセスしたいときに条件の並び順を覚えておかなければなりません．そこで，上記の代わりに構造体を使うことができます．

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

ここまで来ると，上記をクラスにして，型クラスのインスタンス解決プロセスを使って，単純な関数のインスタンスから複雑な関数の isMonoidHom₂ を自動的に推論できるようにしたくなるでしょう．例えばモノイドの射の合成はモノイドの射となり，これは上記クラスの有用なインスタンスのように思えるでしょう．しかし，このようなインスタンスは g ∘ f を至るところで探し出す必要があるので，解決プロセスにとっては非常に厄介です． g (f x) でさえも失敗してしまうので，使う人にとってはとてもイライラすることでしょう．より一般的には，与えられた式の中でどの関数が適用されているかを認識することは「高階ユニフィケーション問題」と呼ばれる非常に難しい問題であることを常に念頭に置く必要があります．そのため，Mathlibではこのようなクラスの使い方はされていません．

より根本的な問題として，上記のように述語を使うか（ def か structure のどちらでも），それとも関数と述語を束ねた構造体を使うのかということです．これは気持ちの問題でもあります．射ではないモノイド間の関数を考えることは非常にまれです．「モノイドの射」は普通の関数につけられる形容詞ではなく，名詞なのです．一方で位相空間の間の連続関数は，考えていた対象の関数がたまたま連続だったと主張することもできます．これがMathlibに Continuous という述語がある理由です．例えば次のように書くことができます:

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

連続関数のあつまりは，例えば連続関数の空間に位相を置くのに便利ですが，連続性を扱う主要な道具ではありません．

これとは対照的に，モノイド（あるいは他の代数的構造）間の射は以下のようにまとめられます:

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

もちろん，全ての利用箇所で toFun を打ち込みたいわけではないので， CoeFun 型クラスを使って型強制を登録します．最初の引数は関数に強制したい型です．第2引数には対象となる関数の型を指定します．この場合，すべての f : MonoidHom₁ G H に対して常に G → H とします．また， MonoidHom₁.toFun には coe 属性のタグを付け， ↑ 接頭辞をつけるだけでタクティクモードではほとんど toFun の存在が見えないようになるようにしています．

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

attribute [coe] MonoidHom₁.toFun

モノイドの射のあつまりを要素に適用できることを確認してみましょう．

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

他の射についても環の射についてまでは同じことができます．

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

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

attribute [coe] AddMonoidHom₁.toFun

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

この方法にはいくつか問題があります．そのうちの些細なものとして， RingHom₁.toFun が存在しないため， coe 属性をどこに置けばいいのかよくわからないことです．対応する関数は MonoidHom₁.toFun ∘ RingHom₁.toMonoidHom₁ ですが，これは属性タグを付けられる宣言ではありません．（ただ CoeFun  (RingHom₁ R S) (fun _ ↦ R → S) インスタンスを定義することはできます．）もっと重要なのは，モノイドの射に関する補題は環の射には直接適用できないということです．このため，モノイドの射の補題を適用しようとするたびに， RingHom₁.toMonoidHom₁ と格闘するか，環の射の補題をすべて書き直すかのどちらかしかありません．どちらの選択肢も魅力的ではないため，Mathlibはここで新しい階層の技法を使います．そのアイデアは，少なくともモノイド射であるオブジェクトのための型クラスを定義し，そのクラスをモノイドの射と環の射の両方でインスタンス化し，すべての補題を記述するために使うというものです．以下の定義では， F は MonoidHom₁ M N であり，また M と N が環構造を持つ場合は RingHom₁ M N でもあります．

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

しかし，上記の実装には問題があります．まだ関数インスタンスへの型強制が登録されていません．これをやってみましょう．

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

このようなインスタンスの作成はよくありません． f が関数の型ではない場合に f x という式に遭遇した時，Leanは f を関数に変換するために CoeFun インスタンスを探そうとします．上記の関数の型は {M N F : Type} → [Monoid M] → [Monoid N] → [MonoidHomClass₁ F M N] → CoeFun F (fun x ↦ M → N) となり，したがってこれを適用しようとすると，未知の型 M と N ， F がどの順番で推論されるべきかLeanにとっては先験的に明らかではありません．これは前節で見た悪いインスタンスの種類とはまた少し違うものですが，同じ問題に帰着します． M のインスタンスがわからないと，Leanは未知の型のモノイドインスタンスを探さなければならず，データベース内の すべての モノイドインスタンスを試すことになります．このようなインスタンスの効果を見たい場合は，上記の宣言の上に set_option synthInstance.checkSynthOrder false in と入力し， def badInst を instance に置き換えると，このファイル中であちこち失敗することを確認できるでしょう．

この問題の解決は簡単です．まず F がなんであるかを検索し，次に M と N を推論するようにLeanに指示すればよいのです．これは outParam 関数を使って行います．この関数は恒等関数として定義されていますが，型クラスの仕組みによって認識され，目的の動作を引き起こします．したがって， outParam 関数に注意しながら，クラスの定義をやり直すことができます．

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

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

attribute [coe] MonoidHomClass₂.toFun

これでこのクラスをインスタンス化する方針を進めることができます．

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

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

お約束したように， MonoidHomClass₁ F のインスタンスを仮定して， f : F について証明するすべての補題は，モノイドの射と環の射の両方に適用できます．補題の例を見て，両方の状況に当てはまることを確認してみましょう．

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

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

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

一見すると， MonoidHom₁ をクラスにするという昔の悪いアイデアに戻ったように見えるかもしれません．しかしそうではありません．すべて抽象度が1つ上がっているのです．型クラス解決プロセスは関数を探すのではなく， MonoidHom₁ か RingHom₁ のどちらかを探すことになります．

本書でのアプローチで残っている問題は， toFun フィールドとそれに対応する CoeFun インスタンスと coe 属性の周りに繰り返しコードが存在することです．また，このパターンは余分なプロパティを持つ関数にのみ使用され，関数への型強制は単射的であるべきだということを記録しておいたほうが良いでしょう．このために，Mathlibは基底クラス `` DFunLike`` （ DFun は依存関数を意味します）で抽象化のレイヤーを1つ増やしています．この基底クラスの上に MonoidHomClass を再定義してみましょう．

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

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

もちろん射の階層はここで終わりません．さらに続けて MonoidHomClass₃ を特殊化した RingHomClass₃ クラスを定義し，それを RingHom にインスタンス化し，さらに AlgebraHom にインスタンス化することもできます．（代数環は環に特別な構造を加えたものです．）しかし，Mathlibで使用される射の主な形式化のアイデアをカバーしたので，Mathlibで射がどのように定義されるかを理解する準備はできているはずです．

演習問題として，順序型の間の順序を保つ関数を集めたクラスと，順序を保つモノイドの射を定義してみましょう．これは練習のためだけのものです．連続関数と同様に，順序を保つ関数はMathlibではとくにまとめられておらず， Monotone 述語によって定義されています．この演習を達成するにはもちろん，以下のクラス定義を完成させる必要があります．

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

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

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

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

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

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

7.3. 部分対象

ある代数構造とその射を定義した後の次なるステップとして，この代数構造を継承する集合，例えば部分群や部分環を考えましょう．これは前回の話題とほぼ重複します．実際， X の集合は X から Prop への関数として実装されるので，部分対象はある述語を満たす関数です．したがって， DFunLike クラスとその子孫のクラスを生み出した多くのアイデアを再利用できます． DFunLike 自体は再利用しません．これをしてしまうと集合 X から X → Prop への抽象化の壁を壊してしまうためです．その代わりに SetLike クラスが存在します．関数型への埋め込みをラップする代わりに，このクラスは Set 型への埋め込みをラップし，対応する型強制と Membership インスタンスを定義します．

@[ext]
structure Submonoid₁ (M : Type) [Monoid M] where
  /-- The carrier of a submonoid. -/
  carrier : Set M
  /-- The product of two elements of a submonoid belongs to the submonoid. -/
  mul_mem {a b} : a ∈ carrier → b ∈ carrier → a * b ∈ carrier
  /-- The unit element belongs to the submonoid. -/
  one_mem : 1 ∈ carrier

/-- Submonoids in `M` can be seen as sets in `M`. -/
instance [Monoid M] : SetLike (Submonoid₁ M) M where
  coe := Submonoid₁.carrier
  coe_injective' _ _ := Submonoid₁.ext

上記の SetLike インスタンスがあれば， N.carrier を使わなくても，部分モノイド N が 1 を含むことを自然に示すことができます．また， N を M の集合として扱い，写像の像を直接取ることもできます．

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

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

また SubType を使うことで Type への型強制も行え得るため，部分モノイド N に対して， N に属する M の要素へと強制できるようなパラメータ (x : N) を書くことができます．

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

この Type への強制を使って，部分モノイドにモノイド構造を持たせることもできます．上記のように N に関連する型からの強制と，この型強制が単射であることを保証する補題 SetCoe.ext を使用します．どちらも SetLike インスタンスによって提供されます．

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

上記の例では， M への型強制の使用と property フィールドを呼び出す代わりに，以下のように分解しながらの束縛を使用することができたことに注意してください．

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

部分モノイドに関する補題を部分群や部分環に適用するには，射と同じようにクラスが必要です．このクラスは SetLike インスタンスをパラメータとして受け取るので，carrierフィールドを必要とせず，フィールドに帰属の表記を使うことができます．

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

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

演習として， Subgroup₁ 構造体を定義し，それに SetLike インスタンスと SubmonoidClass₁ インスタンスを与え， Subgroup₁ に関連付けられた部分型に Group インスタンスを置き， SubgroupClass₁ クラスを定義してください．

知っておくべき点としてもう一つ重要なこととして，Mathlibでは所与の代数オブジェクトの部分対象は完備束を構成し，この構造はよく使われるということです．例えば，「部分モノイド同士の共通部分も部分モノイドである」という補題を探したい場合を考えましょう．しかし，これは補題ではなく，下限の構成です．2つの部分モノイドの場合を考えてみましょう．

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

これにより，2つの部分モノイドの共通部分を部分モノイドとして得ることができます．

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

上の例で共通部分の記号 ∩ の代わりに下限の記号 ⨅ を使わなければならなかったのは残念だと思うかもしれません．しかし，上限の場合について考えてみましょう．2つの部分モノイドの合併は部分モノイドになりません．しかし，部分モノイドは束を（特に完備であるものを）形成します．実際には， N ⨆ P は N と P の合併によって生成される部分モノイドであり，もちろんこれを N ∪ P で表すのは非常に紛らわしくなります．したがって，上記で N ⊓ P を使うほうが一貫性があることがわかるでしょう．また，この書き方は様々な種類の代数構造に対してもより一貫性があります．2つのベクトル部分空間 E と F の和を E + F ではなく， E ⊔ F と表記するのは最初は少し奇妙に見えるかもしれません．しかしすぐに慣れるでしょう．そしてすぐに E + F という表記が， E ⊔ F が E と F の両方を含む最小のベクトル部分空間であるという基本的な事実よりも E ⊔ F の要素が E と F の要素の和として書けるというわかりやすい事実を強調する気休めのようなものだと考えるようになるでしょう．

この章の最後の話題は商についてです．ここでもMathlibで便利な表記法がどのように構築され，コードの重複がどのように回避されているかを説明していきます．ここでの主な工夫は HasQuotient クラスで， M ⧸ N のように書き表すことができます．この商の記号 ⧸ は特殊なUnicode文字で，通常のASCIIの除算記号ではないので注意してください．

例として，可換モノイドの部分モノイドによる商を作ることにしましょう．最後の例では， Setoid.refl を使うことができますが，その際に適切な Setoid 構造が自動的に選ばれてはくれません．この問題は @Setoid.refl M N.Setoid のようにすべての引数を @ 構文で指定することで解決できます．

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

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

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

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