Theorems · Theorem · algebraic geometry
AlgebraicGeometry.Scheme.IdealSheafData.map_ideal
∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) {U V : ↑X.affineOpens} (h : U ≤ V),
Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE h).op)) (I.ideal V) = I.ideal U- Cited by
- 5 results in Mathlib
- Foundations
- Depth 158 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites43
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Quiver.Homproof · cited by 32,603
- CategoryTheory.Functor.objstatement and proof · cited by 19,642
- Semiringproof · cited by 13,802
- RingHomstatement and proof · cited by 10,189
- CategoryTheory.Functor.mapstatement and proof · cited by 8,698
- Oppositestatement · cited by 8,081
- Set.Elemstatement and proof · cited by 7,166
- Idealstatement and proof · cited by 4,748
- TopCat.carrierstatement and proof · cited by 3,184
- FunLikeproof · cited by 2,560
- AlgebraicGeometry.Schemestatement and proof · cited by 2,540
Cited by5
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_comap_idealproof · cited by 4
- AlgebraicGeometry.Scheme.IdealSheafData.le_of_isAffineproof · cited by 2
- AlgebraicGeometry.Scheme.IdealSheafData.map_ideal'proof · cited by 1
- AlgebraicGeometry.Scheme.IdealSheafData.le_of_iSup_eq_topproof · cited by 1