Galois descent of bialgebra morphisms

A morphism between scalar-extended bialgebras over a Galois extension descends uniquely if and only if it commutes with the Galois action on the scalar factor. The descended algebra morphism preserves the counit and comultiplication, since these identities can be checked after the injective scalar extension. For Hopf algebras, antipode compatibility then follows from the usual bialgebra-morphism theorem.

This permits descent of morphisms between affine groups from equivariant morphisms over a splitting field, without first identifying their coordinate algebras with invariant group algebras. Neither finite type nor commutativity of the bialgebras is required.

Main declarations

• BialgHom.galoisDescend: descent of an equivariant bialgebra morphism.
• BialgHom.map_galoisDescend: scalar extension recovers the original morphism.
• BialgHom.existsUnique_map_eq_iff: equivariance characterizes unique descent.

References

• J. S. Milne, Algebraic Groups (2017), Appendix A.64.

noncomputable def BialgHom.galoisDescend {k : Type u_1} {L : Type u_2} {A : Type u_3} {B : Type u_4} [Field k] [Field L] [Algebra k L] [Semiring A] [Semiring B] [Bialgebra k A] [Bialgebra k B] [IsGalois k L] (F : TensorProduct k L A →ₐc[L] TensorProduct k L B) (hF : ∀ (σ : Gal(L/k)) (x : TensorProduct k L A), F ((TensorProduct.map σ.toLinearMap LinearMap.id) x) = (TensorProduct.map σ.toLinearMap LinearMap.id) (F x)) : A →ₐc[k] B

Descent of a bialgebra morphism commuting with the scalar-factor Galois action. Counit and comultiplication compatibility descend along with the algebra map.

Equations

• F.galoisDescend hF = BialgHom.ofAlgHom ((↑F).galoisDescend hF) ⋯ ⋯

@[simp]

theorem BialgHom.galoisDescend_toAlgHom {k : Type u_1} {L : Type u_2} {A : Type u_3} {B : Type u_4} [Field k] [Field L] [Algebra k L] [Semiring A] [Semiring B] [Bialgebra k A] [Bialgebra k B] [IsGalois k L] (F : TensorProduct k L A →ₐc[L] TensorProduct k L B) (hF : ∀ (σ : Gal(L/k)) (x : TensorProduct k L A), F ((TensorProduct.map σ.toLinearMap LinearMap.id) x) = (TensorProduct.map σ.toLinearMap LinearMap.id) (F x)) : ↑(F.galoisDescend hF) = (↑F).galoisDescend hF

The algebra map underlying bialgebra descent is algebra descent.

@[simp]

theorem BialgHom.one_tmul_galoisDescend {k : Type u_1} {L : Type u_2} {A : Type u_3} {B : Type u_4} [Field k] [Field L] [Algebra k L] [Semiring A] [Semiring B] [Bialgebra k A] [Bialgebra k B] [IsGalois k L] (F : TensorProduct k L A →ₐc[L] TensorProduct k L B) (hF : ∀ (σ : Gal(L/k)) (x : TensorProduct k L A), F ((TensorProduct.map σ.toLinearMap LinearMap.id) x) = (TensorProduct.map σ.toLinearMap LinearMap.id) (F x)) (a : A) : 1 ⊗ₜ[k] (F.galoisDescend hF) a = F (1 ⊗ₜ[k] a)

Descent recovers the given map on elements of the original bialgebra.

@[simp]

theorem BialgHom.map_galoisDescend {k : Type u_1} {L : Type u_2} {A : Type u_3} {B : Type u_4} [Field k] [Field L] [Algebra k L] [Semiring A] [Semiring B] [Bialgebra k A] [Bialgebra k B] [IsGalois k L] (F : TensorProduct k L A →ₐc[L] TensorProduct k L B) (hF : ∀ (σ : Gal(L/k)) (x : TensorProduct k L A), F ((TensorProduct.map σ.toLinearMap LinearMap.id) x) = (TensorProduct.map σ.toLinearMap LinearMap.id) (F x)) : Bialgebra.TensorProduct.map (BialgHom.id L L) (F.galoisDescend hF) = F

Extending a descended bialgebra morphism recovers the original morphism.

theorem BialgHom.existsUnique_map_eq_iff {k : Type u_1} {L : Type u_2} {A : Type u_3} {B : Type u_4} [Field k] [Field L] [Algebra k L] [Semiring A] [Semiring B] [Bialgebra k A] [Bialgebra k B] [IsGalois k L] (F : TensorProduct k L A →ₐc[L] TensorProduct k L B) : (∃! f : A →ₐc[k] B, Bialgebra.TensorProduct.map (BialgHom.id L L) f = F) ↔ ∀ (σ : Gal(L/k)) (x : TensorProduct k L A), F ((TensorProduct.map σ.toLinearMap LinearMap.id) x) = (TensorProduct.map σ.toLinearMap LinearMap.id) (F x)

A bialgebra morphism over a Galois extension descends uniquely exactly when it commutes with the scalar-factor Galois action. In particular this applies to coordinate Hopf algebras of affine group schemes.