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.

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