Theorems · Definition · algebraic geometry
AlgebraicGeometry.LocallyRingedSpace.Hom.toHom
{X Y : AlgebraicGeometry.LocallyRingedSpace} → X.Hom Y → X.Hom Y.toPresheafedSpace- Cited by
- 995 results in Mathlib
- Foundations
- Depth 22 from the axioms, rests on 192 definitions · uses propext, 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.
- CommRingCatstatement · cited by 2,333
- AlgebraicGeometry.SheafedSpace.toPresheafedSpacestatement · cited by 1,988
- AlgebraicGeometry.LocallyRingedSpace.toSheafedSpacestatement · cited by 1,892
- AlgebraicGeometry.LocallyRingedSpacestatement and proof · cited by 205
- AlgebraicGeometry.PresheafedSpace.Homstatement · cited by 32
- AlgebraicGeometry.LocallyRingedSpace.Homstatement and proof · cited by 23
Cited by1,149
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.Hom.appstatement and proof · cited by 176
- AlgebraicGeometry.Scheme.Hom.appLEstatement and proof · cited by 138
- AlgebraicGeometry.Scheme.Hom.opensRangeproof · cited by 113
- AlgebraicGeometry.morphismRestrictstatement · cited by 90
- AlgebraicGeometry.Scheme.Hom.stalkMapstatement · cited by 82
- AlgebraicGeometry.Scheme.Hom.resLEstatement and proof · cited by 45
- AlgebraicGeometry.Scheme.Hom.continuousstatement and proof · cited by 41
- AlgebraicGeometry.Scheme.Hom.preimage_image_eqstatement and proof · cited by 37
- AlgebraicGeometry.Scheme.isBasis_affineOpensproof · cited by 37
- AlgebraicGeometry.topologicallyproof · cited by 35
- AlgebraicGeometry.Scheme.Hom.isOpenEmbeddingstatement · cited by 35
- AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMapstatement · cited by 34
Showing the 200 most cited of 1,149.