Documentation

TauCeti.Algebra.AlgebraicGroup.GroupAlgebra.Galois.Map

Morphisms of descended group algebras #

An equivariant homomorphism of abelian groups with Galois action induces a homomorphism of their invariant coordinate algebras. For a finite Galois extension this preserves the descended Hopf structure. The construction respects identities and composition, and its scalar extension agrees with the usual map of split group algebras under the splitting isomorphisms. These are the coordinate morphisms needed to recover groups of multiplicative type, and in particular tori, functorially from their character groups.

The split map is Mathlib's MonoidAlgebra.mapDomainBialgHom; only its descent is constructed here. No finite-generation or torsion-freeness assumption on the exponent groups is needed.

References #

source
noncomputable def Representation.IntertwiningMap.groupAlgebraInvariantsAlgHom {k : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [AddCommGroup N] [Field k] [Field L] [Algebra k L] {rho : Representation ℤ Gal(L/k) M} {tau : Representation ℤ Gal(L/k) N} (f : rho.IntertwiningMap tau) :
↥(TauCeti.GaloisDescent.groupAlgebraInvariants rho) →ₐ[k] ↥(TauCeti.GaloisDescent.groupAlgebraInvariants tau)

An equivariant map of exponent groups induces a map of invariant algebras.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem Representation.IntertwiningMap.coe_groupAlgebraInvariantsAlgHom {k : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [AddCommGroup N] [Field k] [Field L] [Algebra k L] {rho : Representation ℤ Gal(L/k) M} {tau : Representation ℤ Gal(L/k) N} (f : rho.IntertwiningMap tau) (x : ↥(TauCeti.GaloisDescent.groupAlgebraInvariants rho)) :
    ↑(f.groupAlgebraInvariantsAlgHom x) = (MonoidAlgebra.mapDomainBialgHom L (AddMonoidHom.toMultiplicative f.toAddMonoidHom)) ↑x

    The descended algebra map is the restriction of the split group-algebra map.

    source
    @[simp]
    theorem Representation.IntertwiningMap.groupAlgebraInvariantsAlgHom_id {k : Type u_1} {L : Type u_2} {M : Type u_3} [AddCommGroup M] [Field k] [Field L] [Algebra k L] {rho : Representation ℤ Gal(L/k) M} :
    (id rho).groupAlgebraInvariantsAlgHom = AlgHom.id k ↥(TauCeti.GaloisDescent.groupAlgebraInvariants rho)

    Descent of the identity exponent map is the identity algebra map.

    source
    @[simp]
    theorem Representation.IntertwiningMap.groupAlgebraInvariantsAlgHom_comp {k : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Field k] [Field L] [Algebra k L] {rho : Representation ℤ Gal(L/k) M} {tau : Representation ℤ Gal(L/k) N} {upsilon : Representation ℤ Gal(L/k) P} (f : rho.IntertwiningMap tau) (g : tau.IntertwiningMap upsilon) :
    (g.comp f).groupAlgebraInvariantsAlgHom = g.groupAlgebraInvariantsAlgHom.comp f.groupAlgebraInvariantsAlgHom

    Descent of exponent maps respects composition.

    source
    noncomputable def Representation.IntertwiningMap.groupAlgebraInvariantsBialgHom {k : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [AddCommGroup N] [Field k] [Field L] [Algebra k L] {rho : Representation ℤ Gal(L/k) M} {tau : Representation ℤ Gal(L/k) N} [FiniteDimensional k L] [IsGalois k L] (f : rho.IntertwiningMap tau) :
    ↥(TauCeti.GaloisDescent.groupAlgebraInvariants rho) →ₐc[k] ↥(TauCeti.GaloisDescent.groupAlgebraInvariants tau)

    An equivariant map of exponent groups descends to a bialgebra morphism. Antipode compatibility is given by BialgHom.map_antipode and the simp lemma BialgHomClass.map_antipode.

    Equations
    Instances For
      source
      @[simp]
      theorem Representation.IntertwiningMap.groupAlgebraInvariantsBialgHom_toAlgHom {k : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [AddCommGroup N] [Field k] [Field L] [Algebra k L] {rho : Representation ℤ Gal(L/k) M} {tau : Representation ℤ Gal(L/k) N} [FiniteDimensional k L] [IsGalois k L] (f : rho.IntertwiningMap tau) :
      ↑f.groupAlgebraInvariantsBialgHom = f.groupAlgebraInvariantsAlgHom

      The algebra homomorphism underlying the descended bialgebra morphism.

      source
      @[simp]
      theorem Representation.IntertwiningMap.coe_groupAlgebraInvariantsBialgHom {k : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [AddCommGroup N] [Field k] [Field L] [Algebra k L] {rho : Representation ℤ Gal(L/k) M} {tau : Representation ℤ Gal(L/k) N} [FiniteDimensional k L] [IsGalois k L] (f : rho.IntertwiningMap tau) (x : ↥(TauCeti.GaloisDescent.groupAlgebraInvariants rho)) :
      ↑(f.groupAlgebraInvariantsBialgHom x) = (MonoidAlgebra.mapDomainBialgHom L (AddMonoidHom.toMultiplicative f.toAddMonoidHom)) ↑x

      The descended bialgebra morphism agrees with the split map on invariant elements.

      source
      @[simp]
      theorem Representation.IntertwiningMap.groupAlgebraInvariantsBialgHom_id {k : Type u_1} {L : Type u_2} {M : Type u_3} [AddCommGroup M] [Field k] [Field L] [Algebra k L] {rho : Representation ℤ Gal(L/k) M} [FiniteDimensional k L] [IsGalois k L] :
      (id rho).groupAlgebraInvariantsBialgHom = BialgHom.id k ↥(TauCeti.GaloisDescent.groupAlgebraInvariants rho)

      Descent sends the identity exponent map to the identity bialgebra morphism.

      source
      @[simp]
      theorem Representation.IntertwiningMap.groupAlgebraInvariantsBialgHom_comp {k : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Field k] [Field L] [Algebra k L] {rho : Representation ℤ Gal(L/k) M} {tau : Representation ℤ Gal(L/k) N} {upsilon : Representation ℤ Gal(L/k) P} [FiniteDimensional k L] [IsGalois k L] (f : rho.IntertwiningMap tau) (g : tau.IntertwiningMap upsilon) :
      (g.comp f).groupAlgebraInvariantsBialgHom = g.groupAlgebraInvariantsBialgHom.comp f.groupAlgebraInvariantsBialgHom

      Descent of bialgebra morphisms respects composition of equivariant exponent maps.

      source
      @[simp]
      theorem Representation.IntertwiningMap.groupAlgebraInvariantsBaseChangeBialgEquiv_naturality {k : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [AddCommGroup M] [AddCommGroup N] [Field k] [Field L] [Algebra k L] {rho : Representation ℤ Gal(L/k) M} {tau : Representation ℤ Gal(L/k) N} [FiniteDimensional k L] [IsGalois k L] (f : rho.IntertwiningMap tau) :
      (↑(TauCeti.GaloisDescent.groupAlgebraInvariantsBaseChangeBialgEquiv tau)).comp (Bialgebra.TensorProduct.map (BialgHom.id L L) f.groupAlgebraInvariantsBialgHom) = (MonoidAlgebra.mapDomainBialgHom L (AddMonoidHom.toMultiplicative f.toAddMonoidHom)).comp ↑(TauCeti.GaloisDescent.groupAlgebraInvariantsBaseChangeBialgEquiv rho)

      The splitting isomorphisms identify scalar extension of a descended morphism with the ordinary split group-algebra morphism.