Group-like elements in a bialgebra

This file proves that group-like elements in a bialgebra form a monoid.

theorem IsGroupLikeElem.one {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] : IsGroupLikeElem R 1

In a bialgebra, 1 is a group-like element.

theorem IsGroupLikeElem.mul {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] {a b : A} (ha : IsGroupLikeElem R a) (hb : IsGroupLikeElem R b) : IsGroupLikeElem R (a * b)

Group-like elements in a bialgebra are stable under multiplication.

def groupLikeSubmonoid (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Bialgebra R A] : Submonoid A

The group-like elements form a submonoid.

theorem IsGroupLikeElem.pow {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] {a : A} {n : ℕ} (ha : IsGroupLikeElem R a) : IsGroupLikeElem R (a ^ n)

Group-like elements in a bialgebra are stable under power.

theorem IsGroupLikeElem.of_mul_eq_one {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] {a b : A} (hab : a * b = 1) (hba : b * a = 1) (ha : IsGroupLikeElem R a) : IsGroupLikeElem R b

Group-like elements in a bialgebra are stable under inverses, when they exist.

theorem isGroupLikeElem_iff_of_mul_eq_one {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] {a b : A} (hab : a * b = 1) (hba : b * a = 1) : IsGroupLikeElem R a ↔ IsGroupLikeElem R b

Group-like elements in a bialgebra are stable under inverses, when they exist.

@[simp]

theorem isGroupLikeElem_unitsInv {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] {u : Aˣ} : IsGroupLikeElem R ↑u⁻¹ ↔ IsGroupLikeElem R ↑u

theorem IsGroupLikeElem.of_unitsInv {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] {u : Aˣ} : IsGroupLikeElem R ↑u⁻¹ → IsGroupLikeElem R ↑u

Alias of the forward direction of isGroupLikeElem_unitsInv.

theorem IsGroupLikeElem.unitsInv {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] {u : Aˣ} : IsGroupLikeElem R ↑u → IsGroupLikeElem R ↑u⁻¹

Alias of the reverse direction of isGroupLikeElem_unitsInv.

instance GroupLike.instOne {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] : One (GroupLike R A)

instance GroupLike.instMul {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] : Mul (GroupLike R A)

instance GroupLike.instPowNat {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] : Pow (GroupLike R A) ℕ

@[simp]

theorem GroupLike.val_one {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] : ↑1 = 1

@[simp]

theorem GroupLike.val_mul {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] (a b : GroupLike R A) : ↑(a * b) = ↑a * ↑b

@[simp]

theorem GroupLike.val_pow {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] (a : GroupLike R A) (n : ℕ) : ↑(a ^ n) = ↑a ^ n

instance GroupLike.instMonoid {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] : Monoid (GroupLike R A)

def GroupLike.valMonoidHom (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Bialgebra R A] : GroupLike R A →* A

GroupLike.val as a monoid hom.

@[simp]

theorem GroupLike.valMonoidHom_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Bialgebra R A] (self : GroupLike R A) : (valMonoidHom R A) self = ↑self

instance GroupLike.instCommMonoid {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Bialgebra R A] : CommMonoid (GroupLike R A)