---
tags: TrRun3
id: Arrg-B12_inverse.md
---

# 檜山トレラン3 B12 「逆」のオーバーロード

$\require{color}%
\newcommand{\BL}{ \{\![ }
\newcommand{\BR}{ ]\!\} }
\newcommand{\Keyword}[1]{ \textcolor{green}{ \bf \text{#1} } }%
\newcommand{\When}{\Keyword{When } }
\newcommand{\conc}{\mathop {\#}}%
\newcommand{\In}{\text{ in }}%
\newcommand{\For}{\Keyword{For }}%
\newcommand{\Imp}{ \Rightarrow }%
\newcommand{\Let}{\Keyword{Let }}%
\newcommand{\WeDefine}{\Keyword{WeDefine }}%
\newcommand{\WeAssert}{\Keyword{WeAssert }}%
\newcommand{\Justification}{\Keyword{Justification }}%
\newcommand{\Then}{\Keyword{Then }}%
\newcommand{\cat}[1]{\mathcal{#1}}%
\newcommand{\Where}{\Keyword{Where }}%
\newcommand{\WeWillDefine}{\Keyword{WeWillDefine }}%
\newcommand{\WeUseNotation}{\Keyword{WeUseNotation }}%
\newcommand{\WeAbuseNotation}{\Keyword{WeAbuseNotation }}%
\newcommand{\Exn}[1]{ [\!( #1 )\!] }
\newcommand{\Iff}{\Leftrightarrow}
\newcommand{\R}{ {\bf R} }
\newcommand{\hyp}{ \text{-} }
\newcommand{\Rnn}{ {\bf R}_{\ge 0}}
\newcommand{\Rnni}{ {\bf R}_{\ge 0}^{+\infty}}
\newcommand{\Sy}[1]{ \langle #1 \rangle } % symbole
\newcommand{\id}{ \mathrm{id} } % id
\newcommand{\pto}{ \supseteq\!\to }
%$

$\WeUseNotation \cdots$ は、「$\cdots$ のような記法〈書き方〉を使う」という意味。$\WeAbuseNotation \cdots$ は、「好ましくはないけど（それを知っていて） $\cdots$ のような記法〈書き方〉を使う」という意味。

出てくる圏：

- ${\bf Set}$ ： 集合と写像の圏
- ${\bf Partial}$ ： 集合と部分写像の圏
- ${\bf Grp}$ ： 群と群準同型射〈group homomorphism〉の圏

## 写像の逆

$\For f:X \to Y \In {\bf Set}\\
\WeDefine IsInvertible(f) :\Iff
\forall y\in Y.\exists! x\in X. f(x) = y$

$\For X, Y\in |{\bf Set}| \\
\WeWillDefine inverseMap_{X, Y}:Map(X, Y) \to Map(Y, X)\In {\bf Partial}\\
\Let def(inverseMap_{X, Y}) := \{f \in Map(X, Y) \mid IsInvertible(f) \}\\
\For f\in def(inverseMap_{X, Y})\\
\WeWillDefine inverseMap_{X, Y}(f) \in Map(Y, X)\\
\WeDefine inverseMap_{X, Y}(f) := \lambda\, y\in Y.\varepsilon!\, \{x\in X \mid f(x) = y \}\\
\WeUseNotation f^{-1} := inverseMap_{X, Y}(f)$

## 一点の逆像

inverseImgOfPoint = inverse image of a point

$\For X, Y\in |{\bf Set}| \\
\WeWillDefine inverseImgOfPoint_{X, Y}:Map(X, Y) \to Map(Y, Pow(X)) \In {\bf Set}\\
\For f\in Map(X, Y)\\
\WeWillDefine inverseImgOfPoint_{X, Y}(f) \in Map(Y, Pow(X))\\
\WeDefine inverseImgOfPoint_{X, Y}(f) := \lambda\, y\in Y.(\, \{x\in X \mid f(x) = y\}\;\in Pow(X)\,)\\
\WeAbuseNotation f^{-1} := inverseImgOfPoint_{X, Y}(f)$

## 集合の逆像

inverseImgOfSet = inverse image of a set

$\For X, Y\in |{\bf Set}| \\
\WeWillDefine inverseImgOfSet_{X, Y}:Map(X, Y) \to Map(Pow(Y), Pow(X)) \In {\bf Set}\\
\For f\in Map(X, Y)\\
\WeWillDefine inverseImgOfSet_{X, Y}(f) \in Map(Pow(Y), Pow(X))\\
\WeDefine inverseImgOfSet_{X, Y}(f) := \lambda\, B\in Pow(Y).(\, \{x\in X \mid f(x) \in B\}\;\in Pow(X)\,)\\
\WeAbuseNotation f^{-1} := inverseImgOfSet_{X, Y}(f)$

## 部分写像の部分逆

parInv = partial inverse

[B11Ans 形式的線形結合の「形式的」とは 解答例](https://hackmd.io/@m-hiyama/SJIZbSEyY) 参照。

$\For f:X \to Y \In {\bf Partial}\\
\WeDefine IsPartiallyInvertible(f) :\Iff
\forall y\in Y.(\, y\in im(f) \Imp \exists! x\in X. f(x) = y \,)$

$\For X, Y \in |{\bf Partial}|\\
\WeWillDefine parInv_{X, Y}:ParMap(X, Y) \to ParMap(Y, X) \In {\bf Partial}\\
\Let def(parInv_{X, Y}) := \{f \in ParMap(X, Y) \mid IsPartiallyInvertible(f)\}\\
\For f\in def(parInv_{X, Y})\\
\WeWillDefine ParInv_{X, Y}(f) \in ParMap(Y, X)\\
\Let def(parInv_{X, Y}(f)) := im(f)\\
\WeDefine ParInv_{X, Y}(f) :=
\lambda\, y \in def(parInv_{X, Y}(f)).\varepsilon!\, \{ x\in X \mid f(x) = y\}\\
\WeAbuseNotation f^{-1} := parInv_{X, Y}(f)$

## 群の逆

inv = inverse element

$\For G = (\underline{G}, m_G, e_G) \in |{\bf Grp}|\\
\WeWillDefine inv_G:\underline{G} \to \underline{G} \In {\bf Set}\\
\WeDefine inv_G := \lambda\, x\in \underline{G}.(\,
\varepsilon!\, \{y \in \underline{G} \mid m_G(x, y) = e_G \land m_G(y, x) = e_G \} \;\in \underline{G}
\,)\\
\WeUseNotation x^{-1} := inv_G(x)$

## 逆数関数

recip = reciprocal function

$\For X \in |{\bf Set}|\\
\For G = (\underline{G}, m_G, e_G) \in |{\bf Grp}|\\
\WeWillDefine recip_{X, G}:Map(X, \underline{G}) \to Map(X, \underline{G}) \In {\bf Set}\\
\For f\in Map(X, \underline{G})\\
\WeWillDefine recip_{X, G}(f) \in Map(X, \underline{G})\\
\WeDefine recip_{X, G}(f) := \lambda\, x\in X.(\, inv_G(f(x))\;\in \underline{G}\,)\\
\WeAbuseNotation f^{-1} := recip_{X, G}(f)$

## その他

他にも $(\hyp)^{-1}$ のオーバーロードはあるだろう。毎回意味を確認する必要がある。