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.

Equations

• groupLikeSubmonoid R A = { carrier := {a : A | IsGroupLikeElem R a}, mul_mem' := ⋯, one_mem' := ⋯ }

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)

Equations

• GroupLike.instOne = { one := { val := 1, isGroupLikeElem_val := ⋯ } }

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

Equations

• GroupLike.instMul = { mul := fun (a b : GroupLike R A) => { val := ↑a * ↑b, isGroupLikeElem_val := ⋯ } }

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

Equations

• GroupLike.instPowNat = { pow := fun (a : GroupLike R A) (n : ℕ) => { val := ↑a ^ n, isGroupLikeElem_val := ⋯ } }

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

Equations

• GroupLike.instMonoid = Function.Injective.monoid GroupLike.val ⋯ ⋯ ⋯ ⋯

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.

Equations

• GroupLike.valMonoidHom R A = { toFun := GroupLike.val, map_one' := ⋯, map_mul' := ⋯ }

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

Equations

• GroupLike.instCommMonoid = Function.Injective.commMonoid GroupLike.val ⋯ ⋯ ⋯ ⋯