Documentation

Mathlib.RingTheory.HopfAlgebra.GroupLike

Group-like elements in a Hopf algebra #

This file proves that group-like elements in a Hopf algebra form a group.

source
@[simp]
theorem IsGroupLikeElem.antipode_mul_cancel {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] {a : A} (ha : IsGroupLikeElem R a) :
(HopfAlgebraStruct.antipode R) a * a = 1
source
@[simp]
theorem IsGroupLikeElem.mul_antipode_cancel {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] {a : A} (ha : IsGroupLikeElem R a) :
a * (HopfAlgebraStruct.antipode R) a = 1
source
def GroupLike.toUnits (R : Type u_1) {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] :
GroupLike R A →* Aˣ

Turn a group-like element a into a unit with inverse its antipode.

Equations
    Instances For
      source
      @[simp]
      theorem GroupLike.val_inv_toUnits_apply (R : Type u_1) {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] (a : GroupLike R A) :
      ↑((toUnits R) a)⁻¹ = (HopfAlgebraStruct.antipode R) ↑a
      source
      @[simp]
      theorem GroupLike.val_toUnits_apply (R : Type u_1) {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] (a : GroupLike R A) :
      ↑((toUnits R) a) = ↑a
      source
      theorem IsGroupLikeElem.isUnit {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] {a : A} (ha : IsGroupLikeElem R a) :
      IsUnit a
      source
      @[simp]
      theorem IsGroupLikeElem.antipode {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] {a : A} (ha : IsGroupLikeElem R a) :
      IsGroupLikeElem R ((HopfAlgebraStruct.antipode R) a)
      source
      @[simp]
      theorem IsGroupLikeElem.antipode_antipode {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] {a : A} (ha : IsGroupLikeElem R a) :
      (HopfAlgebraStruct.antipode R) ((HopfAlgebraStruct.antipode R) a) = a
      source
      instance GroupLike.instInv {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] :
      Inv (GroupLike R A)
      Equations
        source
        @[simp]
        theorem GroupLike.val_inv {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] (a : GroupLike R A) :
        ↑a⁻¹ = (HopfAlgebraStruct.antipode R) ↑a
        source
        instance GroupLike.instGroup {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] :
        Group (GroupLike R A)
        Equations
          source
          instance GroupLike.instCommGroup {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] :
          CommGroup (GroupLike R A)
          Equations