Documentation

TauCeti.Algebra.AlgebraicGroup.CommHopfAlgCat.InnerConjugation

Inner conjugation in Hopf coordinates #

An R-valued point g of an affine group acts on all algebra-valued points by inner conjugation. This action is natural in the value algebra and is a group automorphism. Full faithfulness of the functor of points therefore recovers a coordinate Hopf-algebra automorphism.

The coordinate morphism is characterized both on arbitrary algebra-valued points and as an algebra map. The latter is evaluation of the universal conjugation morphism at g in its first factor:

H --conj#--> H ⊗ H --(g ⊗ id)--> H.

Main declarations #

References #

source
noncomputable def TauCeti.CommHopfAlgCat.innerConjugationIso {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (g : ↑(HopfAlgebra.points ↧R)) :
H ≅ H

The coordinate Hopf-algebra automorphism representing conjugation by an R-valued point.

Contravariance means that its underlying coordinate map is the pullback of the pointwise inner automorphism.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.innerConjugationIso_one {R : Type u} [CommRing R] (H : CommHopfAlgCat R) :
    innerConjugationIso H 1 = CategoryTheory.Iso.refl H

    Conjugation by the identity point is the identity coordinate Hopf-algebra automorphism.

    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.innerConjugationIso_mul {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (g h : ↑(HopfAlgebra.points ↧R)) :
    innerConjugationIso H (g * h) = innerConjugationIso H g ≪≫ innerConjugationIso H h

    Coordinate pullback reverses the pointwise composition order: the coordinate automorphism for conjugation by g * h is the composite for g followed by the one for h.

    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.innerConjugationIso_inv_point {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (g : ↑(HopfAlgebra.points ↧R)) :
    innerConjugationIso H g⁻¹ = (innerConjugationIso H g).symm

    The coordinate automorphism for conjugation by an inverse point is the inverse coordinate automorphism.

    source
    theorem TauCeti.CommHopfAlgCat.innerConjugationIso_hom_toAlgHom {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (g : ↑(HopfAlgebra.points ↧R)) :
    ↑(CommHopfAlgCat.Hom.hom (innerConjugationIso H g).hom) = (Algebra.TensorProduct.productMap ((Algebra.ofId R ↑H).comp g.ofConv) (AlgHom.id R ↑H)).comp HopfAlgebra.conjugationAlgHom

    The coordinate algebra map of inner conjugation is obtained from the universal conjugation map by evaluating its conjugating variable at the given R-valued point.

    source
    theorem TauCeti.CommHopfAlgCat.innerConjugationIso_inv_toAlgHom {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (g : ↑(HopfAlgebra.points ↧R)) :
    ↑(CommHopfAlgCat.Hom.hom (innerConjugationIso H g).inv) = (Algebra.TensorProduct.productMap ((Algebra.ofId R ↑H).comp g⁻¹.ofConv) (AlgHom.id R ↑H)).comp HopfAlgebra.conjugationAlgHom

    The inverse coordinate algebra map is obtained from the universal conjugation map by evaluating its conjugating variable at the inverse of the given R-valued point.

    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.mapPointsFunctor_innerConjugationIso_hom {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (g : ↑(HopfAlgebra.points ↧R)) :
    mapPointsFunctor (innerConjugationIso H g).hom = (HopfAlgebra.innerConjugationPointNatIso (↑H) g).hom

    The coordinate inner automorphism induces natural inner conjugation on points over commutative value algebras in any universe.

    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.mapPointsFunctor_innerConjugationIso_inv {R : Type u} [CommRing R] (H : CommHopfAlgCat R) (g : ↑(HopfAlgebra.points ↧R)) :
    mapPointsFunctor (innerConjugationIso H g).inv = (HopfAlgebra.innerConjugationPointNatIso (↑H) g).inv

    The inverse coordinate inner automorphism induces the inverse natural inner conjugation on points over commutative value algebras in any universe.