Documentation

TauCeti.Algebra.AlgebraicGroup.SpecialOrthogonal.Torus

The two-dimensional special orthogonal torus #

Suppose a commutative ring R contains a square root i of -1 and an element half with 2 * half = 1. The standard special orthogonal group SO₂ is then the rank-one split torus. On points, the identification sends a torus coordinate u to

half * (u + u⁻¹)       -i * half * (u - u⁻¹)
i * half * (u - u⁻¹)   half * (u + u⁻¹).

The pointwise equivalence is natural in the value algebra. Full faithfulness of the functor of points therefore recovers an isomorphism between the coordinate Hopf algebra of the rank-one split torus and O(SO₂). Over a field of characteristic different from two, an algebraic closure contains the required square root, so SO₂ is a (possibly non-split) one-dimensional torus over the original field. In particular it is reductive.

Main declarations #

References #

source
noncomputable def TauCeti.SpecialOrthogonal.splitTorusPointsMulEquiv (R : Type u) [CommRing R] (i half : R) (hi : i ^ 2 = -1) (hhalf : 2 * half = 1) (A : Type v) [CommRing A] [Algebra R A] :
WithConv (↑(DiagonalizableGroup.coordinateRing R (SplitTorus.characterGroup (ULift.{u, 0} (Fin 1)))).obj →ₐ[R] A) ≃* WithConv (↑(coordinateHopfAlgebra R 2) →ₐ[R] A)

The points of the rank-one split torus are naturally the points of SO₂ when the base contains a square root of -1 and a half.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.SpecialOrthogonal.splitTorusPointsMulEquiv_apply (R : Type u) [CommRing R] (i half : R) (hi : i ^ 2 = -1) (hhalf : 2 * half = 1) (A : Type v) [CommRing A] [Algebra R A] (t : WithConv (↑(DiagonalizableGroup.coordinateRing R (SplitTorus.characterGroup (ULift.{u, 0} (Fin 1)))).obj →ₐ[R] A)) :
    (splitTorusPointsMulEquiv R i half hi hhalf A) t = (pointsMulEquiv R 2).symm (Matrix.SpecialOrthogonalGroup.finTwoOfUnit ((algebraMap R A) i) ((algebraMap R A) half) ⋯ ⋯ (SplitTorus.pointsMulEquiv t default))

    The split-torus point equivalence sends a point to the point represented by the two-dimensional special orthogonal matrix attached to its unique unit coordinate.

    source
    @[simp]
    theorem TauCeti.SpecialOrthogonal.splitTorusPointsMulEquiv_symm_apply (R : Type u) [CommRing R] (i half : R) (hi : i ^ 2 = -1) (hhalf : 2 * half = 1) (A : Type v) [CommRing A] [Algebra R A] (s : WithConv (↑(coordinateHopfAlgebra R 2) →ₐ[R] A)) :
    (splitTorusPointsMulEquiv R i half hi hhalf A).symm s = SplitTorus.pointsMulEquiv.symm fun (x : ULift.{u, 0} (Fin 1)) => Matrix.SpecialOrthogonalGroup.finTwoToUnit ((algebraMap R A) i) ⋯ ((pointsMulEquiv R 2) s)

    The inverse split-torus point equivalence reads off the unit of a two-dimensional special orthogonal matrix and makes it the unique split-torus coordinate.

    source
    theorem TauCeti.SpecialOrthogonal.splitTorusPointsMulEquiv_mapValue (R : Type u) [CommRing R] (i half : R) (hi : i ^ 2 = -1) (hhalf : 2 * half = 1) {A B : Type v} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (t : WithConv (↑(DiagonalizableGroup.coordinateRing R (SplitTorus.characterGroup (ULift.{u, 0} (Fin 1)))).obj →ₐ[R] A)) :
    (AlgHom.mapValue f) ((splitTorusPointsMulEquiv R i half hi hhalf A) t) = (splitTorusPointsMulEquiv R i half hi hhalf B) ((AlgHom.mapValue f) t)

    The rank-one split-torus point equivalence is natural in the commutative value algebra.

    source
    noncomputable def TauCeti.SpecialOrthogonal.splitTorusPointsNatIso (R : Type u) [CommRing R] (i half : R) (hi : i ^ 2 = -1) (hhalf : 2 * half = 1) :
    HopfAlgebra.pointsFunctor ≅ HopfAlgebra.pointsFunctor

    The natural isomorphism between the group-valued functors of points of the rank-one split torus and SO₂.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.SpecialOrthogonal.splitTorusPointsNatIso_hom_app_apply (R : Type u) [CommRing R] (i half : R) (hi : i ^ 2 = -1) (hhalf : 2 * half = 1) (A : CommAlgCat R) (t : ↑(HopfAlgebra.points A)) :
      (CategoryTheory.ConcreteCategory.hom ((splitTorusPointsNatIso R i half hi hhalf).hom.app A)) t = (splitTorusPointsMulEquiv R i half hi hhalf ↑A) t

      The forward component of the natural split-torus identification is the pointwise equivalence splitTorusPointsMulEquiv.

      source
      @[simp]
      theorem TauCeti.SpecialOrthogonal.splitTorusPointsNatIso_inv_app_apply (R : Type u) [CommRing R] (i half : R) (hi : i ^ 2 = -1) (hhalf : 2 * half = 1) (A : CommAlgCat R) (s : ↑(HopfAlgebra.points A)) :
      (CategoryTheory.ConcreteCategory.hom ((splitTorusPointsNatIso R i half hi hhalf).inv.app A)) s = (splitTorusPointsMulEquiv R i half hi hhalf ↑A).symm s

      The inverse component of the natural split-torus identification is the inverse pointwise equivalence splitTorusPointsMulEquiv.

      source
      noncomputable def TauCeti.SpecialOrthogonal.splitTorusCoordinateIso (R : Type u) [CommRing R] (i half : R) (hi : i ^ 2 = -1) (hhalf : 2 * half = 1) :
      (DiagonalizableGroup.coordinateRing R (SplitTorus.characterGroup (ULift.{u, 0} (Fin 1)))).obj ≅ coordinateHopfAlgebra R 2

      The coordinate Hopf algebra of SO₂ is the coordinate Hopf algebra of the rank-one split torus when the base contains a square root of -1 and a half.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TauCeti.SpecialOrthogonal.mapPointsFunctor_splitTorusCoordinateIso_hom_app_apply (R : Type u) [CommRing R] (i half : R) (hi : i ^ 2 = -1) (hhalf : 2 * half = 1) (A : CommAlgCat R) (s : ↑(HopfAlgebra.points A)) :
        (CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (splitTorusCoordinateIso R i half hi hhalf).hom).app A)) s = (splitTorusPointsMulEquiv R i half hi hhalf ↑A).symm s

        On every value algebra, the point map induced by the forward coordinate isomorphism is the inverse pointwise split-torus equivalence.

        source
        @[simp]
        theorem TauCeti.SpecialOrthogonal.mapPointsFunctor_splitTorusCoordinateIso_inv_app_apply (R : Type u) [CommRing R] (i half : R) (hi : i ^ 2 = -1) (hhalf : 2 * half = 1) (A : CommAlgCat R) (t : ↑(HopfAlgebra.points A)) :
        (CategoryTheory.ConcreteCategory.hom ((CommHopfAlgCat.mapPointsFunctor (splitTorusCoordinateIso R i half hi hhalf).inv).app A)) t = (splitTorusPointsMulEquiv R i half hi hhalf ↑A) t

        On every value algebra, the point map induced by the inverse coordinate isomorphism is the forward pointwise split-torus equivalence.

        source
        noncomputable def TauCeti.SpecialOrthogonal.finiteTypeSplitTorusCoordinateIso (R : Type u) [CommRing R] (i half : R) (hi : i ^ 2 = -1) (hhalf : 2 * half = 1) :
        DiagonalizableGroup.coordinateRing R (SplitTorus.characterGroup (ULift.{u, 0} (Fin 1))) ≅ finiteTypeCoordinateHopfAlgebra R 2

        The finite-type coordinate Hopf algebra of SO₂ is isomorphic to the standard rank-one split-torus coordinate Hopf algebra under the same splitting hypotheses.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem TauCeti.SpecialOrthogonal.splitTorusCommHopfAlgProperty_finiteTypeCoordinateHopfAlgebra_two (R : Type u) [CommRing R] (i half : R) (hi : i ^ 2 = -1) (hhalf : 2 * half = 1) :
          splitTorusCommHopfAlgProperty R (finiteTypeCoordinateHopfAlgebra R 2)

          When the base contains a square root of -1 and a half, SO₂ is a split torus of rank one.

          source
          theorem TauCeti.SpecialOrthogonal.torusCommHopfAlgProperty_finiteTypeCoordinateHopfAlgebra_two (k : Type u) [Field k] [NeZero 2] :
          torusCommHopfAlgProperty k (finiteTypeCoordinateHopfAlgebra k 2)

          The standard two-dimensional special orthogonal group is a torus over every field of characteristic different from two. It need not be split over the ground field.

          source
          theorem TauCeti.SpecialOrthogonal.reductiveCommHopfAlgProperty_finiteTypeCoordinateHopfAlgebra_two (k : Type u) [Field k] [NeZero 2] :
          reductiveCommHopfAlgProperty k (finiteTypeCoordinateHopfAlgebra k 2)

          The standard two-dimensional special orthogonal group is reductive over every field of characteristic different from two.