Theorems · Definition · algebraic geometry
AlgebraicGeometry.Scheme.PartialMap.hom
{X Y : AlgebraicGeometry.Scheme} → (self : X.PartialMap Y) → ↑self.domain ⟶ YThe underlying morphism of a partial map.
- Cited by
- 49 results in Mathlib
- Foundations
- Depth 137 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement · cited by 32,603
- AlgebraicGeometry.Schemestatement and proof · cited by 2,540
- AlgebraicGeometry.Scheme.Opens.toSchemestatement · cited by 433
- AlgebraicGeometry.Scheme.PartialMapstatement and proof · cited by 76
- AlgebraicGeometry.Scheme.PartialMap.domainstatement · cited by 60
Cited by58
Results whose statement or proof uses this declaration.
- AlgebraicGeometry.Scheme.PartialMap.restrictproof · cited by 31
- AlgebraicGeometry.Scheme.PartialMap.equivproof · cited by 18
- AlgebraicGeometry.Scheme.PartialMap.compstatement and proof · cited by 15
- AlgebraicGeometry.Scheme.PartialMap.extstatement and proof · cited by 12
- AlgebraicGeometry.Scheme.PartialMap.IsOverproof · cited by 11
- AlgebraicGeometry.Scheme.PartialMap.compHomproof · cited by 11
- AlgebraicGeometry.Scheme.PartialMap.fromSpecStalkOfMemproof · cited by 5
- AlgebraicGeometry.Scheme.PartialMap.restrict_homstatement and proof · cited by 3
- AlgebraicGeometry.Scheme.RationalMap.toPartialMapproof · cited by 3
- AlgebraicGeometry.Scheme.PartialMap.comp_equiv_of_equiv_leftstatement and proof · cited by 3
- AlgebraicGeometry.Scheme.PartialMap.comp_toPartialMapstatement and proof · cited by 3
- AlgebraicGeometry.Scheme.PartialMap.equiv.reflproof · cited by 2