Mathlib Map

Theorems · Definition · category theory

ModuleCat.carrier

{R : Type u} → [inst : Ring R] → ModuleCat R → Type v

the underlying type of an object in ModuleCat R

Defined in
Mathlib.Algebra.Category.ModuleCat.Basic
Cited by
997 results in Mathlib
Foundations
Depth 2 from the axioms, rests on 3 definitions · uses no axioms
Assumes
Ring
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

ModuleCat.Hom.hom · cited by 341Hom.homCategoryTheory.ShortComplex.moduleCatLeftHomologyData · cited by 106ShortComplex.moduleCatLef…ModuleCat.hom_ext · cited by 84ModuleCat.hom_extModuleCat.isFG · cited by 53ModuleCat.isFGQuadraticModuleCat.form · cited by 30QuadraticModuleCat.formFGModuleCat.carrier · cited by 28FGModuleCat.carrierRep.coinvariantsMk · cited by 26Rep.coinvariantsMkAlgebraicGeometry.tilde · cited by 24AlgebraicGeometry.tildeTopModuleCat.Hom.hom · cited by 22Hom.homModuleCat.mono_iff_injective · cited by 21ModuleCat.mono_iff_inject…CategoryTheory.ShortComplex.moduleCatToCycles · cited by 20ShortComplex.moduleCatToC…QuadraticModuleCat.Hom.toIsometry · cited by 18Hom.toIsometryModuleCat.freeMk · cited by 18ModuleCat.freeMkCategoryTheory.preadditiveYoneda · cited by 17CategoryTheory.preadditiv…ModuleCat.localizedModule · cited by 16ModuleCat.localizedModuleRing · cited by 7463RingModuleCat · cited by 1429ModuleCatModuleCat.carrierCITED BYCITES

Cites2

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

  • Ringstatement and proof · cited by 7,463
  • ModuleCatstatement and proof · cited by 1,429

Cited by1,264

Results whose statement or proof uses this declaration.

Showing the 200 most cited of 1,264.