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.

@[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' := ⋯ }

Instances For

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

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

theorem IsGroupLikeElem.isUnit {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [HopfAlgebra R A] {a : A} (ha : IsGroupLikeElem R 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_reducible]

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_reducible]

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_reducible]

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.