Theorems · Definition · algebraic geometry
AlgebraicGeometry.Scheme.Hom.ker
{X Y : AlgebraicGeometry.Scheme} → X.Hom Y → Y.IdealSheafDataThe kernel of a morphism,
defined as the largest (quasi-coherent) ideal sheaf contained in the component-wise kernel.
This is usually only well-behaved when f is quasi-compact.
- Cited by
- 51 results in Mathlib
- Foundations
- Depth 165 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Set.Elemproof · cited by 7,166
- AlgebraicGeometry.Schemestatement and proof · cited by 2,540
- CommRingCat.Hom.homproof · cited by 432
- RingHom.kerproof · cited by 363
- AlgebraicGeometry.Scheme.affineOpensproof · cited by 220
- AlgebraicGeometry.Scheme.IdealSheafDatastatement · cited by 192
- AlgebraicGeometry.Scheme.Hom.appproof · cited by 176
- AlgebraicGeometry.Scheme.Homstatement and proof · cited by 35
- AlgebraicGeometry.Scheme.IdealSheafData.ofIdealsproof · cited by 4
Cited by61
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.IdealSheafData.comapproof · cited by 23
- AlgebraicGeometry.Scheme.IdealSheafData.mapproof · cited by 19
- AlgebraicGeometry.Scheme.Hom.ker_applystatement · cited by 14
- AlgebraicGeometry.Scheme.Hom.imageιproof · cited by 13
- AlgebraicGeometry.Scheme.Hom.imageproof · cited by 9
- AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeιstatement · cited by 7
- AlgebraicGeometry.Scheme.Hom.support_kerstatement and proof · cited by 6
- AlgebraicGeometry.IsClosedImmersion.liftstatement and proof · cited by 5
- AlgebraicGeometry.Scheme.Hom.le_ker_compstatement · cited by 5
- AlgebraicGeometry.Scheme.Hom.range_subset_ker_supportstatement and proof · cited by 4
- AlgebraicGeometry.Scheme.kerFunctorproof · cited by 4
- AlgebraicGeometry.IsClosedImmersion.lift_facstatement and proof · cited by 4