Documentation

TauCeti.Algebra.AlgebraicGroup.GroupAlgebra.Galois.Invariants

Galois invariants of a group algebra #

Let L/k be a Galois extension and let M be an abelian group carrying an integral representation of Gal(L/k). The simultaneous action on coefficients and exponents of L[Multiplicative M] has a fixed k-subalgebra. This file constructs that subalgebra and proves that the Hopf operations preserve the corresponding descent data.

The counit of an invariant element is fixed by every automorphism of L/k, hence belongs to k. The antipode preserves the invariant subalgebra. Comultiplication lands in the fixed subalgebra of the tensor square for the diagonal semilinear action. The latter is deliberately not identified here with the tensor square of the invariant subalgebra: that identification is the faithfully flat scalar-extension theorem needed in the next descent step.

Main declarations #

References #

This is the invariant-algebra step in Layer 4, "Tori: split and non-split", of the ReductiveGroups roadmap. It follows the semilinear group-algebra action and precedes the theorem identifying scalar extension of the invariant algebra with the original split coordinate algebra.

source
noncomputable def TauCeti.GaloisDescent.groupAlgebraInvariants {k : Type u_k} {L : Type u_L} {M : Type u_M} [Field k] [Field L] [Algebra k L] [AddCommGroup M] (rho : Representation ℤ Gal(L/k) M) :
Subalgebra k (MonoidAlgebra L (Multiplicative M))

The fixed k-subalgebra of L[Multiplicative M] for the simultaneous action on coefficients and exponents.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.GaloisDescent.mem_groupAlgebraInvariants_iff {k : Type u_k} {L : Type u_L} {M : Type u_M} [Field k] [Field L] [Algebra k L] [AddCommGroup M] (rho : Representation ℤ Gal(L/k) M) (x : MonoidAlgebra L (Multiplicative M)) :
    x ∈ groupAlgebraInvariants rho ↔ ∀ (sigma : Gal(L/k)), ((groupAlgebraAction rho) sigma) x = x

    Membership in the invariant subalgebra means being fixed by every automorphism of L/k.

    source
    theorem TauCeti.GaloisDescent.mem_groupAlgebraInvariants_iff_coeff {k : Type u_k} {L : Type u_L} {M : Type u_M} [Field k] [Field L] [Algebra k L] [AddCommGroup M] (rho : Representation ℤ Gal(L/k) M) (x : MonoidAlgebra L (Multiplicative M)) :
    x ∈ groupAlgebraInvariants rho ↔ ∀ (sigma : Gal(L/k)) (m : Multiplicative M), sigma (x.coeff (Multiplicative.ofAdd ((rho sigma⁻¹) (Multiplicative.toAdd m)))) = x.coeff m

    Coefficientwise characterization of the invariant group algebra. The coefficient at m after applying sigma is read at the inverse translate of m.

    source
    theorem TauCeti.GaloisDescent.single_mem_groupAlgebraInvariants {k : Type u_k} {L : Type u_L} {M : Type u_M} [Field k] [Field L] [Algebra k L] [AddCommGroup M] (rho : Representation ℤ Gal(L/k) M) (m : Multiplicative M) (a : L) (hm : ∀ (sigma : Gal(L/k)), (rho sigma) (Multiplicative.toAdd m) = Multiplicative.toAdd m) (ha : ∀ (sigma : Gal(L/k)), sigma a = a) :
    MonoidAlgebra.single m a ∈ groupAlgebraInvariants rho

    A monomial is invariant if its coefficient and exponent are fixed by every Galois automorphism.

    source
    noncomputable def TauCeti.GaloisDescent.groupAlgebraInvariantsCounit {k : Type u_k} {L : Type u_L} {M : Type u_M} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [IsGalois k L] (rho : Representation ℤ Gal(L/k) M) :
    ↥(groupAlgebraInvariants rho) →ₐ[k] k

    The counit of the descended invariant algebra. Invariance forces the original L-valued counit to lie in the image of k, and Galois fixed-field descent identifies that image with k.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.GaloisDescent.algebraMap_groupAlgebraInvariantsCounit {k : Type u_k} {L : Type u_L} {M : Type u_M} [Field k] [Field L] [Algebra k L] [AddCommGroup M] [IsGalois k L] (rho : Representation ℤ Gal(L/k) M) (x : ↥(groupAlgebraInvariants rho)) :
      (algebraMap k L) ((groupAlgebraInvariantsCounit rho) x) = CoalgebraStruct.counit ↑x

      Extending the descended counit value back to L recovers the ordinary group-algebra counit.

      source
      noncomputable def TauCeti.GaloisDescent.groupAlgebraInvariantsAntipode {k : Type u_k} {L : Type u_L} {M : Type u_M} [Field k] [Field L] [Algebra k L] [AddCommGroup M] (rho : Representation ℤ Gal(L/k) M) :
      ↥(groupAlgebraInvariants rho) ≃ₐ[k] ↥(groupAlgebraInvariants rho)

      The group-algebra antipode restricted to the Galois-invariant subalgebra.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TauCeti.GaloisDescent.groupAlgebraInvariantsAntipode_apply {k : Type u_k} {L : Type u_L} {M : Type u_M} [Field k] [Field L] [Algebra k L] [AddCommGroup M] (rho : Representation ℤ Gal(L/k) M) (x : ↥(groupAlgebraInvariants rho)) :
        ↑((groupAlgebraInvariantsAntipode rho) x) = (HopfAlgebraStruct.antipode L) ↑x

        The restricted antipode acts by the ordinary group-algebra antipode.

        source
        @[simp]
        theorem TauCeti.GaloisDescent.groupAlgebraInvariantsAntipode_apply_apply {k : Type u_k} {L : Type u_L} {M : Type u_M} [Field k] [Field L] [Algebra k L] [AddCommGroup M] (rho : Representation ℤ Gal(L/k) M) (x : ↥(groupAlgebraInvariants rho)) :
        (groupAlgebraInvariantsAntipode rho) ((groupAlgebraInvariantsAntipode rho) x) = x

        The antipode on the invariant algebra is involutive.

        source
        @[simp]
        theorem TauCeti.GaloisDescent.groupAlgebraInvariantsAntipode_symm {k : Type u_k} {L : Type u_L} {M : Type u_M} [Field k] [Field L] [Algebra k L] [AddCommGroup M] (rho : Representation ℤ Gal(L/k) M) :
        (groupAlgebraInvariantsAntipode rho).symm = groupAlgebraInvariantsAntipode rho

        The restricted antipode equivalence is its own inverse.

        source
        noncomputable def TauCeti.GaloisDescent.groupAlgebraTensorInvariants {k : Type u_k} {L : Type u_L} {M : Type u_M} [Field k] [Field L] [Algebra k L] [AddCommGroup M] (rho : Representation ℤ Gal(L/k) M) :
        Subalgebra k (TensorProduct L (MonoidAlgebra L (Multiplicative M)) (MonoidAlgebra L (Multiplicative M)))

        The fixed k-subalgebra of the tensor square for the diagonal semilinear Galois action.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.GaloisDescent.mem_groupAlgebraTensorInvariants_iff {k : Type u_k} {L : Type u_L} {M : Type u_M} [Field k] [Field L] [Algebra k L] [AddCommGroup M] (rho : Representation ℤ Gal(L/k) M) (t : TensorProduct L (MonoidAlgebra L (Multiplicative M)) (MonoidAlgebra L (Multiplicative M))) :
          t ∈ groupAlgebraTensorInvariants rho ↔ ∀ (sigma : Gal(L/k)), (groupAlgebraTensorActionSemilinearEquiv rho sigma) t = t

          Membership among invariant tensors means being fixed by the diagonal action.

          source
          noncomputable def TauCeti.GaloisDescent.groupAlgebraInvariantsComul {k : Type u_k} {L : Type u_L} {M : Type u_M} [Field k] [Field L] [Algebra k L] [AddCommGroup M] (rho : Representation ℤ Gal(L/k) M) :
          ↥(groupAlgebraInvariants rho) →ₐ[k] ↥(groupAlgebraTensorInvariants rho)

          Comultiplication from invariant elements to tensors invariant under the diagonal action.

          Identifying the codomain with the tensor square of groupAlgebraInvariants rho is the subsequent faithfully flat descent step.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem TauCeti.GaloisDescent.groupAlgebraInvariantsComul_apply {k : Type u_k} {L : Type u_L} {M : Type u_M} [Field k] [Field L] [Algebra k L] [AddCommGroup M] (rho : Representation ℤ Gal(L/k) M) (x : ↥(groupAlgebraInvariants rho)) :
            ↑((groupAlgebraInvariantsComul rho) x) = CoalgebraStruct.comul ↑x

            The restricted comultiplication acts by the ordinary group-algebra comultiplication.