Naturality of base-changed points

This file records the two naturality properties of TauCeti.AlgHom.baseChangePointsMulEquiv. Base-changing a bialgebra from k to K identifies K-algebra maps out of K ⊗[k] A with k-algebra maps out of A; this identification is compatible with post-composition in the value algebra and with pre-composition by morphisms of coordinate bialgebras.

These lemmas are part of the ReductiveGroups roadmap Layer 0 base-change target: after the convolution group structure on points, the functor-of-points dictionary needs base change to behave naturally in both the value algebra and the coordinate Hopf algebra.

Worked examples of base-changed groups can combine these generic lemmas with the corresponding unbased points naturality calculation, avoiding duplicate example-specific wrappers around the same base-change argument.

Main declarations

• TauCeti.AlgHom.mapValue_baseChangePointsMulEquiv: base change of points commutes with post-composition in the value algebra.
• TauCeti.AlgHom.baseChangePointsMulEquiv_mapDomain: base change of points commutes with pre-composition in the coordinate bialgebra.

References

This builds on Mathlib's tensor-product bialgebra map Bialgebra.TensorProduct.map, Mathlib's algebra base-change adjunction AlgHom.liftEquiv, and the Tau Ceti convolution-points API in TauCeti.Algebra.AlgebraicGroup.BaseChange.Basic and TauCeti.Algebra.AlgebraicGroup.Hopf.Map.

theorem TauCeti.AlgHom.mapValue_baseChangePointsMulEquiv {k : Type u_1} {K : Type u_2} {A : Type u_3} {R : Type u_4} {S : Type u_5} [CommSemiring k] [CommSemiring K] [Semiring A] [CommSemiring R] [CommSemiring S] [Algebra k K] [Bialgebra k A] [Algebra K R] [Algebra k R] [IsScalarTower k K R] [Algebra K S] [Algebra k S] [IsScalarTower k K S] (φ : R →ₐ[K] S) (f : WithConv (A →ₐ[k] R)) : (mapValue φ) (baseChangePointsMulEquiv f) = baseChangePointsMulEquiv ((mapValue (AlgHom.restrictScalars k φ)) f)

Base change of points is natural in the value algebra.

Post-composing an R-valued point by a K-algebra homomorphism φ : R →ₐ[K] S and then base-changing agrees with first base-changing the point and then post-composing by φ.

theorem TauCeti.AlgHom.baseChangePointsMulEquiv_symm_mapValue {k : Type u_1} {K : Type u_2} {A : Type u_3} {R : Type u_4} {S : Type u_5} [CommSemiring k] [CommSemiring K] [Semiring A] [CommSemiring R] [CommSemiring S] [Algebra k K] [Bialgebra k A] [Algebra K R] [Algebra k R] [IsScalarTower k K R] [Algebra K S] [Algebra k S] [IsScalarTower k K S] (φ : R →ₐ[K] S) (f : WithConv (TensorProduct k K A →ₐ[K] R)) : baseChangePointsMulEquiv.symm ((mapValue φ) f) = (mapValue (AlgHom.restrictScalars k φ)) (baseChangePointsMulEquiv.symm f)

The inverse direction of base change is natural in the value algebra.

Restricting a post-composed base-changed point along a ↦ 1 ⊗ a agrees with post-composing the restricted point.

theorem TauCeti.AlgHom.baseChangePointsMulEquiv_mapDomain {k : Type u_1} {K : Type u_2} {A : Type u_3} {B : Type u_4} {R : Type u_5} [CommSemiring k] [CommSemiring K] [Algebra k K] [CommSemiring A] [Semiring B] [Bialgebra k A] [Bialgebra k B] [CommSemiring R] [Algebra K R] [Algebra k R] [IsScalarTower k K R] (φ : A →ₐc[k] B) (f : WithConv (B →ₐ[k] R)) : baseChangePointsMulEquiv ((mapDomain φ) f) = (mapDomain (Bialgebra.TensorProduct.map (BialgHom.id K K) φ)) (baseChangePointsMulEquiv f)

Base change of points is natural in the coordinate bialgebra.

Pre-composing a B-point by a bialgebra morphism φ : A →ₐc[k] B and then base-changing agrees with first base-changing the point and then pre-composing by the scalar extension K ⊗[k] A →ₐc[K] K ⊗[k] B.

@[simp]

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

Pointwise form of AlgHom.baseChangePointsMulEquiv_mapDomain on pure tensors.

theorem TauCeti.AlgHom.baseChangePointsMulEquiv_symm_mapDomain {k : Type u_1} {K : Type u_2} {A : Type u_3} {B : Type u_4} {R : Type u_5} [CommSemiring k] [CommSemiring K] [Algebra k K] [CommSemiring A] [Semiring B] [Bialgebra k A] [Bialgebra k B] [CommSemiring R] [Algebra K R] [Algebra k R] [IsScalarTower k K R] (φ : A →ₐc[k] B) (f : WithConv (TensorProduct k K B →ₐ[K] R)) : baseChangePointsMulEquiv.symm ((mapDomain (Bialgebra.TensorProduct.map (BialgHom.id K K) φ)) f) = (mapDomain φ) (baseChangePointsMulEquiv.symm f)

The inverse direction of base change is natural in the coordinate bialgebra.

Restricting along a ↦ 1 ⊗ a after pre-composing with the scalar extension of φ agrees with first restricting and then pre-composing by φ.

@[simp]

theorem TauCeti.AlgHom.baseChangePointsMulEquiv_symm_mapDomain_apply {k : Type u_1} {K : Type u_2} {A : Type u_3} {B : Type u_4} {R : Type u_5} [CommSemiring k] [CommSemiring K] [Algebra k K] [CommSemiring A] [Semiring B] [Bialgebra k A] [Bialgebra k B] [CommSemiring R] [Algebra K R] [Algebra k R] [IsScalarTower k K R] (φ : A →ₐc[k] B) (f : WithConv (TensorProduct k K B →ₐ[K] R)) (a : A) : (baseChangePointsMulEquiv.symm ((mapDomain (Bialgebra.TensorProduct.map (BialgHom.id K K) φ)) f)).ofConv a = f.ofConv (1 ⊗ₜ[k] φ a)

Pointwise form of AlgHom.baseChangePointsMulEquiv_symm_mapDomain.