Theorems · Definition · commutative algebra
CommRingCat.Hom.hom
{R S : CommRingCat} → R.Hom S → ↑R →+* ↑SThe underlying ring hom.
- Defined in
- Mathlib.Algebra.Category.Ring.Basic
- Cited by
- 432 results in Mathlib
- Foundations
- Depth 23 from the axioms, rests on 193 definitions · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- RingHomstatement · cited by 10,189
- CategoryTheory.ConcreteCategory.homproof · cited by 4,022
- CommRingCatstatement and proof · cited by 2,333
- CommRingCat.carrierstatement · cited by 1,096
- CommRingCat.Homstatement and proof · cited by 10
Cited by530
Results whose statement or proof uses this declaration.
- CommRingCat.hom_extstatement and proof · cited by 55
- AlgebraicGeometry.Scheme.Hom.kerproof · cited by 51
- CategoryTheory.Iso.commRingCatIsoToRingEquivproof · cited by 44
- AlgebraicGeometry.Scheme.Hom.residueFieldMapproof · cited by 28
- CommRingCat.hom_compstatement · cited by 27
- AlgebraicGeometry.affineAndproof · cited by 21
- AlgebraicGeometry.HasRingHomProperty.Spec_iffstatement and proof · cited by 19
- RingHom.toMorphismPropertyproof · cited by 19
- RingHom.RespectsIso.cancel_right_isIsostatement and proof · cited by 18
- AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpenproof · cited by 18
- AlgebraicGeometry.modulesSpecToSheafproof · cited by 17
- AlgebraicGeometry.Spec.sheafedSpaceMapproof · cited by 16
Showing the 200 most cited of 530.