Theorems · Definition · algebraic geometry
AlgebraicGeometry.Scheme.IdealSheafData.comap
{X Y : AlgebraicGeometry.Scheme} → Y.IdealSheafData → (X ⟶ Y) → X.IdealSheafDataThe pullback of an ideal sheaf.
- Cited by
- 23 results in Mathlib
- Foundations
- Depth 205 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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 and proof · cited by 2,540
- CategoryTheory.Limits.pullback.fstproof · cited by 639
- AlgebraicGeometry.Scheme.IdealSheafDatastatement and proof · cited by 192
- AlgebraicGeometry.Scheme.Hom.kerproof · cited by 51
- AlgebraicGeometry.Scheme.IdealSheafData.subschemeιproof · cited by 36
Cited by24
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.IdealSheafData.comapIsostatement · cited by 8
- AlgebraicGeometry.Scheme.IdealSheafData.map_gcstatement · cited by 8
- AlgebraicGeometry.Scheme.IdealSheafData.support_comapstatement · cited by 2
- AlgebraicGeometry.Scheme.IdealSheafData.comapIso_hom_fststatement and proof · cited by 2
- AlgebraicGeometry.Scheme.IdealSheafData.comapIso_hom_fst_assocstatement and proof · cited by 2
- AlgebraicGeometry.Scheme.IdealSheafData.comapIso_inv_subschemeιstatement · cited by 2
- AlgebraicGeometry.Scheme.IdealSheafData.le_map_comapstatement · cited by 2
- AlgebraicGeometry.Scheme.IdealSheafData.le_map_iff_comap_lestatement and proof · cited by 2
- AlgebraicGeometry.Scheme.IdealSheafData.ideal_comap_of_isOpenImmersionstatement · cited by 1
- AlgebraicGeometry.Scheme.IdealSheafData.comapIso_hom_sndstatement and proof · cited by 1
- AlgebraicGeometry.Scheme.IdealSheafData.comap_compstatement and proof · cited by 1
- AlgebraicGeometry.Scheme.IdealSheafData.comap_map_lestatement · cited by 1