Conjugation by a rational point

A rational point g of an affine group scheme acts on the group by the inner automorphism x ↦ g * x * g⁻¹. Contravariantly, this file constructs the corresponding automorphism of the coordinate Hopf algebra. Its characteristic lemma describes precomposition on points, and the bialgebra structure records that inner automorphisms are group homomorphisms.

This is the coordinate-algebra operation needed to formulate conjugacy of closed subgroup schemes, in particular conjugacy of Borel subgroups and maximal tori.

Main declarations

• TauCeti.HopfAlgebra.pointConjugationBialgEquiv: the coordinate Hopf-algebra automorphism induced by conjugation by a rational point.
• TauCeti.HopfAlgebra.mapDomain_pointConjugationBialgEquiv: its action on arbitrary algebra-valued points is group-theoretic conjugation.
• TauCeti.HopfAlgebra.pointConjugationFiniteTypeIso: the same automorphism as an isomorphism in the category of finite-type commutative Hopf algebras.

References

• J. S. Milne, Algebraic Groups (2017), Sections 3.5 and 10.20.
• T. A. Springer, Linear Algebraic Groups, Section 6.2.

noncomputable def TauCeti.HopfAlgebra.pointConjugationAlgHom {R : Type u} [CommSemiring R] {H : Type v} [CommSemiring H] [HopfAlgebra R H] (g : WithConv (H →ₐ[R] R)) : H →ₐ[R] H

Pullback on the coordinate algebra by conjugation by an R-valued point.

Equations

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

theorem TauCeti.HopfAlgebra.toConv_pointConjugationAlgHom {R : Type u} [CommSemiring R] {H : Type v} [CommSemiring H] [HopfAlgebra R H] (g : WithConv (H →ₐ[R] R)) : WithConv.toConv (pointConjugationAlgHom g) = (AlgHom.mapValue (Algebra.ofId R H)) g * WithConv.toConv (AlgHom.id R H) * ((AlgHom.mapValue (Algebra.ofId R H)) g)⁻¹

Point conjugation is the specialization of the universal conjugation morphism at the conjugating rational point.

theorem TauCeti.HopfAlgebra.comp_pointConjugationAlgHom {R : Type u} [CommSemiring R] {H : Type v} [CommSemiring H] [HopfAlgebra R H] {A : Type w} [CommSemiring A] [Algebra R A] (g : WithConv (H →ₐ[R] R)) (x : WithConv (H →ₐ[R] A)) : WithConv.toConv (x.ofConv.comp (pointConjugationAlgHom g)) = (AlgHom.mapValue (Algebra.ofId R A)) g * x * ((AlgHom.mapValue (Algebra.ofId R A)) g)⁻¹

Precomposition by point conjugation is group-theoretic conjugation by the corresponding constant point.

@[simp]

theorem TauCeti.HopfAlgebra.pointConjugationAlgHom_one {R : Type u} [CommSemiring R] {H : Type v} [CommSemiring H] [HopfAlgebra R H] : pointConjugationAlgHom 1 = AlgHom.id R H

Conjugation by the identity point is the identity coordinate map.

theorem TauCeti.HopfAlgebra.pointConjugationAlgHom_mul {R : Type u} [CommSemiring R] {H : Type v} [CommSemiring H] [HopfAlgebra R H] (g h : WithConv (H →ₐ[R] R)) : pointConjugationAlgHom (g * h) = (pointConjugationAlgHom h).comp (pointConjugationAlgHom g)

Coordinate maps for point conjugation compose in the order forced by contravariance.

noncomputable def TauCeti.HopfAlgebra.pointConjugationBialgEquiv {R : Type u} [CommSemiring R] {H : Type v} [CommSemiring H] [HopfAlgebra R H] (g : WithConv (H →ₐ[R] R)) : H ≃ₐc[R] H

Conjugation by a rational point as a bialgebra automorphism of the coordinate Hopf algebra.

Equations

• TauCeti.HopfAlgebra.pointConjugationBialgEquiv g = BialgEquiv.ofBijective (BialgHom.ofAlgHom (TauCeti.HopfAlgebra.pointConjugationAlgHom g) ⋯ ⋯) ⋯

@[simp]

theorem TauCeti.HopfAlgebra.pointConjugationBialgEquiv_toAlgHom {R : Type u} [CommSemiring R] {H : Type v} [CommSemiring H] [HopfAlgebra R H] (g : WithConv (H →ₐ[R] R)) : ↑↑(pointConjugationBialgEquiv g) = pointConjugationAlgHom g

The bialgebra equivalence underlying point conjugation has the expected algebra map.

theorem TauCeti.HopfAlgebra.mapDomain_pointConjugationBialgEquiv {R : Type u} [CommSemiring R] {H : Type v} [CommSemiring H] [HopfAlgebra R H] {A : Type w} [CommSemiring A] [Algebra R A] (g : WithConv (H →ₐ[R] R)) (x : WithConv (H →ₐ[R] A)) : (AlgHom.mapDomain (pointConjugationBialgEquiv g).toBialgHom) x = (AlgHom.mapValue (Algebra.ofId R A)) g * x * ((AlgHom.mapValue (Algebra.ofId R A)) g)⁻¹

Pulling back an algebra-valued point by the bialgebra automorphism of point conjugation conjugates it by the corresponding constant point.

noncomputable def TauCeti.HopfAlgebra.pointConjugationFiniteTypeIso {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] [Algebra.FiniteType R H] (g : WithConv (H →ₐ[R] R)) : FiniteTypeCommHopfAlgCat.of R H ≅ FiniteTypeCommHopfAlgCat.of R H

Conjugation by a rational point as an automorphism of the coordinate Hopf algebra in the category of finite-type commutative Hopf algebras.

This is the categorical packaging of pointConjugationBialgEquiv, used to transport isomorphism-invariant properties of closed subgroup schemes along conjugation.

Equations

• TauCeti.HopfAlgebra.pointConjugationFiniteTypeIso g = (TauCeti.finiteTypeCommHopfAlgProperty R).isoMk (CommHopfAlgCat.isoMk (TauCeti.HopfAlgebra.pointConjugationBialgEquiv g))

@[simp]

theorem TauCeti.HopfAlgebra.pointConjugationFiniteTypeIso_hom {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] [Algebra.FiniteType R H] (g : WithConv (H →ₐ[R] R)) : FiniteTypeCommHopfAlgCat.toBialgHom (pointConjugationFiniteTypeIso g).hom = (pointConjugationBialgEquiv g).toBialgHom

The underlying bialgebra map of the finite-type point-conjugation isomorphism is the point-conjugation bialgebra equivalence.

theorem BialgHom.comp_pointConjugationAlgHom_mapDomain_of_isCocomm {R : Type u_1} {H : Type u_2} {K : Type u_3} [CommSemiring R] [CommSemiring H] [CommSemiring K] [HopfAlgebra R H] [HopfAlgebra R K] [Coalgebra.IsCocomm R K] (π : H →ₐc[R] K) (t : WithConv (K →ₐ[R] R)) : (↑π).comp (TauCeti.HopfAlgebra.pointConjugationAlgHom ((TauCeti.AlgHom.mapDomain π) t)) = ↑π

A point coming from a commutative affine group centralizes that group's image, scheme-theoretically: conjugation restricts to the identity coordinate map.