Base change of bialgebra points

This file records that the usual algebraic base-change adjunction is compatible with the convolution monoid structure on the functor of points of a bialgebra. For a bialgebra A over k, a k-algebra K, and a commutative K-algebra R, the R-points of the base-changed bialgebra K ⊗[k] A over K are the same as k-algebra maps A →ₐ[k] R, and this identification is a monoid isomorphism for convolution. When A is a Hopf algebra, these are the convolution groups of points.

This is the algebraic-group-facing form of the ReductiveGroups roadmap item "Base change. K ⊗[k] A as a Hopf algebra over K"; it builds on Mathlib's tensor-product bialgebra instance, Mathlib's tensor-product Hopf algebra antipode formula, and AlgHom.liftEquiv.

Main definitions

• TauCeti.AlgHom.baseChangePointsMulEquiv: the convolution monoid isomorphism between A →ₐ[k] R and K ⊗[k] A →ₐ[K] R. When A is a Hopf algebra these are convolution groups, so this is automatically an isomorphism of groups.
• TauCeti.AlgHom.baseChangePointsMulEquiv_inv_apply_tmul and TauCeti.AlgHom.baseChangePointsMulEquiv_symm_inv_apply: pointwise formulas for convolution inverses of base-changed points.

References

The tensor-product bialgebra and Hopf-algebra structures and algebra base-change adjunction used here are from Mathlib, respectively Mathlib.RingTheory.Bialgebra.TensorProduct, Mathlib.RingTheory.HopfAlgebra.TensorProduct, and AlgHom.liftEquiv.

noncomputable def TauCeti.AlgHom.baseChangePointsMulEquiv {k : Type u_1} {K : Type u_2} {A : Type u_3} {R : Type u_4} [CommSemiring k] [CommSemiring K] [Semiring A] [CommSemiring R] [Algebra k K] [Bialgebra k A] [Algebra K R] [Algebra k R] [IsScalarTower k K R] : WithConv (A →ₐ[k] R) ≃* WithConv (TensorProduct k K A →ₐ[K] R)

Base change of bialgebra points is a monoid isomorphism for the convolution product.

The forward direction sends f : A →ₐ[k] R to s ⊗ a ↦ s • f a; the inverse restricts a K-algebra map K ⊗[k] A →ₐ[K] R along a ↦ 1 ⊗ a.

Equations

• TauCeti.AlgHom.baseChangePointsMulEquiv = { toEquiv := WithConv.congr (AlgHom.liftEquiv k K A R), map_mul' := ⋯ }

@[simp]

theorem TauCeti.AlgHom.baseChangePointsMulEquiv_apply_ofConv {k : Type u_1} {K : Type u_2} {A : Type u_3} {R : Type u_4} [CommSemiring k] [CommSemiring K] [Semiring A] [CommSemiring R] [Algebra k K] [Bialgebra k A] [Algebra K R] [Algebra k R] [IsScalarTower k K R] (f : WithConv (A →ₐ[k] R)) : (baseChangePointsMulEquiv f).ofConv = (AlgHom.liftEquiv k K A R) f.ofConv

The base-change convolution-monoid isomorphism sends f to s ⊗ a ↦ s • f a.

@[simp]

theorem TauCeti.AlgHom.baseChangePointsMulEquiv_symm_ofConv {k : Type u_1} {K : Type u_2} {A : Type u_3} {R : Type u_4} [CommSemiring k] [CommSemiring K] [Semiring A] [CommSemiring R] [Algebra k K] [Bialgebra k A] [Algebra K R] [Algebra k R] [IsScalarTower k K R] (f : WithConv (TensorProduct k K A →ₐ[K] R)) : (baseChangePointsMulEquiv.symm f).ofConv = (AlgHom.liftEquiv k K A R).symm f.ofConv

The inverse base-change convolution-monoid isomorphism is restriction along A → K ⊗[k] A.

@[simp]

theorem TauCeti.AlgHom.baseChangePointsMulEquiv_apply_tmul {k : Type u_1} {K : Type u_2} {A : Type u_3} {R : Type u_4} [CommSemiring k] [CommSemiring K] [Semiring A] [CommSemiring R] [Algebra k K] [Bialgebra k A] [Algebra K R] [Algebra k R] [IsScalarTower k K R] (f : WithConv (A →ₐ[k] R)) (s : K) (a : A) : (baseChangePointsMulEquiv f).ofConv (s ⊗ₜ[k] a) = s • f.ofConv a

The base-change convolution-monoid isomorphism sends f to s ⊗ a ↦ s • f a.

@[simp]

theorem TauCeti.AlgHom.baseChangePointsMulEquiv_symm_apply {k : Type u_1} {K : Type u_2} {A : Type u_3} {R : Type u_4} [CommSemiring k] [CommSemiring K] [Semiring A] [CommSemiring R] [Algebra k K] [Bialgebra k A] [Algebra K R] [Algebra k R] [IsScalarTower k K R] (f : WithConv (TensorProduct k K A →ₐ[K] R)) (a : A) : (baseChangePointsMulEquiv.symm f).ofConv a = f.ofConv (1 ⊗ₜ[k] a)

The inverse of the base-change convolution-monoid isomorphism restricts along a ↦ 1 ⊗ a.

@[simp]

theorem TauCeti.AlgHom.baseChangePointsMulEquiv_inv_apply_tmul {k : Type u_1} {K : Type u_2} {A : Type u_3} {R : Type u_4} [CommSemiring k] [CommSemiring K] [Semiring A] [CommSemiring R] [Algebra k K] [HopfAlgebra k A] [Algebra K R] [Algebra k R] [IsScalarTower k K R] (f : WithConv (A →ₐ[k] R)) (s : K) (a : A) : (baseChangePointsMulEquiv f)⁻¹.ofConv (s ⊗ₜ[k] a) = s • f.ofConv ((HopfAlgebraStruct.antipode k) a)

Pointwise inverse formula after base change: on a pure tensor s ⊗ a, the convolution inverse of a base-changed point has value s • f (S a).

The ≃* AlgHom.baseChangePointsMulEquiv is automatically a group isomorphism here, since A is a Hopf algebra; this records the value of an inverse point on pure tensors.

@[simp]

theorem TauCeti.AlgHom.baseChangePointsMulEquiv_symm_inv_apply {k : Type u_1} {K : Type u_2} {A : Type u_3} {R : Type u_4} [CommSemiring k] [CommSemiring K] [Semiring A] [CommSemiring R] [Algebra k K] [HopfAlgebra k A] [Algebra K R] [Algebra k R] [IsScalarTower k K R] (f : WithConv (TensorProduct k K A →ₐ[K] R)) (a : A) : (baseChangePointsMulEquiv.symm f)⁻¹.ofConv a = f.ofConv (1 ⊗ₜ[k] (HopfAlgebraStruct.antipode k) a)

Pointwise inverse formula after restricting a base-changed point along a ↦ 1 ⊗ a: the inverse of (e.symm f) has value f (1 ⊗ S a) at a.