Example. internal inhabitation without a global point [fgap-000T]
Example. internal inhabitation without a global point [fgap-000T]
Work in \(\mathsf {B}C_2\), the topos of right \(C_2\)-sets, and let \(U=C_2\) carry the regular right action. The unique equivariant map \(U\to 1\) is an epimorphism because its underlying function is surjective. In the internal language, this says that \(U\) is inhabited. Internal Group Actions are developed in [maclane1992sheaves, sec. V.2, pp. 237--240].
A global element would be an equivariant map \(1\to U\). Its value would have to satisfy \(u\mathbin {\cdot }s=u\), but the regular action has no fixed point. Hence \[ \operatorname {Hom}_{\mathsf {B}C_2}(1,U)=\varnothing . \] The two external tests are: \[ \begin {array}{c|c} \text {internal statement}&\text {external test}\\ \hline U\text { is inhabited}&U\to 1\text { is epi}\\ U\text { has a global point}&U^{C_2}\neq \varnothing . \end {array} \]
More generally, for a nontrivial group \(G\), the regular right \(G\)-object \(U_G=G\) satisfies \[ U_G\to 1\text { is epi}, \qquad \Gamma (U_G)=U_G^G=\varnothing . \] Indeed, if \(xg=x\) for every \(g\), cancellation forces every \(g\) to be \(1\). Internal existence is therefore generalized or local existence; it does not choose a global invariant element. This distinction is not a physical existence claim.