The tensor shear of a commutative Hopf algebra

The pullback of (g, h) ↦ (g, gh) is an automorphism of H ⊗[R] H. It fixes the left factor and sends the right factor to comultiplication. Its inverse uses the antipode in the left factor. This is the algebraic change of coordinates used in the canonical map for a quotient by a closed subgroup.

noncomputable def TauCeti.HopfAlgebra.tensorShearMulRight {R : Type u_1} {H : Type u_2} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] : TensorProduct R H H ≃ₐ[R] TensorProduct R H H

The coordinate automorphism of (g, h) ↦ (g, gh) on the tensor square of a commutative Hopf algebra.

Equations

• TauCeti.HopfAlgebra.tensorShearMulRight = AlgEquiv.ofAlgHom TauCeti.HopfAlgebra.tensorShearHom✝ TauCeti.HopfAlgebra.tensorShearInv✝ ⋯ ⋯

@[simp]

theorem TauCeti.HopfAlgebra.tensorShearMulRight_tmul {R : Type u_1} {H : Type u_2} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] (a b : H) : tensorShearMulRight (a ⊗ₜ[R] b) = a ⊗ₜ[R] 1 * CoalgebraStruct.comul b

The tensor shear fixes the first coordinate and multiplies the second by it.

@[simp]

theorem TauCeti.HopfAlgebra.tensorShearMulRight_symm_tmul {R : Type u_1} {H : Type u_2} [CommSemiring R] [CommSemiring H] [HopfAlgebra R H] (a b : H) : tensorShearMulRight.symm (a ⊗ₜ[R] b) = a ⊗ₜ[R] 1 * (TensorProduct.map (HopfAlgebraStruct.antipode R) LinearMap.id) (CoalgebraStruct.comul b)

The inverse tensor shear divides the second coordinate by the first.