In a topos ${\mathcal{A}}$, given a group object $G$ and a subgroup $H$, the object $H\backslash G$ of right cosets is the coequalizer of two maps $G\times H\rightrightarrows G$, namely the group multiplication and the projection onto $G$. Denote the coequalizing map by $H\backslash -$:
$$G\times H\rightrightarrows G\xrightarrow{H\backslash -}H\backslash G$$ 


Say that a map $f:X\to Y$ is a *product projection* if it is part of a span $Z\leftarrow X\xrightarrow{f} Y$ that writes $X$ as a product of $Y$ and $Z$. One can show that $H\backslash -:G\to H\backslash G$ has a section if and only if it is a product projection. If so, then in fact $G$ is the product of $H$ and $H\backslash G$:
$$G\simeq H\times H\backslash G$$


In the topos ${\mathcal{FinSet}}$ of finite sets, the external axiom of choice holds, which is to say that every epimorphism has a section. The map $H\backslash -$ is an epimorphism, hence has a section if $G$ is a finite group, hence $G\simeq H\times H\backslash G$. This is (a strong form of) Lagrange's theorem.


Say that a topos ${\mathcal{A}}$ *satisfies Lagrange's theorem* if, for each group object $G$ and a subgroup $H$, the map $H\backslash -:G\to H\backslash G$ has a section (or equivalently, is a product projection). ~~For example, the topos ${\mathcal{Top}}$ of topological spaces and continuous maps does not satisfy Lagrange's theorem as the Hopf fibration $S^1\to S^3\to S^2$ is a counterexample.~~ 


The external axiom of choice implies Lagrange's theorem. Hence the topos ${\mathcal{Set}}$ satisfies Lagrange's theorem. The internal axiom of choice, namely that exponentials $-^X:{\mathcal{A}}\to{\mathcal{A}}$ preserve epimorphisms, is weaker than the external axiom of choice. My question is:



> 
> Does there exist a topos that satisfies the internal axiom of choice but not Lagrange's theorem? 
> 
> 
> 



Does the internal axiom of choice imply Lagrange's theorem?
Consider the topos $\mathcal E$ of $\mathbb Z/2$-sets. It satisfies the internal axiom of choice but not the external one. The Klein four-group $(\mathbb Z/2)\times(\mathbb Z/2)$ admits an action of $\mathbb Z/2$, namely interchanging the two factors, which makes it an object of $\mathcal E$. Let $H$ be the diagonal subgroup, $\{(0,0),(1,1)\}$ and note that it is pointwise fixed by the $\mathbb Z/2$-action. The quotient $H\backslash G$ consists of two points, both of which are fixed by the $\mathbb Z/2$-action. Therefore, the product $H\times(H\backslash G)$ consists of four points, each fixed by the $\mathbb Z/2$-action. But $G$ has only two fixed-points, the other two points, namely $(0,1)$ and $(1,0)$, being interchanged by the action.


