Mathlib Map

Theorems · Definition · category theory

CommAlgCat.Hom.hom

{R : Type u} → [inst : CommRing R] → {A B : CommAlgCat R} → A.Hom B → ↑A →ₐ[R] ↑B

Turn a morphism in CommAlgCat back into an AlgHom.

Defined in
Mathlib.Algebra.Category.CommAlgCat.Basic
Cited by
39 results in Mathlib
Foundations
Depth 28 from the axioms · uses propext, Quot.sound
Assumes
CommRing
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

commAlgCatEquivUnder · cited by 9commAlgCatEquivUndercommBialgCatEquivComonCommAlgCat · cited by 9commBialgCatEquivComonCom…commHopfAlgCatEquivCogrpCommAlgCat · cited by 6commHopfAlgCatEquivCogrpC…CommAlgCat.FiniteEtale.finiteSpec · cited by 3FiniteEtale.finiteSpecCommAlgCat.algEquivOfIso · cited by 3CommAlgCat.algEquivOfIsoModule.Grassmannian.functor · cited by 2Grassmannian.functorCommAlgCat.FiniteEtale.baseChange · cited by 2FiniteEtale.baseChangeCommAlgCat.FiniteEtale.fiber · cited by 2FiniteEtale.fiberCommAlgCat.hom_ext · cited by 1CommAlgCat.hom_extCommAlgCat.FiniteEtale.fiber_map · cited by 0FiniteEtale.fiber_mapCommAlgCat.ofHom_hom · cited by 0CommAlgCat.ofHom_homModule.Grassmannian.functor_map · cited by 0Grassmannian.functor_mapCommAlgCat.one_op_of_unop_hom · cited by 0CommAlgCat.one_op_of_unop…CommAlgCat.FiniteEtale.finiteSpec_map · cited by 0FiniteEtale.finiteSpec_mapCommAlgCat.snd_unop_hom · cited by 0CommAlgCat.snd_unop_homCommRing · cited by 17173CommRingCategoryTheory.ConcreteCategory.hom · cited by 4022ConcreteCategory.homAlgHom · cited by 3236AlgHomCommAlgCat · cited by 96CommAlgCatCommAlgCat.carrier · cited by 77CommAlgCat.carrierCommAlgCat.Hom · cited by 2CommAlgCat.HomHom.homCITED BYCITES

Cites6

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

Cited by53

Results whose statement or proof uses this declaration.