Mathlib Map

Theorems · Definition · category theory

CoalgCat.ofComonObj

{R : Type u} → [inst : CommRing R] → (X : ModuleCat R) → [CategoryTheory.ComonObj X] → CoalgCat R

A comonoid object in the category of R-modules has a natural R-coalgebra structure.

Defined in
Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
Cited by
0 results in Mathlib
Foundations
Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CommRingCategoryTheory.ComonObj
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

CoalgCat.ofComon · cited by 3CoalgCat.ofComonCommRing · cited by 17173CommRingModuleCat · cited by 1429ModuleCatModuleCat.carrier · cited by 997ModuleCat.carrierModuleCat.of · cited by 594ModuleCat.ofCoalgebraStruct · cited by 230CoalgebraStructCoalgCat · cited by 63CoalgCatCategoryTheory.ComonObj · cited by 48CategoryTheory.ComonObjCoalgCat.ofComonObjCITED BYCITES

Cites7

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

Cited by1

Results whose statement or proof uses this declaration.