Theorems · Inductive type · algebraic geometry
AlgebraicGeometry.Scheme.PartialMap
AlgebraicGeometry.Scheme → AlgebraicGeometry.Scheme → Type u
A partial map from X to Y (X.PartialMap Y) is a morphism into Y
defined on a dense open subscheme of X.
- Cited by
- 76 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AlgebraicGeometry.Schemestatement · cited by 2,540
Cited by106
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.PartialMap.domainstatement and proof · cited by 60
- AlgebraicGeometry.Scheme.PartialMap.homstatement and proof · cited by 49
- AlgebraicGeometry.Scheme.PartialMap.restrictstatement and proof · cited by 31
- AlgebraicGeometry.Scheme.PartialMap.toRationalMapstatement and proof · cited by 26
- AlgebraicGeometry.Scheme.PartialMap.equivstatement and proof · cited by 18
- AlgebraicGeometry.Scheme.PartialMap.compstatement and proof · cited by 15
- AlgebraicGeometry.Scheme.PartialMap.dense_domainstatement and proof · cited by 14
- AlgebraicGeometry.Scheme.PartialMap.extstatement and proof · cited by 12
- AlgebraicGeometry.Scheme.PartialMap.IsOverstatement and proof · cited by 11
- AlgebraicGeometry.Scheme.PartialMap.compHomstatement and proof · cited by 11
- AlgebraicGeometry.Scheme.Hom.toPartialMapstatement · cited by 10
- AlgebraicGeometry.Scheme.PartialMap.toRationalMap_eq_iffstatement and proof · cited by 7