Theorems · Definition · category theory
commBialgCatEquivComonCommAlgCat
(R : Type u) → [inst : CommRing R] → CommBialgCat R ≌ (CategoryTheory.Mon (CommAlgCat R)ᵒᵖ)ᵒᵖ
Commutative bialgebras over a commutative ring R are the same thing as comonoid
R-algebras.
- Defined in
- Mathlib.Algebra.Category.CommBialgCat
- Cited by
- 9 results in Mathlib
- Foundations
- Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites26
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homproof · cited by 32,603
- CommRingstatement and proof · cited by 17,173
- Oppositestatement and proof · cited by 8,081
- CategoryTheory.Functor.compproof · cited by 6,529
- CategoryTheory.CategoryStruct.idproof · cited by 6,235
- CategoryTheory.Functor.idproof · cited by 3,333
- Opposite.unopproof · cited by 2,231
- Quiver.Hom.opproof · cited by 1,948
- Quiver.Hom.unopproof · cited by 903
- CategoryTheory.Equivalencestatement · cited by 601
- CategoryTheory.Monstatement and proof · cited by 465
- CategoryTheory.Mon.Xproof · cited by 329
Cited by11
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.bialgSpecproof · cited by 1
- AlgebraicGeometry.one_defstatement · cited by 0
- AlgebraicGeometry.bialgSpec.fullyFaithfulproof · cited by 0
- commBialgCatEquivComonCommAlgCat_counitIso_hom_appstatement and proof · cited by 0
- commBialgCatEquivComonCommAlgCat_counitIso_inv_appstatement and proof · cited by 0
- commBialgCatEquivComonCommAlgCat_functor_map_unop_homstatement · cited by 0
- commBialgCatEquivComonCommAlgCat_functor_obj_unop_Xstatement and proof · cited by 0
- commBialgCatEquivComonCommAlgCat_inverse_map_unop_homstatement · cited by 0
- commBialgCatEquivComonCommAlgCat_inverse_objstatement and proof · cited by 0
- commBialgCatEquivComonCommAlgCat_unitIso_hom_appstatement and proof · cited by 0
- commBialgCatEquivComonCommAlgCat_unitIso_inv_appstatement and proof · cited by 0