Base change of bialgebras in stages

For a tower of commutative semirings k → L → K and a k-bialgebra H, extending H to L and then to K agrees with extending it to K in one step. This file upgrades the algebra equivalence TauCeti.Algebra.TensorProduct.baseChangeTowerAlgEquiv to a bialgebra equivalence

K ⊗[L] (L ⊗[k] H) ≃ₐc[K] K ⊗[k] H.

When H is commutative, contravariantly this is the statement that the geometric fibre of the affine monoid scheme represented by H — an affine group scheme when H is moreover a Hopf algebra — may be computed through an intermediate field: it is what lets a group split by a finite Galois extension be recognised over an algebraic closure.

Main declarations

• TauCeti.Bialgebra.TensorProduct.baseChangeTowerBialgEquiv: the tower comparison as a bialgebra equivalence.
• TauCeti.Bialgebra.TensorProduct.baseChangeTowerBialgEquiv_tmul: its value on nested pure tensors.
• TauCeti.Bialgebra.TensorProduct.baseChangeTowerBialgEquiv_symm_tmul: the value of its inverse on pure tensors.

References

• This formalization is adapted from the sibling comparison TauCeti.Bialgebra.TensorProduct.baseChangeTensorBialgEquiv between base change and tensor products.

noncomputable def TauCeti.Bialgebra.TensorProduct.baseChangeTowerBialgEquiv (k : Type u_1) (L : Type u_2) (H : Type u_3) (K : Type u_4) [CommSemiring k] [CommSemiring L] [Algebra k L] [CommSemiring K] [Algebra k K] [Algebra L K] [IsScalarTower k L K] [Semiring H] [Bialgebra k H] : TensorProduct L K (TensorProduct k L H) ≃ₐc[K] TensorProduct k K H

Base change of bialgebras composes in stages. For a tower k → L → K, extending a k-bialgebra H to L and then to K is extending it to K in one step.

The underlying algebra equivalence is TauCeti.Algebra.TensorProduct.baseChangeTowerAlgEquiv; the content added here is that it respects the counit and the comultiplication.

Equations

• TauCeti.Bialgebra.TensorProduct.baseChangeTowerBialgEquiv k L H K = BialgEquiv.ofAlgEquiv (TauCeti.Algebra.TensorProduct.baseChangeTowerAlgEquiv k L H K) ⋯ ⋯

@[simp]

theorem TauCeti.Bialgebra.TensorProduct.baseChangeTowerBialgEquiv_tmul (k : Type u_1) (L : Type u_2) (H : Type u_3) (K : Type u_4) [CommSemiring k] [CommSemiring L] [Algebra k L] [CommSemiring K] [Algebra k K] [Algebra L K] [IsScalarTower k L K] [Semiring H] [Bialgebra k H] (s : K) (l : L) (h : H) : (baseChangeTowerBialgEquiv k L H K) (s ⊗ₜ[L] (l ⊗ₜ[k] h)) = (l • s) ⊗ₜ[k] h

On a nested pure tensor, the tower comparison absorbs the intermediate scalar.

@[simp]

theorem TensorProduct.baseChangeTowerBialgEquiv_one_tmul (k : Type u_1) (L : Type u_2) (H : Type u_3) (K : Type u_4) [CommSemiring k] [CommSemiring L] [Algebra k L] [CommSemiring K] [Algebra k K] [Algebra L K] [IsScalarTower k L K] [Semiring H] [Bialgebra k H] (x : TensorProduct k L H) : (TauCeti.Bialgebra.TensorProduct.baseChangeTowerBialgEquiv k L H K) (1 ⊗ₜ[L] x) = (Algebra.TensorProduct.map (IsScalarTower.toAlgHom k L K) (AlgHom.id k H)) x

On a tensor with unit scalar, the tower comparison extends the intermediate coefficients.

@[simp]

theorem TauCeti.Bialgebra.TensorProduct.baseChangeTowerBialgEquiv_symm_tmul (k : Type u_1) (L : Type u_2) (H : Type u_3) (K : Type u_4) [CommSemiring k] [CommSemiring L] [Algebra k L] [CommSemiring K] [Algebra k K] [Algebra L K] [IsScalarTower k L K] [Semiring H] [Bialgebra k H] (s : K) (h : H) : (baseChangeTowerBialgEquiv k L H K).symm (s ⊗ₜ[k] h) = s ⊗ₜ[L] (1 ⊗ₜ[k] h)

The inverse tower comparison inserts the unit of the intermediate ring.