The two-dimensional special orthogonal group

Over a commutative ring containing an element i with i ^ 2 = -1 and a chosen half, the special orthogonal group of the standard form in dimension two is the unit group. The equivalence sends

!![a, b; -b, a] to the unit a + i * b.

This is the elementary matrix form of the splitness of the even-dimensional standard orthogonal group in rank one. Keeping the explicit formulas available is useful when a one-parameter family in SO₂ must be evaluated over a Laurent polynomial ring.

Main declaration

• Matrix.SpecialOrthogonalGroup.finTwoMulEquivUnits: the explicit equivalence SO₂(R) ≃* Rˣ.

References

• J. S. Milne, Algebraic Groups (2017), §18.c.

noncomputable def Matrix.SpecialOrthogonalGroup.finTwoToUnit {R : Type u_1} [CommRing R] (i : R) (hi : i ^ 2 = -1) (M : ↥(specialOrthogonalGroup (Fin 2) R)) : Rˣ

The unit determined by a two-dimensional special orthogonal matrix.

Equations

• Matrix.SpecialOrthogonalGroup.finTwoToUnit i hi M = { val := ↑M 0 0 + i * ↑M 0 1, inv := ↑M 0 0 - i * ↑M 0 1, val_inv := ⋯, inv_val := ⋯ }

@[simp]

theorem Matrix.SpecialOrthogonalGroup.coe_finTwoToUnit {R : Type u_1} [CommRing R] (i : R) (hi : i ^ 2 = -1) (M : ↥(specialOrthogonalGroup (Fin 2) R)) : ↑(finTwoToUnit i hi M) = ↑M 0 0 + i * ↑M 0 1

The underlying value of the unit determined by a two-dimensional special orthogonal matrix.

@[simp]

theorem Matrix.SpecialOrthogonalGroup.coe_inv_finTwoToUnit {R : Type u_1} [CommRing R] (i : R) (hi : i ^ 2 = -1) (M : ↥(specialOrthogonalGroup (Fin 2) R)) : ↑(finTwoToUnit i hi M)⁻¹ = ↑M 0 0 - i * ↑M 0 1

The inverse of the unit determined by a two-dimensional special orthogonal matrix.

noncomputable def Matrix.SpecialOrthogonalGroup.finTwoOfUnit {R : Type u_1} [CommRing R] (i half : R) (hi : i ^ 2 = -1) (hhalf : 2 * half = 1) (u : Rˣ) : ↥(specialOrthogonalGroup (Fin 2) R)

The two-dimensional special orthogonal matrix determined by a unit.

Equations

• Matrix.SpecialOrthogonalGroup.finTwoOfUnit i half hi hhalf u = ⟨!![half * (↑u + ↑u⁻¹), -i * half * (↑u - ↑u⁻¹); -(-i * half * (↑u - ↑u⁻¹)), half * (↑u + ↑u⁻¹)], ⋯⟩

@[simp]

theorem Matrix.SpecialOrthogonalGroup.coe_finTwoOfUnit {R : Type u_1} [CommRing R] (i half : R) (hi : i ^ 2 = -1) (hhalf : 2 * half = 1) (u : Rˣ) : ↑(finTwoOfUnit i half hi hhalf u) = !![half * (↑u + ↑u⁻¹), -i * half * (↑u - ↑u⁻¹); -(-i * half * (↑u - ↑u⁻¹)), half * (↑u + ↑u⁻¹)]

The underlying matrix determined by a unit, in terms of the unit and its inverse.

@[simp]

theorem Matrix.SpecialOrthogonalGroup.finTwoToUnit_finTwoOfUnit {R : Type u_1} [CommRing R] (i half : R) (hi : i ^ 2 = -1) (hhalf : 2 * half = 1) (u : Rˣ) : finTwoToUnit i hi (finTwoOfUnit i half hi hhalf u) = u

Extracting the unit from its two-dimensional special orthogonal matrix recovers the unit.

@[simp]

theorem Matrix.SpecialOrthogonalGroup.finTwoOfUnit_finTwoToUnit {R : Type u_1} [CommRing R] (i half : R) (hi : i ^ 2 = -1) (hhalf : 2 * half = 1) (M : ↥(specialOrthogonalGroup (Fin 2) R)) : finTwoOfUnit i half hi hhalf (finTwoToUnit i hi M) = M

Reconstructing a two-dimensional special orthogonal matrix from its unit recovers the matrix.

theorem Matrix.SpecialOrthogonalGroup.finTwoToUnit_mul {R : Type u_1} [CommRing R] (i : R) (hi : i ^ 2 = -1) (M N : ↥(specialOrthogonalGroup (Fin 2) R)) : finTwoToUnit i hi (M * N) = finTwoToUnit i hi M * finTwoToUnit i hi N

Multiplication of two-dimensional special orthogonal matrices becomes multiplication of their associated units.

theorem Matrix.SpecialOrthogonalGroup.map_finTwoOfUnit {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) (i half : R) (hi : i ^ 2 = -1) (hhalf : 2 * half = 1) (u : Rˣ) : (map f) (finTwoOfUnit i half hi hhalf u) = finTwoOfUnit (f i) (f half) ⋯ ⋯ ((Units.map ↑f) u)

The two-dimensional matrix attached to a unit is natural under ring homomorphisms.

theorem Matrix.SpecialOrthogonalGroup.finTwoToUnit_map {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (f : R →+* S) (i : R) (hi : i ^ 2 = -1) (M : ↥(specialOrthogonalGroup (Fin 2) R)) : finTwoToUnit (f i) ⋯ ((map f) M) = (Units.map ↑f) (finTwoToUnit i hi M)

The unit attached to a two-dimensional matrix is natural under ring homomorphisms.

noncomputable def Matrix.SpecialOrthogonalGroup.finTwoMulEquivUnits {R : Type u_1} [CommRing R] (i half : R) (hi : i ^ 2 = -1) (hhalf : 2 * half = 1) : ↥(specialOrthogonalGroup (Fin 2) R) ≃* Rˣ

Over a commutative ring containing a square root of -1 and a half, the standard two-dimensional special orthogonal group is the group of units.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Matrix.SpecialOrthogonalGroup.finTwoMulEquivUnits_apply {R : Type u_1} [CommRing R] (i half : R) (hi : i ^ 2 = -1) (hhalf : 2 * half = 1) (M : ↥(specialOrthogonalGroup (Fin 2) R)) : (finTwoMulEquivUnits i half hi hhalf) M = finTwoToUnit i hi M

The explicit equivalence from two-dimensional special orthogonal matrices to units is given by finTwoToUnit.

@[simp]

theorem Matrix.SpecialOrthogonalGroup.finTwoMulEquivUnits_symm_apply {R : Type u_1} [CommRing R] (i half : R) (hi : i ^ 2 = -1) (hhalf : 2 * half = 1) (u : Rˣ) : (finTwoMulEquivUnits i half hi hhalf).symm u = finTwoOfUnit i half hi hhalf u

The inverse of the explicit equivalence from two-dimensional special orthogonal matrices to units is given by finTwoOfUnit.

@[simp]

theorem Matrix.SpecialOrthogonalGroup.finTwoOfUnit_one {R : Type u_1} [CommRing R] (i half : R) (hi : i ^ 2 = -1) (hhalf : 2 * half = 1) : finTwoOfUnit i half hi hhalf 1 = 1

The unit 1 determines the identity two-dimensional special orthogonal matrix.