Demo of SO(2, ℝ) as a non-split torus

In this file, we construct SO(2, R) as a group scheme for an arbitrary commutative ring R, and show that SO(2, ℂ) is a split torus while SO(2, ℝ) isn't, which implies that SO(2, ℝ) is a non-split torus.

SO(2, R) as a Hopf algebra

@[reducible, inline]

abbrev SO2Ring (R : Type u_1) [CommRing R] : Type u_1

The ring whose spectrum is SO(2, R), defined as R[X, Y] / ⟨X ^ 2 + Y ^ 2 - 1⟩.

Equations

• SO2Ring R = AdjoinRoot (Polynomial.X ^ 2 + Polynomial.C Polynomial.X ^ 2 - 1)

instance SO2Ring.instCommRing {R : Type u_1} [CommRing R] : CommRing (SO2Ring R)

Equations

• SO2Ring.instCommRing = id inferInstance

instance SO2Ring.instAlgebra {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] : Algebra R (SO2Ring S)

Equations

• SO2Ring.instAlgebra = id inferInstance

instance SO2Ring.instIsScalarTower {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] : IsScalarTower R S (SO2Ring S)

def SO2Ring.mk {R : Type u_1} [CommRing R] : Polynomial (Polynomial R) →ₐ[R] SO2Ring R

The quotient map from R[X, Y] to SO2Ring R.

Equations

• SO2Ring.mk = Ideal.Quotient.mkₐ R (Ideal.span {Polynomial.X ^ 2 + Polynomial.C Polynomial.X ^ 2 - 1})

def SO2Ring.X {R : Type u_1} [CommRing R] : SO2Ring R

X as an element of SO2Ring R.

Equations

• SO2Ring.X = SO2Ring.mk Polynomial.X

def SO2Ring.Y {R : Type u_1} [CommRing R] : SO2Ring R

Y as an element of SO2Ring R.

Equations

• SO2Ring.Y = SO2Ring.mk (Polynomial.C Polynomial.X)

@[simp]

theorem SO2Ring.X_def {R : Type u_1} [CommRing R] : mk Polynomial.X = X

@[simp]

theorem SO2Ring.Y_def {R : Type u_1} [CommRing R] : mk (Polynomial.C Polynomial.X) = Y

def SO2Ring.liftₐ {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (x y : S) (H : x ^ 2 + y ^ 2 = 1) : SO2Ring R →ₐ[R] S

Lift two elements of S with squares summing to 1 to an algebra hom from SO2Ring R to S.

Equations

• SO2Ring.liftₐ x y H = Ideal.Quotient.liftₐ (Ideal.span {Polynomial.X ^ 2 + Polynomial.C Polynomial.X ^ 2 - 1}) (Polynomial.aevalAEval x y) ⋯

@[simp]

theorem SO2Ring.liftₐ_X {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (x y : S) (H : x ^ 2 + y ^ 2 = 1) : (liftₐ x y H) X = x

@[simp]

theorem SO2Ring.liftₐ_Y {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] (x y : S) (H : x ^ 2 + y ^ 2 = 1) : (liftₐ x y H) Y = y

@[simp]

theorem SO2Ring.relation {R : Type u_1} [CommRing R] : X ^ 2 + Y ^ 2 = 1

theorem SO2Ring.relation' {R : Type u_1} [CommRing R] : X ^ 2 = 1 - Y ^ 2

@[simp]

theorem SO2Ring.relation'' {R : Type u_1} [CommRing R] : X * X + Y * Y = 1

theorem SO2Ring.algebraMap_ext {R : Type u_1} [CommRing R] {A : Type u_3} [Semiring A] [Algebra R A] {f g : SO2Ring R →ₐ[R] A} (h1 : f X = g X) (h2 : f Y = g Y) : f = g

theorem SO2Ring.algebraMap_ext_iff {R : Type u_1} [CommRing R] {A : Type u_3} [Semiring A] [Algebra R A] {f g : SO2Ring R →ₐ[R] A} : f = g ↔ f X = g X ∧ f Y = g Y

def SO2Ring.comulAlgHom {R : Type u_1} [CommRing R] : SO2Ring R →ₐ[R] TensorProduct R (SO2Ring R) (SO2Ring R)

The comultiplication on SO2Ring R, given by X ↦ X ⊗ X - Y ⊗ Y, Y ↦ X ⊗ Y + Y ⊗ X.

Equations

• SO2Ring.comulAlgHom = SO2Ring.liftₐ (SO2Ring.X ⊗ₜ[R] SO2Ring.X - SO2Ring.Y ⊗ₜ[R] SO2Ring.Y) (SO2Ring.X ⊗ₜ[R] SO2Ring.Y + SO2Ring.Y ⊗ₜ[R] SO2Ring.X) ⋯

@[simp]

theorem SO2Ring.comulAlgHom_apply_X {R : Type u_1} [CommRing R] : comulAlgHom X = X ⊗ₜ[R] X - Y ⊗ₜ[R] Y

@[simp]

theorem SO2Ring.comulAlgHom_apply_Y {R : Type u_1} [CommRing R] : comulAlgHom Y = X ⊗ₜ[R] Y + Y ⊗ₜ[R] X

def SO2Ring.counitAlgHom {R : Type u_1} [CommRing R] : SO2Ring R →ₐ[R] R

The counit on SO2Ring R, given by X ↦ 1, Y ↦ 0.

Equations

• SO2Ring.counitAlgHom = SO2Ring.liftₐ 1 0 ⋯

@[simp]

theorem SO2Ring.counitAlgHom.apply_X {R : Type u_1} [CommRing R] : counitAlgHom X = 1

@[simp]

theorem SO2Ring.counitAlgHom.apply_Y {R : Type u_1} [CommRing R] : counitAlgHom Y = 0

instance SO2Ring.instBialgebra {R : Type u_1} [CommRing R] : Bialgebra R (SO2Ring R)

Equations

• SO2Ring.instBialgebra = Bialgebra.ofAlgHom SO2Ring.comulAlgHom SO2Ring.counitAlgHom ⋯ ⋯ ⋯

@[simp]

theorem SO2Ring.comul_def {R : Type u_1} [CommRing R] : CoalgebraStruct.comul = ↑comulAlgHom

@[simp]

theorem SO2Ring.counit_def {R : Type u_1} [CommRing R] : CoalgebraStruct.counit = ↑counitAlgHom

def SO2Ring.antipodeAlgHom {R : Type u_1} [CommRing R] : SO2Ring R →ₐ[R] SO2Ring R

The comultiplication on SO2Ring R, given by X ↦ X, Y ↦ -Y.

Equations

• SO2Ring.antipodeAlgHom = SO2Ring.liftₐ SO2Ring.X (-SO2Ring.Y) ⋯

@[simp]

theorem SO2Ring.antipodeAlgHom_X {R : Type u_1} [CommRing R] : antipodeAlgHom X = X

@[simp]

theorem SO2Ring.antipodeAlgHom_Y {R : Type u_1} [CommRing R] : antipodeAlgHom Y = -Y

instance SO2Ring.instHopfAlgebra {R : Type u_1} [CommRing R] : HopfAlgebra R (SO2Ring R)

Equations

• SO2Ring.instHopfAlgebra = HopfAlgebra.ofAlgHom SO2Ring.antipodeAlgHom ⋯ ⋯

@[simp]

theorem SO2Ring.antipode_X {R : Type u_1} [CommRing R] : (HopfAlgebraStruct.antipode R) X = X

@[simp]

theorem SO2Ring.antipode_Y {R : Type u_1} [CommRing R] : (HopfAlgebraStruct.antipode R) Y = -Y

SO(2, ℂ)

def SO2Ring.T : GroupLike ℂ (SO2Ring ℂ)

The group-like element X + iY of SO2Ring ℂ.

Equations

• SO2Ring.T = { val := SO2Ring.X + Complex.I • SO2Ring.Y, isGroupLikeElem_val := SO2Ring.T._proof_2 }

@[simp]

theorem SO2Ring.T_val : ↑T = X + Complex.I • Y

def SO2Ring.complexEquiv : SO2Ring ℂ ≃ₐc[ℂ] AddMonoidAlgebra ℂ ℤ

SO2Ring ℂ is isomorphic to Laurent series ℂ[ℤ].

Equations

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

@[simp]

theorem SO2Ring.complexEquiv_inv_single (a : ℤ) (b : ℂ) : complexEquiv.symm (AddMonoidAlgebra.single a b) = b • ↑(T ^ a)

@[simp]

theorem SO2Ring.complexEquiv_inv_C (b : ℂ) : complexEquiv.symm (LaurentPolynomial.C b) = (algebraMap ℂ (SO2Ring ℂ)) b

@[simp]

theorem SO2Ring.complexEquiv_symm_comp_algebraMap : (↑complexEquiv.symm).comp (algebraMap ℂ (AddMonoidAlgebra ℂ ℤ)) = algebraMap ℂ (SO2Ring ℂ)

R-points of SO(2, R)

def SO2Ring.algHomMulEquiv {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] : (SO2Ring R →ₐ[R] S) ≃* ↥(Matrix.specialOrthogonalGroup (Fin 2) S)

The isomorphism between the R-algebra homomorphisms from SO2Ring(R) to S and the group SO(2,S).

Equations

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

Base change

instance SO2Ring.instAlgebraTensorProduct {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] : Algebra S (TensorProduct R S (SO2Ring R))

Equations

• SO2Ring.instAlgebraTensorProduct = Algebra.TensorProduct.leftAlgebra

def SO2Ring.baseChangeAlgEquiv (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] : TensorProduct R S (SO2Ring R) ≃ₐ[S] SO2Ring S

SO2Ring is invariant under base change of algebras.

Equations

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

@[simp]

theorem SO2Ring.baseChangeAlgEquiv_X {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] : (baseChangeAlgEquiv R S) (1 ⊗ₜ[R] X) = X

@[simp]

theorem SO2Ring.baseChangeAlgEquiv_Y {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] : (baseChangeAlgEquiv R S) (1 ⊗ₜ[R] Y) = Y

def SO2Ring.baseChangeBialgEquiv (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] : TensorProduct R S (SO2Ring R) ≃ₐc[S] SO2Ring S

SO2Ring is invariant under base change of bialgebras.

Equations

• SO2Ring.baseChangeBialgEquiv R S = BialgEquiv.ofAlgEquiv (SO2Ring.baseChangeAlgEquiv R S) ⋯ ⋯

@[simp]

theorem SO2Ring.coe_baseChangeBialgEquiv {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] : ⇑(baseChangeBialgEquiv R S) = ⇑(baseChangeAlgEquiv R S)

theorem SO2Ring.baseChangeBialgEquiv_comp_algebraMap {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] : (↑(baseChangeBialgEquiv R S)).comp (Algebra.ofId S (TensorProduct R S (SO2Ring R))) = Algebra.ofId S (SO2Ring S)

SO(2, R) as a scheme

def AlgebraicGeometry.SO₂.«termSO₂(_)» : Lean.ParserDescr

Notation for the special orghogonal group of 2x2 matrices as a scheme.

Equations

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

SO(2, ℂ) is a split torus

def AlgebraicGeometry.SO₂.so₂ComplexIso : Spec (CommRingCat.of (SO2Ring ℂ)) ≅ (Spec (CommRingCat.of ℂ)).Diag ℤ

The isomorphism between SO₂(ℂ) and the 1-dimensional ℂ-torus.

Equations

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

@[simp]

theorem AlgebraicGeometry.SO₂.so₂ComplexIso_hom : so₂ComplexIso.hom = CategoryTheory.CategoryStruct.comp ((bialgSpec (CommRingCat.of ℂ)).map (CommBialgCat.ofHom SO2Ring.complexEquiv.symm.toBialgHom).op).hom.left (Scheme.diagSpecIso (CommRingCat.of ℂ) ℤ).inv

@[simp]

theorem AlgebraicGeometry.SO₂.so₂ComplexIso_inv : so₂ComplexIso.inv = CategoryTheory.CategoryStruct.comp (Scheme.diagSpecIso (CommRingCat.of ℂ) ℤ).hom ((bialgSpec (CommRingCat.of ℂ)).map (CommBialgCat.ofHom SO2Ring.complexEquiv.toBialgHom).op).hom.left

instance AlgebraicGeometry.SO₂.instIsOverHomSchemeSo₂ComplexIsoSpecOfComplex : Scheme.Hom.IsOver so₂ComplexIso.hom (Spec (CommRingCat.of ℂ))

theorem AlgebraicGeometry.SO₂.so₂ComplexIso_hom_asOver : Scheme.Hom.asOver so₂ComplexIso.hom (Spec (CommRingCat.of ℂ)) = CategoryTheory.CategoryStruct.comp ((bialgSpec (CommRingCat.of ℂ)).map (CommBialgCat.ofHom SO2Ring.complexEquiv.symm.toBialgHom).op).hom (Scheme.Hom.asOver (Scheme.diagSpecIso (CommRingCat.of ℂ) ℤ).inv (Spec (CommRingCat.of ℂ)))

instance AlgebraicGeometry.SO₂.instIsMonHomOverSchemeSpecOfComplexAsOverHomSo₂ComplexIso : IsMonHom (Scheme.Hom.asOver so₂ComplexIso.hom (Spec (CommRingCat.of ℂ)))

instance AlgebraicGeometry.SO₂.instIsSplitTorusOverSpecOfSO2RingComplex : (Spec (CommRingCat.of (SO2Ring ℂ))).IsSplitTorusOver (Spec (CommRingCat.of ℂ))

SO(2, ℝ) is a torus

def AlgebraicGeometry.SO₂.pullbackSO₂RealComplex : CategoryTheory.Limits.pullback (Spec (CommRingCat.of (SO2Ring ℝ)) ↘ Spec (CommRingCat.of ℝ)) (Spec (CommRingCat.of ℂ) ↘ Spec (CommRingCat.of ℝ)) ≅ Spec (CommRingCat.of (SO2Ring ℂ))

The isomorphism between the base change of SO₂(ℝ) to ℂ and SO₂(ℂ).

Equations

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

@[simp]

theorem AlgebraicGeometry.SO₂.pullbackSO₂RealComplex_hom : pullbackSO₂RealComplex.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry (Spec (CommRingCat.of (SO2Ring ℝ)) ↘ Spec (CommRingCat.of ℝ)) (Spec (CommRingCat.of ℂ) ↘ Spec (CommRingCat.of ℝ)) ≪≫ Scheme.pullbackSpecIso' ℝ ℂ (SO2Ring ℝ)).hom ((bialgSpec (CommRingCat.of ℂ)).map (CommBialgCat.ofHom (SO2Ring.baseChangeBialgEquiv ℝ ℂ).symm.toBialgHom).op).hom.left

instance AlgebraicGeometry.SO₂.instIsOverHomSchemePullbackSO₂RealComplexSpecOfComplex : Scheme.Hom.IsOver pullbackSO₂RealComplex.hom (Spec (CommRingCat.of ℂ))

theorem AlgebraicGeometry.SO₂.pullbackSO₂RealComplex_hom_asOver : Scheme.Hom.asOver pullbackSO₂RealComplex.hom (Spec (CommRingCat.of ℂ)) = CategoryTheory.CategoryStruct.comp (Scheme.Hom.asOver (CategoryTheory.Limits.pullbackSymmetry (Spec (CommRingCat.of (SO2Ring ℝ)) ↘ Spec (CommRingCat.of ℝ)) (Spec (CommRingCat.of ℂ) ↘ Spec (CommRingCat.of ℝ)) ≪≫ Scheme.pullbackSpecIso' ℝ ℂ (SO2Ring ℝ)).hom (Spec (CommRingCat.of ℂ))) ((bialgSpec (CommRingCat.of ℂ)).map (CommBialgCat.ofHom (SO2Ring.baseChangeBialgEquiv ℝ ℂ).symm.toBialgHom).op).hom

instance AlgebraicGeometry.SO₂.instIsMonHomOverSchemeSpecOfComplexAsOverHomPullbackSO₂RealComplex : IsMonHom (Scheme.Hom.asOver pullbackSO₂RealComplex.hom (Spec (CommRingCat.of ℂ)))

instance AlgebraicGeometry.SO₂.pullback_SO₂_real_isSplitTorusOver_complex : (CategoryTheory.Limits.pullback (Spec (CommRingCat.of (SO2Ring ℝ)) ↘ Spec (CommRingCat.of ℝ)) (Spec (CommRingCat.of ℂ) ↘ Spec (CommRingCat.of ℝ))).IsSplitTorusOver (Spec (CommRingCat.of ℂ))

instance AlgebraicGeometry.SO₂.instIsTorusOverRealSpecOfSO2Ring : Scheme.IsTorusOver ℝ (Spec (CommRingCat.of (SO2Ring ℝ)))

SO(2) is a torus over the reals.

SO(2, ℝ) is not split

def AlgebraicGeometry.SO₂.pointsMulEquiv (R : Type u_1) [CommRing R] : ((Spec (CommRingCat.of R)).asOver (Spec (CommRingCat.of R)) ⟶ (Spec (CommRingCat.of (SO2Ring R))).asOver (Spec (CommRingCat.of R))) ≃* ↥(Matrix.specialOrthogonalGroup (Fin 2) R)

The R-points of SO₂(R) as a group R-scheme are isomorphic to the group SO(2, R).

Equations

• AlgebraicGeometry.SO₂.pointsMulEquiv R = AlgebraicGeometry.Scheme.Spec.mulEquiv.symm.trans SO2Ring.algHomMulEquiv

def AlgebraicGeometry.SO₂.I : ↥(Matrix.specialOrthogonalGroup (Fin 2) ℝ)

A 4-torsion element of SO(2, ℝ).

Equations

• AlgebraicGeometry.SO₂.I = ⟨!![0, 1; -1, 0], AlgebraicGeometry.SO₂.I._proof_1⟩

theorem AlgebraicGeometry.SO₂.I_sq_ne_1 : I ^ 2 ≠ 1

@[simp]

theorem AlgebraicGeometry.SO₂.I_ord_4' : I ^ 4 = 1

theorem AlgebraicGeometry.SO₂.not_isSplitTorusOver_SO₂_real : ¬(Spec (CommRingCat.of (SO2Ring ℝ))).IsSplitTorusOver (Spec (CommRingCat.of ℝ))

SO(2) is not a split torus over the real numbers.