Special orthogonal groups in ranks zero and one

The standard special orthogonal groups SO₀ and SO₁ are trivial over every commutative base ring. In Hopf coordinates, their defining ideals agree with the corresponding special-linear ideals. In rank zero there are no orthogonality relations. In rank one, the single relation x² - 1 is a multiple of the determinant-one relation x - 1.

The resulting equality identifies the finite-type coordinate Hopf algebras with those of SL₀ and SL₁. Since the special linear groups are reductive in every rank and characteristic, this settles reductivity of the two low-rank special orthogonal groups without a hypothesis on 2.

Main declarations

• TauCeti.SpecialOrthogonal.definingHopfIdeal_zero: the rank-zero defining ideal agrees with the special-linear ideal.
• TauCeti.SpecialOrthogonal.definingHopfIdeal_one: the rank-one defining ideal agrees with the special-linear ideal.
• TauCeti.SpecialOrthogonal.reductiveCommHopfAlgProperty_finiteTypeCoordinateHopfAlgebra_zero and TauCeti.SpecialOrthogonal.reductiveCommHopfAlgProperty_finiteTypeCoordinateHopfAlgebra_one: SO₀ and SO₁ are reductive over every field.

References

• J. S. Milne, Algebraic Groups (2017), §§2.3 and 21, for the standard orthogonal groups and reductivity.

@[simp]

theorem TauCeti.SpecialOrthogonal.definingHopfIdeal_zero (R : Type u) [CommRing R] : definingHopfIdeal R 0 = SpecialLinear.definingHopfIdeal R 0

In rank zero the special-orthogonal and special-linear defining Hopf ideals agree.

@[simp]

theorem TauCeti.SpecialOrthogonal.definingHopfIdeal_one (R : Type u) [CommRing R] : definingHopfIdeal R 1 = SpecialLinear.definingHopfIdeal R 1

In rank one the special-orthogonal and special-linear defining Hopf ideals agree.

@[simp]

theorem TauCeti.SpecialOrthogonal.finiteTypeCoordinateHopfAlgebra_zero (R : Type u) [CommRing R] : finiteTypeCoordinateHopfAlgebra R 0 = SpecialLinear.finiteTypeCoordinateHopfAlgebra R 0

The finite-type coordinate Hopf algebra of SO₀ is the one of SL₀.

@[simp]

theorem TauCeti.SpecialOrthogonal.finiteTypeCoordinateHopfAlgebra_one (R : Type u) [CommRing R] : finiteTypeCoordinateHopfAlgebra R 1 = SpecialLinear.finiteTypeCoordinateHopfAlgebra R 1

The finite-type coordinate Hopf algebra of SO₁ is the one of SL₁.

theorem TauCeti.SpecialOrthogonal.reductiveCommHopfAlgProperty_finiteTypeCoordinateHopfAlgebra_zero (k : Type u) [Field k] : reductiveCommHopfAlgProperty k (finiteTypeCoordinateHopfAlgebra k 0)

The rank-zero special orthogonal group is reductive over every field.

theorem TauCeti.SpecialOrthogonal.reductiveCommHopfAlgProperty_finiteTypeCoordinateHopfAlgebra_one (k : Type u) [Field k] : reductiveCommHopfAlgProperty k (finiteTypeCoordinateHopfAlgebra k 1)

The rank-one special orthogonal group is reductive over every field.