数学の定義集
トップへ戻る: index.md
数学というかLeanのmathlibというかの定義を日本語化したもの。工事中
$\mathrm{Mul}$
mathlib
型 $\alpha$ に対して、構造 $\mathrm{Mul} \; \alpha$ は、
- $\mathrm{mul},*: \alpha \to \alpha \to \alpha$
を備える構造である。
$\mathrm{Semigroup}$ (半群)
mathlib
型 $G$ に対して、構造 $\mathrm{Semigroup} \; G$ は、
- $\mathrm{Mul} \; G$
- $\mathrm{mul},*: G \to G \to G$
を備え、次の公理を満たす構造である。
- $\mathrm{mul\_assoc}: \forall a,b,c \in G,\; (a * b) * c = a * (b * c)$
$\mathrm{One}$
mathlib
型 $\alpha$ に対して、構造 $\mathrm{One} \; \alpha$ は
を備える構造である。
$\mathrm{MulOne}$
mathlib
型 $M$ に対して、構造 $\mathrm{MulOne} \; M$ は
- $\mathrm{Mul} \; M$
- $\mathrm{mul},*: M \to M \to M$
- $\mathrm{One} \; M$
を備える構造である。
$\mathrm{MulOneClass}$
mathlib
型 $M$ に対して、構造 $\mathrm{MulOneClass} \; M$ は
- $\mathrm{Mul} \; M$
- $\mathrm{mul},*: M \to M \to M$
- $\mathrm{One} \; M$
を備え、次の公理を満たす構造である。
- $\mathrm{one\_mul}: \forall a \in M,\; 1 * a = a$
- $\mathrm{mul\_one}: \forall a \in M,\; a * 1 = a$
$\mathrm{Monoid}$ (モノイド)
mathlib
型 $M$ に対して、構造 $\mathrm{Monoid} \; M$ は
- $\mathrm{Mul} \; M$
- $\mathrm{mul},*: M \to M \to M$
- $\mathrm{One} \; M$
を備え、次の公理を満たす構造である。
- $\mathrm{Semigroup} \; M$
- $\mathrm{mul\_assoc}: \forall a,b,c \in M,\; (a * b) * c = a * (b * c)$
- $\mathrm{MulOneClass} \; M$
- $\mathrm{one\_mul}: \forall a \in M,\; 1 * a = a$
- $\mathrm{mul\_one}: \forall a \in M,\; a * 1 = a$
$\mathrm{Inv}$
mathlib
型 $\alpha$ に対して、構造 $\mathrm{Inv} \; \alpha$ は
- $\mathrm{inv},\cdot^{-1}: \alpha \to \alpha$
を備えた構造である。
$\mathrm{Div}$
mathlib
型 $\alpha$ に対して、構造 $\mathrm{Div} \; \alpha$ は
- $\mathrm{div},/: \alpha \to \alpha \to \alpha$
を備えた構造である。
$\mathrm{DivInvMonoid}$
mathlib
型 $G$ に対して、構造 $\mathrm{DivInvMonoid} \; G$ は
- $\mathrm{Mul} \; G$
- $\mathrm{mul},*: G \to G \to G$
- $\mathrm{One} \; G$
- $\mathrm{Inv} \; G$
- $\mathrm{inv},\cdot^{-1}: G \to G$
- $\mathrm{Div} \; G$
- $\mathrm{div},/: G \to G \to G$
を備え、次の公理を満たす構造である。
- $\mathrm{Semigroup} \; G$
- $\mathrm{mul\_assoc}: \forall a,b,c \in G,\; (a * b) * c = a * (b * c)$
- $\mathrm{MulOneClass} \; G$
- $\mathrm{one\_mul}: \forall a \in G,\; 1 * a = a$
- $\mathrm{mul\_one}: \forall a \in G,\; a * 1 = a$
- $\mathrm{div\_eq\_mul\_inv}: \forall a,b \in G,\; a / b = a * b^{-1}$
$\mathrm{Group}$ (群)
mathlib
型 $G$ に対して、構造 $\mathrm{Group} \; G$ は
- $\mathrm{Mul} \; G$
- $\mathrm{mul},*: G \to G \to G$
- $\mathrm{One} \; G$
- $\mathrm{Inv} \; G$
- $\mathrm{inv},\cdot^{-1}: G \to G$
- $\mathrm{Div} \; G$
- $\mathrm{div},/: G \to G \to G$
を備え、次の公理を満たす構造である。
- $\mathrm{Semigroup} \; G$
- $\mathrm{mul\_assoc}: \forall a,b,c \in G,\; (a * b) * c = a * (b * c)$
- $\mathrm{MulOneClass} \; G$
- $\mathrm{one\_mul}: \forall a \in G,\; 1 * a = a$
- $\mathrm{mul\_one}: \forall a \in G,\; a * 1 = a$
- $\mathrm{DivInvMonoid} \; G$
- $\mathrm{div\_eq\_mul\_inv}: \forall a,b \in G,\; a / b = a * b^{-1}$
- $\mathrm{inv\_mul\_cancel}: \forall a \in G,\; a^{-1} * a = 1$
$\mathrm{CommMagma}$
mathlib
型 $G$ に対して、構造 $\mathrm{CommMagma} \; G$ は
- $\mathrm{Mul} \; G$
- $\mathrm{mul},*: G \to G \to G$
を備え、次の公理を満たす構造である。
- $\mathrm{mul\_comm}: \forall a,b \in G,\; a * b = b * a$
$\mathrm{CommSemigroup}$
mathlib
型 $G$ に対して、構造 $\mathrm{CommSemigroup} \; G$ は
- $\mathrm{Mul} \; G$
- $\mathrm{mul},*: G \to G \to G$
を備え、次の公理を満たす構造である。
- $\mathrm{Semigroup} \; G$
- $\mathrm{mul\_assoc}: \forall a,b,c \in G,\; (a * b) * c = a * (b * c)$
- $\mathrm{CommMagma} \; G$
- $\mathrm{mul\_comm}: \forall a,b \in G,\; a * b = b * a$
$\mathrm{CommMonoid}$
mathlib
型 $G$ に対して、構造 $\mathrm{CommMonoid} \; M$ は
- $\mathrm{Mul} \; M$
- $\mathrm{mul},*: M \to M \to M$
- $\mathrm{One} \; M$
を備え、次の公理を満たす構造である。
- $\mathrm{Semigroup} \; M$
- $\mathrm{mul\_assoc}: \forall a,b,c \in M,\; (a * b) * c = a * (b * c)$
- $\mathrm{MulOneClass} \; M$
- $\mathrm{one\_mul}: \forall a \in M,\; 1 * a = a$
- $\mathrm{mul\_one}: \forall a \in M,\; a * 1 = a$
- $\mathrm{CommMagma} \; M$
- $\mathrm{mul\_comm}: \forall a,b \in M,\; a * b = b * a$
$\mathrm{CommGroup}$ (可換群・アーベル群 mul版)
mathlib
型 $G$ に対して、構造 $\mathrm{CommGroup} \; G$ は
- $\mathrm{Mul} \; G$
- $\mathrm{mul},*: G \to G \to G$
- $\mathrm{One} \; G$
- $\mathrm{Inv} \; G$
- $\mathrm{inv},\cdot^{-1}: G \to G$
- $\mathrm{Div} \; G$
- $\mathrm{div},/: G \to G \to G$
を備え、次の公理を満たす構造である。
- $\mathrm{Semigroup} \; G$
- $\mathrm{mul\_assoc}: \forall a,b,c \in G,\; (a * b) * c = a * (b * c)$
- $\mathrm{MulOneClass} \; G$
- $\mathrm{one\_mul}: \forall a \in G,\; 1 * a = a$
- $\mathrm{mul\_one}: \forall a \in G,\; a * 1 = a$
- $\mathrm{CommMagma} \; G$
- $\mathrm{mul\_comm}: \forall a,b \in G,\; a * b = b * a$
- $\mathrm{DivInvMonoid} \; G$
- $\mathrm{div\_eq\_mul\_inv}: \forall a,b \in G,\; a / b = a * b^{-1}$
- $\mathrm{Group} \; G$
- $\mathrm{inv\_mul\_cancel}: \forall a \in G,\; a^{-1} * a = 1$
$\mathrm{Quiver}$
mathlib
型 $V$ に対して、構造 $\mathrm{Quiver} \; V$ は
- $\mathrm{Hom},\rightarrow: V \to V \to \mathrm{Sort}\;v$
を備える構造である。
---
古いもの
（単位的）環（Ring）
mathlib
組 $(R,\,+,\,\cdot,\,0,\,1,\,-)$ が（単位的）環（ring）であるとは、
- 台集合: $R$（集合）
- 加法: $+: R \to R \to R$
- 乗法: $\cdot: R \to R \to R$
- 負: $-: R \to R$
- 零元: $0 \in R$
- 乗法単位元: $1 \in R$
を備え、次の公理を満たすことをいう。
- $\forall a,b,c \in R,\; (a + b) + c = a + (b + c)$
- $\forall a \in R,\; (a + 0 = a) \land (0 + a = a)$
- $\forall a,b \in R,\; a + b = b + a$
- $\forall a,b,c \in R,\; a \cdot (b + c) = a \cdot b + a \cdot c$
- $\forall a,b,c \in R,\; (a + b) \cdot c = a \cdot c + b \cdot c$
- $\forall a,b,c \in R,\; (a \cdot b) \cdot c = a \cdot (b \cdot c)$
- $\forall a \in R,\; 1 \cdot a = a$
- $\forall a \in R,\; a \cdot 1 = a$
- $\forall a \in R,\; (-a) + a = 0$
体（Field）
mathlib
組 $(K,\,+,\,\cdot,\,0,\,1,\,-,\,{}^{-1})$ が体（field）であるとは、
- 台集合: $K$（集合）
- 加法: $+: K \to K \to K$
- 乗法: $\cdot: K \to K \to K$
- 加法に関する逆元（負）: $-: K \to K$
- 零元: $0 \in K$
- 乗法単位元: $1 \in K$
- 乗法に関する逆元写像: ${}^{-1}: K \setminus\{0\} \to K \setminus\{0\},\; a \mapsto a^{-1}$
を備え、次の公理を満たすことをいう。
- $\forall a,b,c \in K,\; (a + b) + c = a + (b + c)$
- $\forall a \in K,\; 0 + a = a$
- $\forall a \in K,\; a + 0 = a$
- $\forall a,b \in K,\; a + b = b + a$
- $\forall a \in K,\; (-a) + a = 0$
- $\forall a,b,c \in K,\; (a \cdot b) \cdot c = a \cdot (b \cdot c)$
- $\forall a \in K,\; 1 \cdot a = a$
- $\forall a \in K,\; a \cdot 1 = a$
- $\forall a \in K\setminus\{0\},\; a \cdot a^{-1} = 1$
- $\forall a,b \in K,\; a \cdot b = b \cdot a$
- $\forall a,b,c \in K,\; a \cdot (b + c) = a \cdot b + a \cdot c$
- $\forall a,b,c \in K,\; (a + b) \cdot c = a \cdot c + b \cdot c$
- $\exists x \in K,\; \exists y \in K,\; x \neq y$
圏（Category）
mathlib
データ $(\mathcal{C},\,\mathrm{Ob},\,\mathrm{Hom},\,\mathrm{id},\,\circ)$ が圏（category）であるとは、
- 対象の類（あるいは集合）: $\mathrm{Ob}(\mathcal{C})$
- 射の集合族: 各 $X,Y\in\mathrm{Ob}(\mathcal{C})$ に対して集合 $\mathrm{Hom}_{\mathcal{C}}(X,Y)$（$X$ から $Y$ への射の集合）
- 恒等射: 各 $X\in\mathrm{Ob}(\mathcal{C})$ に対して $\mathrm{id}_X\in\mathrm{Hom}_{\mathcal{C}}(X,X)$
- 合成: 各 $X,Y,Z\in\mathrm{Ob}(\mathcal{C})$ に対して写像
$\circ:\; \mathrm{Hom}_{\mathcal{C}}(Y,Z)\times \mathrm{Hom}_{\mathcal{C}}(X,Y)\to \mathrm{Hom}_{\mathcal{C}}(X,Z),\; (g,f)\mapsto g\circ f$
を備え、次の公理（圏の公理）を満たすことをいう。
- $\forall f \in \mathrm{Hom}(W,X),\; \forall g \in \mathrm{Hom}(X,Y),\; \forall h \in \mathrm{Hom}(Y,Z),\; h \circ (g \circ f) = (h \circ g) \circ f$
- $\forall f \in \mathrm{Hom}(X,Y),\; \mathrm{id}_Y \circ f = f$
- $\forall f \in \mathrm{Hom}(X,Y),\; f \circ \mathrm{id}_X = f$