Galois invariants of a scalar extension

For a Galois extension L/k, the elements of L ⊗[k] A fixed by the scalar-factor action are precisely the tensors 1 ⊗ a. This identifies the original vector space inside its scalar extension, in arbitrary characteristic. An algebra morphism between scalar extensions therefore descends uniquely if and only if it commutes with the scalar-factor Galois action. This supplies the underlying algebra map for descent of coordinate bialgebra morphisms.

Main declarations

• TauCeti.GaloisDescent.tensorProduct_forall_map_eq_self_iff_exists_one_tmul_eq: the fixed tensors are exactly those coming from the original vector space.
• AlgHom.galoisDescend: descent of an equivariant algebra morphism.
• AlgHom.existsUnique_map_eq_iff: equivariance characterizes unique descent.

References

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

theorem TauCeti.GaloisDescent.tensorProduct_forall_map_eq_self_iff_exists_one_tmul_eq {k : Type u_1} {L : Type u_2} {A : Type u_3} [Field k] [Field L] [Algebra k L] [AddCommGroup A] [Module k A] [IsGalois k L] (x : TensorProduct k L A) : (∀ (σ : Gal(L/k)), (TensorProduct.map σ.toLinearMap LinearMap.id) x = x) ↔ ∃ (a : A), 1 ⊗ₜ[k] a = x

The fixed elements of a scalar extension along a Galois extension are exactly the image of the original vector space.

noncomputable def AlgHom.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] [Algebra k A] [Algebra k B] [IsGalois k L] (F : TensorProduct k L A →ₐ[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 →ₐ[k] B

Descent of an algebra morphism commuting with the scalar-factor Galois action. Its scalar extension is the original morphism.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgHom.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] [Algebra k A] [Algebra k B] [IsGalois k L] (F : TensorProduct k L A →ₐ[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)

The descended morphism is characterized on the original algebra inside its scalar extension.

@[simp]

theorem AlgHom.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] [Algebra k A] [Algebra k B] [IsGalois k L] (F : TensorProduct k L A →ₐ[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)) : Algebra.TensorProduct.map (AlgHom.id L L) (F.galoisDescend hF) = F

Extending a descended algebra morphism recovers the given equivariant morphism.

theorem AlgHom.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] [Algebra k A] [Algebra k B] [IsGalois k L] (F : TensorProduct k L A →ₐ[L] TensorProduct k L B) : (∃! f : A →ₐ[k] B, Algebra.TensorProduct.map (AlgHom.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)

An algebra morphism over a Galois extension descends uniquely exactly when it commutes with the scalar-factor Galois action.