# O(2) as a semidirect product

It is a simple linear algebra exercise to show that $$O(n)$$, the group of orthogonal $$n × n$$ real matrices, is the semidirect product of its subgroup $$SO(n)$$, consisting of matrices of determinant 1, and the cyclic group $$C_2$$ on two elements.

In other words, there is a short exact sequence of Lie groups $1 → SO(n) → O(n) → O(1) → 1,$ where the map $$O(n) → O(1)$$ is the determinant, and this sequence splits through any homomorphism $$O(1) → O(n)$$ that maps $$-1$$ to a reflection.

We can replicate this construction in HoTT, but unfortunately only for the case $$n = 2$$, where, thanks to some fortuitous coincidences, we can obtain (the homotopy types of) the Lie groups above and their deloopings.

First, let $$\mathsf{Aut}(F)$$ denote the automorphism group of a type $$F$$, i.e. the type $$F ≅ F$$. If $$F : \mathcal{U}$$, where $$\mathcal{U}$$ is a univalent universe, then we can define a delooping of $$\mathsf{Aut}(F)$$ simply as the connected component of $$F$$ in $$\mathcal{U}$$, i.e. $B\mathsf{Aut}(F) = (X : \mathcal{U}) × \| X = F \|.$

Now we can define: $\begin{array}{l} O(1) :≡ \mathsf{Aut}(\underline{2}), \\ O(2) :≡ \mathsf{Aut}(S¹). \\ \end{array}$

The first definition is justified by the fact that $$O(1)$$ is the discrete group with two elements, which is isomorphic to the permutation group $$Σ_2 ≡ \mathsf{Aut}(\underline{2})$$.

As for the second, consider the function $$(S^1 → S^1) → S^1$$ that maps a function to its value on the base point. One can show that the fibres of this map form the constant $$ℤ$$ family. So $$(S^1 → S^1) ≅ S^1 × ℤ$$, where composition acts like multiplication on the second component. It follows that $$\mathsf{Aut}(S^1) ≅ S^1 × ℤ^* ≅ S^1 × \mathsf{Aut}(\underline{2})$$. This argument shows that the inclusion $$O(2) → \mathsf{Aut}(S^1)$$ is a homotopy equivalence in spaces, which justifies our definition.

To replicate the exact sequence above in type theory, we have to construct it at the level of deloopings. Let $$p: \mathcal{U}→ \mathcal{U}$$ be defined by $p(X) :≡ \| X = S¹ \|_0.$ It follows from the above calculations of $$\mathsf{Aut}(S¹)$$ that $$p(S¹) = \underline{2}$$. Therefore, $$p$$ maps the connected component of $$S¹$$ to the connected component of $$\underline{2}$$, hence it defines a function $$p: BO(2) → BO(1)$$. Define $$BSO(2)$$ to be the fibre of $$p$$.

Lemma 1. For $$A : BO(1)$$, there is an equivalence $$(\underline{2} = A) ≅ A$$.

Proof. Let $$ϕ_A : (\underline{2} = A) → A$$ be defined by $$ϕ_A(α) = α(0)$$, where we are implicitly regarding an element of $$\underline{2} = A$$ as an equivalence. Since $$ϕ_{\underline{2}}$$ is obviously an equivalence, it follows that $$ϕ_A$$ is an equivalence for all $$A$$ in the connected component of $$\underline{2}$$.$$\square$$

Proposition 2. The map $$\| BO(2) \|_1 → BO(1)$$ induced by $$p$$ is an equivalence.

Proof. Since both types are connected, it is enough to show that the induced map on the loop spaces is an equivalence. For any $$X : BO(2)$$, let $$ϕ: (X = S^1) → p(X)$$ be the map obtained by composing $$\mathsf{ap}_p: (X = S^1) → (p(X) = p(S¹))$$ with the equivalence $$(p(X) = p(S¹)) → p(X)$$ given by Lemma 1, and using the fact that $$p(S¹) = \underline{2}$$. We will show that $$ϕ$$ is equal to the canonical projection into the 0-truncation.

By path elimination, it is enough to show that the reflexivity path $$S^1 = S^1$$ is mapped to its image in the 0-truncation, which follows immediately from expanding the definitions.

In particular, the map $$p(X) → p(X)$$ induced by $$ϕ$$ is an equivalence, hence $$\mathsf{ap}_p$$ is an equivalence by 2-out-of-3.$$\square$$

Corollary 3. Ω(BSO(2)) ≅ S¹

Proof. By identifying $$Ω\| BO(2) \|$$ with $$ΩBO(1) = \underline{2}$$, we get that the map induced by $$p$$ on the loop spaces is equivalent to the second projection $$S¹ × \underline{2} → \underline{2}$$. In particular, its fibre is $$S¹$$. The conclusion then follows from the long exact sequence of homotopy groups.$$\square$$

So we have the desired fibre sequence $$BSO(2) → BO(2) → BO(1)$$. To show that our definition of $$BSO(2)$$ matches what we have in spaces, there is one more subtle point that we need to address. We only showed that the loop space of $$BSO(2)$$ is equivalent to $$S¹$$ as a space, but a priori there could be another ∞-group structure on $$S¹$$, corresponding to another delooping. Fortunately, though, $$S¹$$ is the Eilenberg-MacLane space $$K(ℤ, 1)$$, hence any delooping of it must be a $$K(ℤ, 2)$$, which means that there is exactly one. In particular, $$BSO(2)$$ as we defined it is a possible model for the infinite dimensional complex projective space, another one being what arises from the type-theory construction of Eilenberg-MacLane spaces, namely $$\| S² \|_2$$.

The fibre sequence $$BSO(2) → BO(2) → BO(1)$$ gives rise to an exact sequence of $$∞$$-groups $$SO(2) → O(2) → O(1)$$. Such a sequence splits if and only if the second map has a section.

Since the suspension of $$\underline{2}$$ is equivalent to $$S^1$$, suspension can be regarded as a pointed map $$Σ : BO(1) → BO(2)$$. As usual, we will denote by $$\mathsf{merid}: A → N = S$$ the path constructor in the definition of the suspension $$Σ A$$, and take the north pole $$N$$ as the base point of $$Σ A$$.

Proposition 4. The suspension map $$Σ: BO(1) → BO(2)$$ is a section of $$p: BO(2) → BO(1)$$.

Proof. For any type $$A$$ in $$BO(1)$$, let $$σ_A : A → A$$ be the only non-identity equivalence of $$A$$, and define a function $$ψ_A : A → S^1 → ΣA$$ so that $$ψ_A(a)$$ corresponds to the loop $$\mathsf{merid}(a) · \mathsf{merid}(σ_A(a))^{-1}$$.

Then for all $$A : BO(1)$$, and all $$a: A$$, $$ψ_A(a)$$ is an equivalence, since this is true for $$A ≡ \underline{2}$$, and being an equivalence is a proposition. We have thus defined a map $$A → (S¹ ≅ ΣA)$$, hence in particular a map $$A → \| S^1 ≅ ΣA \|_0$$. It is easy to verify that the latter map is an equivalence for $$A ≡ 2$$, which implies that it is an equivalence for all $$A : BO(1)$$. This shows that $$Σ$$ is a section of $$p$$, concluding the proof.$$\square$$