Inner conjugation on the functor of points

An R-valued point of a Hopf algebra acts on its algebra-valued points by conjugation after extension to the value algebra. This action is a group automorphism, natural in the value algebra, and respects identity, multiplication, and inversion of the conjugating point.

For conjugation by an arbitrary point over a fixed value algebra, use MulAut.conj and its application lemmas MulAut.conj_apply and MulAut.conj_symm_apply. The natural automorphism below specializes this group construction to the extensions of one R-valued point, so that its components are compatible with maps of value algebras.

Main declarations

• TauCeti.HopfAlgebra.innerConjugationPointNatIso: the natural automorphism of the functor of points, for an arbitrary semiring Hopf algebra.

References

• J. S. Milne, Algebraic Groups (2017), §§3.5 and 10.20.
• A. Borel, Linear Algebraic Groups, 2nd ed. (1991), §8.
• The Tau Ceti contributors, prior formalization of inner conjugation, TauCeti#5490, commit 8419e7ceed8e87e7a14be030b7a0dda52aea2d41.

noncomputable def TauCeti.HopfAlgebra.innerConjugationPointNatIso {R : Type u} [CommRing R] (H : Type w) [Semiring H] [HopfAlgebra R H] (g : ↑(points ↧R)) : pointsFunctor ≅ pointsFunctor

Conjugation by an R-valued point, naturally on the full functor of points.

Equations

• TauCeti.HopfAlgebra.innerConjugationPointNatIso H g = CategoryTheory.NatIso.ofComponents (fun (A : CommAlgCat R) => MulEquiv.toGrpIso (MulAut.conj ((TauCeti.HopfAlgebra.extendPoint H A) g))) ⋯

@[simp]

theorem TauCeti.HopfAlgebra.innerConjugationPointNatIso_hom_app_apply {R : Type u} [CommRing R] (H : Type w) [Semiring H] [HopfAlgebra R H] (g : ↑(points ↧R)) (A : CommAlgCat R) (x : ↑(points A)) : (CategoryTheory.ConcreteCategory.hom ((innerConjugationPointNatIso H g).hom.app A)) x = (extendPoint H A) g * x * ((extendPoint H A) g)⁻¹

The forward component of the natural inner-conjugation isomorphism acts by conjugation.

@[simp]

theorem TauCeti.HopfAlgebra.innerConjugationPointNatIso_inv_app_apply {R : Type u} [CommRing R] (H : Type w) [Semiring H] [HopfAlgebra R H] (g : ↑(points ↧R)) (A : CommAlgCat R) (x : ↑(points A)) : (CategoryTheory.ConcreteCategory.hom ((innerConjugationPointNatIso H g).inv.app A)) x = ((extendPoint H A) g)⁻¹ * x * (extendPoint H A) g

The inverse component of the natural inner-conjugation isomorphism acts by conjugation by the inverse extended point.

@[simp]

theorem TauCeti.HopfAlgebra.innerConjugationPointNatIso_one {R : Type u} [CommRing R] (H : Type w) [Semiring H] [HopfAlgebra R H] : innerConjugationPointNatIso H 1 = CategoryTheory.Iso.refl pointsFunctor

Conjugation by the identity point is the identity automorphism of the functor of points.

@[simp]

theorem TauCeti.HopfAlgebra.innerConjugationPointNatIso_mul {R : Type u} [CommRing R] (H : Type w) [Semiring H] [HopfAlgebra R H] (g h : ↑(points ↧R)) : innerConjugationPointNatIso H (g * h) = innerConjugationPointNatIso H h ≪≫ innerConjugationPointNatIso H g

Conjugation by a product is successive conjugation, first by the second point and then by the first.

@[simp]

theorem TauCeti.HopfAlgebra.innerConjugationPointNatIso_inv_point {R : Type u} [CommRing R] (H : Type w) [Semiring H] [HopfAlgebra R H] (g : ↑(points ↧R)) : innerConjugationPointNatIso H g⁻¹ = (innerConjugationPointNatIso H g).symm

Conjugation by an inverse point is inverse to conjugation by the original point.