Theorems · Definition · ring theory

Bialgebra.ofAlgHom

{R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [inst_2 : Algebra R A] →
          (comul : A →ₐ[R] TensorProduct R A A) →
            (counit : A →ₐ[R] R) →
              (↑(Algebra.TensorProduct.assoc R R R A A A)).comp
                    ((Algebra.TensorProduct.map comul (AlgHom.id R A)).comp comul) =
                  (Algebra.TensorProduct.map (AlgHom.id R A) comul).comp comul →
                (Algebra.TensorProduct.map counit (AlgHom.id R A)).comp comul = ↑(Algebra.TensorProduct.lid R A).symm →
                  (Algebra.TensorProduct.map (AlgHom.id R A) counit).comp comul =
                      ↑(Algebra.TensorProduct.rid R R A).symm →
                    Bialgebra R A

If R is a commutative semiring and A is an R-algebra, then Bialgebra.ofAlgHom consumes the counit and comultiplication as algebra homomorphisms that satisfy the coalgebra axioms to define a bialgebra structure on A.

Defined in

Mathlib.RingTheory.Bialgebra.Basic

Cited by

0 results in Mathlib

Foundations

Depth 82 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringSemiringAlgebra