Mathlib Map

Theorems · Definition · category theory

BialgCat.of

(R : Type u) → [inst : CommRing R] → (X : Type v) → [inst_1 : Ring X] → [Bialgebra R X] → BialgCat R

The object in the category of R-bialgebras associated to an R-bialgebra.

Defined in
Mathlib.Algebra.Category.BialgCat.Basic
Cited by
17 results in Mathlib
Foundations
Depth 7 from the axioms · uses no axioms
Assumes
CommRingRingBialgebra
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

BialgEquiv.toBialgIso · cited by 8BialgEquiv.toBialgIsoBialgCat.ofHom · cited by 6BialgCat.ofHomBialgCat.associator_def · cited by 0BialgCat.associator_defBialgCat.whiskerLeft_def · cited by 0BialgCat.whiskerLeft_defBialgCat.whiskerRight_def · cited by 0BialgCat.whiskerRight_defBialgCat.leftUnitor_def · cited by 0BialgCat.leftUnitor_defHopfAlgCat.forget₂_bialgebra_obj · cited by 0HopfAlgCat.forget₂_bialge…BialgCat.of_carrier · cited by 0BialgCat.of_carrierBialgCat.of_comul · cited by 0BialgCat.of_comulBialgEquiv.toBialgIso_hom · cited by 0BialgEquiv.toBialgIso_homBialgEquiv.toBialgIso_inv · cited by 0BialgEquiv.toBialgIso_invBialgEquiv.toBialgIso_refl · cited by 0BialgEquiv.toBialgIso_reflBialgEquiv.toBialgIso_symm · cited by 0BialgEquiv.toBialgIso_symmBialgEquiv.toBialgIso_trans · cited by 0BialgEquiv.toBialgIso_tra…BialgCat.of_counit · cited by 0BialgCat.of_counitCommRing · cited by 17173CommRingRing · cited by 7463RingBialgebra · cited by 160BialgebraBialgCat · cited by 40BialgCatBialgCat.ofCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • CommRingstatement and proof · cited by 17,173
  • Ringstatement and proof · cited by 7,463
  • Bialgebrastatement and proof · cited by 160
  • BialgCatstatement · cited by 40

Cited by19

Results whose statement or proof uses this declaration.