Documentation

TauCeti.Algebra.AlgebraicGroup.Tangent.CounitPoints

Points valued in the counit algebra #

Tangent vectors at the identity of Spec H are derivations valued in Bialgebra.CounitAlgebra R H B, and the points that conjugate them are therefore points valued in that same algebra. The counit algebra is B carrying one extra H-algebra structure, which an R-algebra homomorphism out of H does not see, so those points are just the B-points.

This file records that identification as an isomorphism of convolution groups, so that a computation of the adjoint action stated for counit-algebra-valued points can be read off the ordinary functor of points.

Main declarations #

This is coefficient bookkeeping for the adjoint action of Layer 2, "Lie algebra and the adjoint representation", of the ReductiveGroups roadmap.

source
noncomputable def TauCeti.Bialgebra.CounitAlgebra.pointsMulEquiv (R : Type u) (H : Type v) (B : Type w) [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] [CommSemiring B] [Algebra R B] :
WithConv (H →ₐ[R] CounitAlgebra R H B) ≃* WithConv (H →ₐ[R] B)

Points valued in the counit algebra of H are the points valued in the coefficient algebra B itself: the counit algebra is B with one extra H-algebra structure, which an R-algebra homomorphism out of H does not see. The identification is an isomorphism of convolution groups.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TauCeti.Bialgebra.CounitAlgebra.pointsMulEquiv_eq_mapValue (R : Type u) (H : Type v) (B : Type w) [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] [CommSemiring B] [Algebra R B] (g : WithConv (H →ₐ[R] CounitAlgebra R H B)) :
    (pointsMulEquiv R H B) g = (AlgHom.mapValue ↑(algEquivSelf R H B)) g

    The transport of points is postcomposition with the identification of the counit algebra with the coefficient algebra.

    source
    @[simp]
    theorem TauCeti.Bialgebra.CounitAlgebra.pointsMulEquiv_apply (R : Type u) (H : Type v) (B : Type w) [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] [CommSemiring B] [Algebra R B] (g : WithConv (H →ₐ[R] CounitAlgebra R H B)) (h : H) :
    ((pointsMulEquiv R H B) g).ofConv h = (algEquivSelf R H B) (g.ofConv h)

    Transporting a counit-algebra-valued point does not change its values.

    source
    @[simp]
    theorem TauCeti.Bialgebra.CounitAlgebra.pointsMulEquiv_symm_apply (R : Type u) (H : Type v) (B : Type w) [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] [CommSemiring B] [Algebra R B] (f : WithConv (H →ₐ[R] B)) (h : H) :
    ((pointsMulEquiv R H B).symm f).ofConv h = (algEquivSelf R H B).symm (f.ofConv h)

    Transporting a B-valued point into the counit algebra does not change its values.

    source
    theorem TauCeti.Bialgebra.CounitAlgebra.pointsMulEquiv_mapValue (R : Type u) (H : Type v) (B : Type w) [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] [CommSemiring B] [Algebra R B] {C : Type u_1} [CommSemiring C] [Algebra R C] (phi : B →ₐ[R] C) (g : WithConv (H →ₐ[R] CounitAlgebra R H B)) :
    (pointsMulEquiv R H C) ((AlgHom.mapValue (mapAlgHom phi)) g) = (AlgHom.mapValue phi) ((pointsMulEquiv R H B) g)

    The counit-points equivalence is natural in the coefficient algebra.

    source
    theorem TauCeti.Bialgebra.CounitAlgebra.mapValue_pointsMulEquiv_symm_apply (R : Type u) (H : Type v) (B : Type w) [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] [CommSemiring B] [Algebra R B] {C : Type u_1} [CommSemiring C] [Algebra R C] (phi : B →ₐ[R] C) (f : WithConv (H →ₐ[R] B)) :
    (AlgHom.mapValue (mapAlgHom phi)) ((pointsMulEquiv R H B).symm f) = (pointsMulEquiv R H C).symm ((AlgHom.mapValue phi) f)

    Naturality of the inverse counit-points equivalence in the coefficient algebra.