Return to Answer

Here is a constructive proof that can be enacted in any topos with a natural numbers object.

Let $i: H \to G$ be monic, and let $\pi: G \to G/H$ be the canonical surjective function $g \mapsto g H$  . Let $A$ be the free abelian group on $G/H$ with $j: G/H \to A$ the canonical injection, and let $A^G$ denote the set of functions $f: G \to A$, with the pointwise abelian group structure inherited from $A$. This carries a $G$-module structure defined by

$$(g \cdot f)(g') = f(g' g).$$

For any $f \in A^G$, the function $d_f: G \to A^G$ defined by $d_f(g) = g f - f$ defines a derivation. Passing to the wreath product $A^G \rtimes G$, we have two homomorphisms $\phi, \psi: G \rightrightarrows A^G \rtimes G$ defined by $\phi(g) := (d_{j \pi}(g), g)$ and $\psi(g) := (0, g)$. I claim that $i: H \to G$ is the equalizer of the pair $\phi, \psi$. For,

$$\begin{array}{lcl} d_{j\pi}(g) = 0 & \text{iff} & (\forall_{g': G})\; g\cdot j\pi(g') = j\pi(g') \\ & \text{iff} & (\forall_{g': G})\; j\pi(g' g) = j\pi(g') \\ & \text{iff} & (\forall_{g': G})\; j(g' gH) = j(g' H) \\ & \text{iff} & (\forall_{g': G})\; g' g H = g' H \\ & \text{iff} & g H = H \\ & \text{iff} & g \in H. \end{array}$$

(All we needed was some injection $j: G/H \to A$ into an abelian group; I chose the canonical one.)

Edit: Peter LeFanu Lumsdaine asked in a comment whether it is indeed constructively true that one can embed any set (or object in a topos) into an abelian group (object), and then later answered this affirmatively, which supplements this answer. The link to this effort is buried in a comment below; it deserves to be made more visible here: Constructively, is the unit of the “free abelian group” monad on sets injective?

Here is a constructive proof that can be enacted in any topos with a natural numbers object.

Let $i: H \to G$ be monic; let $\pi: G \to G/H$ be the canonical surjective function $g \mapsto g H$. Let $A$ be the free abelian group on $G/H$ with $j: G/H \to A$ the canonical injection, and let $A^G$ denote the set of functions $f: G \to A$, with the pointwise abelian group structure inherited from $A$. This carries a $G$-module structure defined by

$$(g \cdot f)(g') = f(g' g).$$

For any $f \in A^G$, the function $d_f: G \to A^G$ defined by $d_f(g) = g f - f$ defines a derivation. Passing to the wreath product $A^G \rtimes G$, we have two homomorphisms $\phi, \psi: G \rightrightarrows A^G \rtimes G$ defined by $\phi(g) := (d_{j \pi}(g), g)$ and $\psi(g) := (0, g)$. I claim that $i: H \to G$ is the equalizer of the pair $\phi, \psi$. For,

$$\begin{array}{lcl} d_{j\pi}(g) = 0 & \text{iff} & (\forall_{g': G})\; g\cdot j\pi(g') = j\pi(g') \\ & \text{iff} & (\forall_{g': G})\; j\pi(g' g) = j\pi(g') \\ & \text{iff} & (\forall_{g': G})\; j(g' gH) = j(g' H) \\ & \text{iff} & (\forall_{g': G})\; g' g H = g' H \\ & \text{iff} & g H = H \\ & \text{iff} & g \in H. \end{array}$$

(All we needed was some injection $j: G/H \to A$ into an abelian group; I chose the canonical one.)

Edit: Peter LeFanu Lumsdaine asked in a comment whether it is indeed constructively true that one can embed any set (or object in a topos) into an abelian group (object), and then later answered this affirmatively, which supplements this answer. The link to this effort is buried in a comment below; it deserves to be made more visible here: Constructively, is the unit of the “free abelian group” monad on sets injective?

Here is a constructive proof that can be enacted in any topos with a natural numbers object.

Let $i: H \to G$ be monic, and let $\pi: G \to G/H$ be the canonical surjective function $g \mapsto g H$ . Let $A$ be the free abelian group on $G/H$ with $j: G/H \to A$ the canonical injection, and let $A^G$ denote the set of functions $f: G \to A$, with the pointwise abelian group structure inherited from $A$. This carries a $G$-module structure defined by

$$(g \cdot f)(g') = f(g' g).$$

For any $f \in A^G$, the function $d_f: G \to A^G$ defined by $d_f(g) = g f - f$ defines a derivation. Passing to the wreath product $A^G \rtimes G$, we have two homomorphisms $\phi, \psi: G \rightrightarrows A^G \rtimes G$ defined by $\phi(g) := (d_{j \pi}(g), g)$ and $\psi(g) := (0, g)$. I claim that $i: H \to G$ is the equalizer of the pair $\phi, \psi$. For,

$$\begin{array}{lcl} d_{j\pi}(g) = 0 & \text{iff} & (\forall_{g': G})\; g\cdot j\pi(g') = j\pi(g') \\ & \text{iff} & (\forall_{g': G})\; j\pi(g' g) = j\pi(g') \\ & \text{iff} & (\forall_{g': G})\; j(g' gH) = j(g' H) \\ & \text{iff} & (\forall_{g': G})\; g' g H = g' H \\ & \text{iff} & g H = H \\ & \text{iff} & g \in H. \end{array}$$

(All we needed was some injection $j: G/H \to A$ into an abelian group; I chose the canonical one.)

Here is a constructive proof that can be enacted in any topos with a natural numbers object.

Let $i: H \to G$ be monic, and let $\pi: G \to G/H$ be the canonical surjective function $g \mapsto g H$ . Let $A$ be the free abelian group on $G/H$ with $j: G/H \to A$ the canonical injection, and let $A^G$ denote the set of functions $f: G \to A$, with the pointwise abelian group structure inherited from $A$. This carries a $G$-module structure defined by

$$(g \cdot f)(g') = f(g' g).$$

For any $f \in A^G$, the function $d_f: G \to A^G$ defined by $d_f(g) = g f - f$ defines a derivation. Passing to the wreath product $A^G \rtimes G$, we have two homomorphisms $\phi, \psi: G \rightrightarrows A^G \rtimes G$ defined by $\phi(g) := (d_{j \pi}(g), g)$ and $\psi(g) := (0, g)$. I claim that $i: H \to G$ is the equalizer of the pair $\phi, \psi$. For,

$$\begin{array}{lcl} d_{j\pi}(g) = 0 & \text{iff} & (\forall_{g': G})\; g\cdot j\pi(g') = j\pi(g') \\ & \text{iff} & (\forall_{g': G})\; j\pi(g' g) = j\pi(g') \\ & \text{iff} & (\forall_{g': G})\; j(g' gH) = j(g' H) \\ & \text{iff} & (\forall_{g': G})\; g' g H = g' H \\ & \text{iff} & g H = H \\ & \text{iff} & g \in H. \end{array}$$

(All we needed was some injection $j: G/H \to A$ into an abelian group; I chose the canonical one.)

Edit: Peter LeFanu Lumsdaine asked in a comment whether it is indeed constructively true that one can embed any set (or object in a topos) into an abelian group (object), and then later answered this affirmatively, which supplements this answer. The link to this effort is buried in a comment below; it deserves to be made more visible here: Constructively, is the unit of the “free abelian group” monad on sets injective?

Here is a constructive proof that can be enacted in any topos with a natural numbers object.

Let $i: H \to G$ be monic, and let $\pi: G \to G/H$ be the canonical surjective function $g \mapsto g H$ . Let $A$ be the free abelian group on $G/H$ with $j: G/H \to A$ the canonical injection, and let $A^G$ denote the set of functions $f: G \to A$, with the pointwise abelian group structure inherited from $A$. This carries a $G$-module structure defined by

$$(g \cdot f)(g') = f(g' g^{-1}).$$

For any $f \in A^G$, the function $d_f: G \to A^G$ defined by $d_f(g) = g f - f$ defines a derivation. Passing to the wreath product $A^G \rtimes G$, we have two homomorphisms $\phi, \psi: G \rightrightarrows A^G \rtimes G$ defined by $\phi(g) := (d_{j \pi}(g), g)$ and $\psi(g) := (0, g)$. I claim that $i: H \to G$ is the equalizer of the pair $\phi, \psi$. For,

$$\begin{array}{lcl} d_{j\pi}(g) = 0 & \text{iff} & (\forall_{g': G})\; g\cdot j\pi(g') = j\pi(g') \\ & \text{iff} & (\forall_{g': G})\; j\pi(g' g^{-1}) = j\pi(g') \\ & \text{iff} & (\forall_{g': G})\; j(g' g^{-1}H) = j(g' H) \\ & \text{iff} & (\forall_{g': G})\; g' g^{-1} H = g' H \\ & \text{iff} & g^{-1} H = H \\ & \text{iff} & g \in H. \end{array}$$

(All we needed was some injection $j: G/H \to A$ into an abelian group; I chose the canonical one.)

Here is a constructive proof that can be enacted in any topos with a natural numbers object.

Let $i: H \to G$ be monic, and let $\pi: G \to G/H$ be the canonical surjective function $g \mapsto g H$ . Let $A$ be the free abelian group on $G/H$ with $j: G/H \to A$ the canonical injection, and let $A^G$ denote the set of functions $f: G \to A$, with the pointwise abelian group structure inherited from $A$. This carries a $G$-module structure defined by

$$(g \cdot f)(g') = f(g' g).$$

For any $f \in A^G$, the function $d_f: G \to A^G$ defined by $d_f(g) = g f - f$ defines a derivation. Passing to the wreath product $A^G \rtimes G$, we have two homomorphisms $\phi, \psi: G \rightrightarrows A^G \rtimes G$ defined by $\phi(g) := (d_{j \pi}(g), g)$ and $\psi(g) := (0, g)$. I claim that $i: H \to G$ is the equalizer of the pair $\phi, \psi$. For,

$$\begin{array}{lcl} d_{j\pi}(g) = 0 & \text{iff} & (\forall_{g': G})\; g\cdot j\pi(g') = j\pi(g') \\ & \text{iff} & (\forall_{g': G})\; j\pi(g' g) = j\pi(g') \\ & \text{iff} & (\forall_{g': G})\; j(g' gH) = j(g' H) \\ & \text{iff} & (\forall_{g': G})\; g' g H = g' H \\ & \text{iff} & g H = H \\ & \text{iff} & g \in H. \end{array}$$

(All we needed was some injection $j: G/H \to A$ into an abelian group; I chose the canonical one.)