Theorems · Theorem · algebraic geometry
AlgebraicGeometry.Scheme.IdealSheafData.le_map_comap
∀ {X Y : AlgebraicGeometry.Scheme} (J : Y.IdealSheafData) (f : X ⟶ Y), J ≤ (J.comap f).map f- Cited by
- 2 results in Mathlib
- Foundations
- Depth 230 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 and proof · cited by 2,540
- AlgebraicGeometry.Scheme.IdealSheafDatastatement and proof · cited by 192
- GaloisConnection.le_u_lproof · cited by 52
- AlgebraicGeometry.Scheme.IdealSheafData.comapstatement · cited by 23
- AlgebraicGeometry.Scheme.IdealSheafData.mapstatement · cited by 19
- AlgebraicGeometry.Scheme.IdealSheafData.map_gcproof · cited by 8
Cited by2
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.IdealSheafData.comapIso_hom_sndstatement and proof · cited by 1
- AlgebraicGeometry.Scheme.IdealSheafData.comapIso_hom_snd_assocstatement and proof · cited by 0