Theorems · Definition · category theory

HopfAlgCat.of

(R : Type u) → [inst : CommRing R] → (X : Type v) → [inst_1 : Ring X] → [HopfAlgebra R X] → HopfAlgCat R

The object in the category of R-Hopf algebras associated to an R-Hopf algebra.

Defined in

Mathlib.Algebra.Category.HopfAlgCat.Basic

Cited by

13 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

CommRingRingHopfAlgebra