Documentation

Mathlib.RingTheory.Bialgebra.GroupLike

Group-like elements in a bialgebra #

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

source
๐Ÿ“ coverage
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.

source
๐Ÿ“ coverage
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.

source
๐Ÿ”ธ coverage
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.

Instances For
    source
    ๐Ÿ“ coverage
    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.

    source
    ๐Ÿ“ coverage
    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.

    source
    ๐Ÿ“ coverage
    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.

    source
    ๐Ÿ“ coverage
    @[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
    source
    ๐Ÿ“ coverage
    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.

    source
    ๐Ÿ“ coverage
    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.

    source
    ๐Ÿ”ธ coverage
    @[implicit_reducible]
    instance GroupLike.instOne {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] :
    One (GroupLike R A)
    source
    ๐Ÿ”ธ coverage
    @[implicit_reducible]
    instance GroupLike.instMul {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] :
    Mul (GroupLike R A)
    source
    ๐Ÿ”ธ coverage
    @[implicit_reducible]
    instance GroupLike.instPowNat {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] :
    Pow (GroupLike R A) โ„•
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem GroupLike.val_one {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] :
    โ†‘1 = 1
    source
    ๐Ÿ“ coverage
    @[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
    source
    ๐Ÿ“ coverage
    @[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
    source
    ๐Ÿ”ธ coverage
    @[implicit_reducible]
    instance GroupLike.instMonoid {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Bialgebra R A] :
    Monoid (GroupLike R A)
    source
    ๐Ÿ”ธ coverage
    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.

    Instances For
      source
      ๐Ÿ“ coverage
      @[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
      source
      ๐Ÿ”ธ coverage
      @[implicit_reducible]
      instance GroupLike.instCommMonoid {R : Type u_1} {A : Type u_2} [CommSemiring R] [CommSemiring A] [Bialgebra R A] :
      CommMonoid (GroupLike R A)