Group-like elements in a Hopf algebra

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

@[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

@[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

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

• GroupLike.toUnits R = { toFun := fun (a : GroupLike R A) => { val := ↑a, inv := (HopfAlgebraStruct.antipode R) ↑a, val_inv := ⋯, inv_val := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }

@[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

@[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

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

@[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)

@[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

instance GroupLike.instInv {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] : Inv (GroupLike R A)

Equations

• GroupLike.instInv = { inv := fun (a : GroupLike R A) => { val := (HopfAlgebraStruct.antipode R) ↑a, isGroupLikeElem_val := ⋯ } }

@[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

instance GroupLike.instGroup {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] : Group (GroupLike R A)

Equations

• One or more equations did not get rendered due to their size.

instance GroupLike.instCommGroup {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [HopfAlgebra R A] : CommGroup (GroupLike R A)

Equations

• One or more equations did not get rendered due to their size.