Mathlib Map

Theorems · Definition · category theory

CommAlgCat.carrier

{R : Type u} → [inst : CommRing R] → CommAlgCat R → Type v

The underlying type.

Defined in
Mathlib.Algebra.Category.CommAlgCat.Basic
Cited by
77 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Assumes
CommRing
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

CommAlgCat.Hom.hom · cited by 39Hom.homcommAlgCatEquivUnder · cited by 9commAlgCatEquivUndercommBialgCatEquivComonCommAlgCat · cited by 9commBialgCatEquivComonCom…commHopfAlgCatEquivCogrpCommAlgCat · cited by 6commHopfAlgCatEquivCogrpC…CommAlgCat.algEquivOfIso · cited by 3CommAlgCat.algEquivOfIsoCommAlgCat.FiniteEtale.finiteSpec · cited by 3FiniteEtale.finiteSpecCommAlgCat.FiniteEtale.equivOfIsSepClosed · cited by 3FiniteEtale.equivOfIsSepC…Module.Grassmannian.functor · cited by 2Grassmannian.functorCommAlgCat.FiniteEtale.baseChange · cited by 2FiniteEtale.baseChangeCommAlgCat.FiniteEtale.fiber · cited by 2FiniteEtale.fiberCommAlgCat.Hom.ext · cited by 2Hom.extCommAlgCat.Hom.hom' · cited by 2Hom.hom'FGAlgCat.equivUnder · cited by 1FGAlgCat.equivUnderAlgebra.FiniteType.exists_fgAlgCatSkeleton · cited by 1FiniteType.exists_fgAlgCa…CommAlgCat.hom_ext · cited by 1CommAlgCat.hom_extCommRing · cited by 17173CommRingCommAlgCat · cited by 96CommAlgCatCommAlgCat.carrierCITED BYCITES

Cites2

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
  • CommAlgCatstatement and proof · cited by 96

Cited by105

Results whose statement or proof uses this declaration.