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
๐Ÿ“ coverage
@[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
๐Ÿ“ coverage
@[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
๐Ÿ”ธ coverage
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
      ๐Ÿ“ coverage
      @[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
      ๐Ÿ“ coverage
      @[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
      ๐Ÿ“ coverage
      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
      ๐Ÿ“ coverage
      @[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
      ๐Ÿ“ coverage
      @[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
      ๐Ÿ”ธ coverage
      instance GroupLike.instInv {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] :
      Inv (GroupLike R A)
      Equations
        source
        ๐Ÿ“ coverage
        @[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
        ๐Ÿ”ธ coverage
        instance GroupLike.instGroup {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] :
        Group (GroupLike R A)
        Equations
          source
          ๐Ÿ”ธ coverage
          instance GroupLike.instCommGroup {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] :
          CommGroup (GroupLike R A)
          Equations