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\)
Comments