Project
\(\alpha \)がlevel uの型である(Type u)であるとは，\(\alpha \)が宇宙\(u\)に属することである．
すべての項あるいは式(Expressions)は型(Type)を持つ．
Type uである\(\alpha \)が単位元を持つ(One)であるとは，以下の性質を満たすことである．
この\(\alpha \)型のoneを\(1\)と書き，これを単位元と呼ぶ．
以降，\(\alpha \)と\(1\)の関係を明記したい場合，これを\(\alpha \)と\(1\)の組\((\alpha ,1)\)を用いて\(\alpha = (\alpha ,1)\)と記述する．
また，\(1\)が単位元を持つ\(\alpha \)の単位元であることを明記したい場合，これを\(1_\alpha \)と記述する．
(注意)上記における\(1\)とは単位元という名前を持つ元があるということだけを保証しているに過ぎない.つまり\(\alpha \)がOne型であるとは\(1\)という\(\alpha \)型の値を持つだけで，その性質は定義していない．
Type uである\(\alpha \)が逆元を持つ(Inv)であるとは，関数Invについて以下の性質を満たすことである．
この\(\alpha \rightarrow \alpha \)型の関数invについて，inv \(\alpha \)を\(\alpha ^{-1}\)と書き，これを逆元と呼ぶ．
（注意）上記におけるinvは\(\alpha \)に対して\(\alpha ^{-1}\)を対応させているだけに過ぎない．つまり\(\alpha \)がInv型であるとは\(\alpha ^{-1}\)という\(\alpha \rightarrow \alpha \)型の値を持つだけで，その性質は定義していない．
Type uである\(\alpha \)が乗法\(\cdot \)で閉じている(Mul)であるとは，二項関数\(\cdot \)について以下の性質を満たすことである．
この\(\cdot \)を乗法演算子と呼ぶ．
以降，\(\alpha \)と\(\cdot \)の関係を明記したい場合，これを\(\alpha \)と\(\cdot \)の組\((\alpha ,\cdot )\)を用いて\(\alpha = (\alpha ,\cdot )\)と記述する．
また，\(\cdot \)が乗法で閉じている\(\alpha \)の乗法演算子であることを明記したい場合，これを\(\cdot _\alpha \)と記述する．
Type uである\(G\)が半群(Semigroup)であるとは，\(G=(G,\cdot )\)が乗法で閉じていて，かつ以下の性質を満たすことである．
また，半群\((G,\cdot _G),(G',\cdot _{G'})\)が等しいとは，型\(G,G'\)が等しく，また乗法演算子\(\cdot _G,\cdot _{G'}\)が等しいということである．
つまり，以下を満たすことである（外延性）．
Type uである\(G\)が乗法単位元を持つ(MulOneClass)であるとは，\((M,\cdot ,1)\)が単位元を持ち，\((M,\cdot ,1)\)が乗法で閉じていて，かつ以下の性質を満たすことである．
Type uであるMがモノイド(Monoid)であるとは，\((M,\cdot _M,1_M)\)が半群で，\((M,\cdot _M,1_M)\)が乗法単位元を持ち，かつ以下の性質を満たすことである．
\(A\)が，単位元を持つ\((M,1_M),(N,1_N)\)の組\((M,N)\)のOneHomであるとは，\(A\)が以下の性質を満たすことである．
\(A\)が，乗法で閉じている\((M,\cdot _M),(N,\cdot _N)\)の組\((M,N)\)のMulHomであるとは，\(A\)が以下の性質を満たすことである．
MulHomである\((M,N)\)を\(M →^{*}_{n} N\)と略記する．
\(A\)が，乗法単位元を持つ\((M,\cdot _M,1_M),(N,\cdot _N,1_N)\)の組\((M,N)\)のMonoidHom型であるとは，\(A\)が組\((M,N)\)のOneHomで，\(A\)が組\((M,N)\)のMulHomであることである．
\((M,N)\)のMonoidHomを\(M →* N\)と略記する．また，\(M →* N\)型の値をモノイド準同型と呼ぶことにする．
\(A\)が，Type uである\(\alpha \)のSet型であるとは，\(A\)が\(\alpha \rightarrow \)Prop型の関数であることである．
数学的に\(a \in M\)であることと，Lean4において\(\alpha : \)Set \(M = M\rightarrow \)Prop型から\(\alpha a = \)Trueであることは同値である．
\(A\)が，Type*であり乗法で閉じている\(M=(M,\cdot )\)の部分半群(Subsemigroup)型であるとは，\(A\)が以下の性質を満たすことである．
\(A\)が，Type*であり乗法単位元を持つ\(M=(M,\cdot _M,1_M)\)の部分モノイド(Submonoid)型であるとは，\(A\)が\(M\)の部分半群であり，かつ以下の性質を満たすことである．
\(A\)が，Type*であり群である\(G\)の部分群(Subgroup)型であるとは，\(A\)が\(G\)の部分モノイドであり，かつ以下の性質を満たすことである．
モノイド\(M,N\)，モノイド準同型\(f : M \rightarrow N\)に対して，\(N'\)を\(N\)の最小の部分モノイドとしたとき，\(f\)の核\(\ker f\)は以下のように定義される．
Type uである\(A\)，Type vである\(B\)の組\((A,B)\)がHasQuotient型であるとは，以下の性質を満たすことである．
\(A / B\)
Sort*である\(\iota \)，Type*である\(\alpha \)に対し，\(f : \iota \rightarrow \alpha \)のrangeとは，Set \(\alpha \)型であり，\(y\in \iota ,x\in \alpha \)に対してProp型\(\{ x | ∃ y, f y = x\} \)を返す関数である．
\(f : G →* N\)のrangeとは，\(N\)の部分群型であり，Deffinition18の意味で「\(G\)の部分群の中で最大のものを集合と見做したもの」の\(f\)のrangeに\(N\)の部分群型の性質を与えたものである．
これをrange\((f)\)と書くことにする．
\(A\)が，Sort*である\(\alpha \)とSort*である\(\beta \)の組\((\alpha ,\beta )\)のEquiv型であるとは，\(A\)が以下の性質を満たすことである．
\((\alpha ,\beta )\)のEquivを\(\alpha \simeq \beta \)と略記する．
\(A\)が，乗法で閉じている\(M=(M,\cdot ),N=(N,\cdot )\)の組\((M,N)\)の同型(MulEquiv)型であるとは，\(A\)が(M,N)のEquip(\(M \simeq N\))型であり，\(A\)が(M,N)のMonoidHom(\(M →^{*}_{n} N\))型であることである．
\((M,N)\)のMulEquivを\(M \simeq * N\)と略記する．
\( G , G' \)を群とし，\( \phi : G \to G' \)を群準同型とする．この時，
が成り立つ．
\(G\) / \(\ker \phi \simeq *\) range \((\phi )\) 型の\(A\)を定義する．
このとき\(A\)は定義より以下の条件
を満たすとき，以下の性質を持つ．
[Equiv]
[MonoidHom]
(\(G / \ker \phi →* \text{range} (\phi )\))型の関数（すなわちモノイド準同型な\(f : G / \ker \phi → \phi (G)\)）をMulEquivのtoFun関数とする．
この\(f\)は(rangeKerLiftInjective \(\phi \)とrangeKerLiftSurjective \(\phi \)より)全単射であるため[Equiv]を満たし，モノイド準同型[MonoidHom]を満たす．
以上より全単射かつモノイド準同型な関数\(f\)によって\(G\) / \(\ker \phi \simeq *\) range \((\phi )\) 型の\(A\)を定義できたため，全単射かつモノイド準同型な関数\(f\)について準同型定理が成り立つ．