Documentation

TauCeti.Algebra.AlgebraicGroup.GroupAlgebra.Galois.BaseChange

Scalar extension of an invariant group algebra #

The natural map from L ⊗[k] (L[M])^Gal(L/k) to L[M] is surjective when the automorphism group of L/k is finite. Here the action twists both the coefficients and the exponents, with the latter specified by an integral representation on the abelian group M. The scalar-extension map is Mathlib's AlgHom.liftEquiv applied to the invariant-subalgebra inclusion; it sends a ⊗ x to a • x.

For a finite Galois extension this map is an algebra equivalence. This identifies the scalar extension of the descended coordinate algebra with the split group algebra, as needed for groups of multiplicative type and non-split tori. Transporting the Hopf structure additionally requires the analogous identification on tensor squares.

References #

source
theorem TauCeti.GaloisDescent.liftEquiv_groupAlgebraInvariants_surjective {k : Type u_1} {L : Type u_2} {M : Type u_3} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [Finite Gal(L/k)] (rho : Representation ℤ Gal(L/k) M) :
Function.Surjective ⇑((AlgHom.liftEquiv k L (↥(groupAlgebraInvariants rho)) (MonoidAlgebra L (Multiplicative M))) (groupAlgebraInvariants rho).val)

Scalar extension of the invariant group-algebra inclusion is surjective. In particular, this holds over every finite Galois extension, without a characteristic restriction or a finite-generation hypothesis on the exponent group.

source
theorem TauCeti.GaloisDescent.liftEquiv_groupAlgebraInvariants_injective {k : Type u_1} {L : Type u_2} {M : Type u_3} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [FiniteDimensional k L] [IsGalois k L] (rho : Representation ℤ Gal(L/k) M) :
Function.Injective ⇑((AlgHom.liftEquiv k L (↥(groupAlgebraInvariants rho)) (MonoidAlgebra L (Multiplicative M))) (groupAlgebraInvariants rho).val)

Over a finite Galois extension, scalar extension of the invariant group-algebra inclusion is injective. The exponent group need not be finitely generated.

source
noncomputable def TauCeti.GaloisDescent.groupAlgebraInvariantsBaseChangeEquiv {k : Type u_1} {L : Type u_2} {M : Type u_3} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [FiniteDimensional k L] [IsGalois k L] (rho : Representation ℤ Gal(L/k) M) :
TensorProduct k L ↥(groupAlgebraInvariants rho) ≃ₐ[L] MonoidAlgebra L (Multiplicative M)

The invariant group algebra descends the split coordinate algebra along a finite Galois extension: extending its scalars recovers the original group algebra.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.GaloisDescent.groupAlgebraInvariantsBaseChangeEquiv_tmul {k : Type u_1} {L : Type u_2} {M : Type u_3} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [FiniteDimensional k L] [IsGalois k L] (rho : Representation ℤ Gal(L/k) M) (a : L) (x : ↥(groupAlgebraInvariants rho)) :
    (groupAlgebraInvariantsBaseChangeEquiv rho) (a ⊗ₜ[k] x) = a • ↑x

    The descent equivalence is scalar multiplication on pure tensors.

    source
    @[simp]
    theorem TauCeti.GaloisDescent.groupAlgebraInvariantsBaseChangeEquiv_symm_apply {k : Type u_1} {L : Type u_2} {M : Type u_3} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [FiniteDimensional k L] [IsGalois k L] (rho : Representation ℤ Gal(L/k) M) (x : ↥(groupAlgebraInvariants rho)) :
    (groupAlgebraInvariantsBaseChangeEquiv rho).symm ↑x = 1 ⊗ₜ[k] x

    The inverse descent equivalence sends an invariant element to its tensor with one.