nLab division

Contents

Idea

Given a Heyting field $F$ , let us define the type of all terms in $F$ apart from 0:

F_{#0} \coloneqq \{a \in F \vert a # 0\}

The division function is a binary function $\frac{(-)}{(-)}:F \times F_{#0} \to F$ defined as

\frac{x}{y} \coloneqq x \cdot \frac{1}{y}

where

\frac{1}{y}

Given finite set $A$ and pointed set $B$ with an element $p:B$ , one can construct finite sets $A \div B$ and $A\ \%\ B$ with a bijection

A \simeq ((B \times (A \div B)) + (A\ \%\ B))

and a bijection

(B \hookrightarrow A\ \%\ B) \simeq \emptyset

A finite pointed set $B$ is a divisor of $A$ if there is a bijection $(A\ \%\ B) \simeq \emptyset$ :

A \vert B \coloneqq (A\ \%\ B) \simeq \emptyset

Last revised on February 27, 2024 at 06:30:33. See the history of this page for a list of all contributions to it.