Theorems · Definition · algebraic geometry
AlgebraicGeometry.Spec.preimage
{R S : CommRingCat} → (AlgebraicGeometry.Spec S ⟶ AlgebraicGeometry.Spec R) → (R ⟶ S)The preimage under Spec.
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 141 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement and proof · cited by 32,603
- AlgebraicGeometry.Schemestatement · cited by 2,540
- CommRingCatstatement and proof · cited by 2,333
- Quiver.Hom.unopproof · cited by 903
- AlgebraicGeometry.Specstatement and proof · cited by 626
- AlgebraicGeometry.Scheme.Specproof · cited by 57
- CategoryTheory.Functor.preimageproof · cited by 55
Cited by17
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Spec.map_surjectiveproof · cited by 25
- AlgebraicGeometry.Spec.map_preimagestatement · cited by 11
- AlgebraicGeometry.residueFieldIsoBaseproof · cited by 6
- AlgebraicGeometry.Spec.homEquivproof · cited by 5
- AlgebraicGeometry.Spec.preimage_compstatement and proof · cited by 2
- AlgebraicGeometry.IsIntegralHom.iff_universallyClosed_and_isAffineHomproof · cited by 2
- AlgebraicGeometry.Spec.preimage_mapstatement and proof · cited by 1
- AlgebraicGeometry.pointsPi_surjective_of_isAffineproof · cited by 1
- AlgebraicGeometry.Spec.homEquiv_applystatement · cited by 1
- AlgebraicGeometry.eq_bot_of_comp_quotientMk_eq_sigmaSpecproof · cited by 1
- AlgebraicGeometry.eq_of_SpecMap_comp_eq_of_isAffineOpenproof · cited by 1