Mathlib Map

Theorems · Theorem · algebraic geometry

AlgebraicGeometry.IsIntegralHom.SpecMap_iff

∀ {R S : CommRingCat} {φ : R ⟶ S},
  AlgebraicGeometry.IsIntegralHom (AlgebraicGeometry.Spec.map φ) ↔ (CommRingCat.Hom.hom φ).IsIntegral
Defined in
Mathlib.AlgebraicGeometry.Morphisms.Integral
Cited by
2 results in Mathlib
Foundations
Depth 175 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

AlgebraicGeometry.IsIntegralHom.iff_universallyClosed_and_isAffineHom · cited by 2IsIntegralHom.iff_univers…AlgebraicGeometry.isIntegral_appTop_of_universallyClosed · cited by 1AlgebraicGeometry.isInteg…Quiver.Hom · cited by 32603Quiver.HomCommRing · cited by 17173CommRingRingHom · cited by 10189RingHomCommRingCat · cited by 2333CommRingCatCommRingCat.carrier · cited by 1096CommRingCat.carrierCategoryTheory.Iso.symm · cited by 993Iso.symmAlgebraicGeometry.Spec · cited by 626AlgebraicGeometry.SpecCommRingCat.Hom.hom · cited by 432Hom.homAlgebraicGeometry.Spec.map · cited by 332Spec.mapCategoryTheory.MorphismProperty.RespectsIso · cited by 248MorphismProperty.Respects…CategoryTheory.MorphismProperty.arrow_mk_iso_iff · cited by 78MorphismProperty.arrow_mk…RingHom.IsIntegral · cited by 54RingHom.IsIntegralAlgebraicGeometry.HasAffineProperty.iff_of_isAffine · cited by 21HasAffineProperty.iff_of_…RingHom.toMorphismProperty · cited by 19RingHom.toMorphismPropertyAlgebraicGeometry.IsIntegralHom · cited by 18AlgebraicGeometry.IsInteg…IsIntegralHom.SpecMap_iffCITED BYCITES

Cites18

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

Cited by2

Results whose statement or proof uses this declaration.