Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.PartialMap.comp

{X Y Z : AlgebraicGeometry.Scheme} →
  [PreirreducibleSpace ↥X] →
    [Nonempty ↥Y] → (f : X.PartialMap Y) → [AlgebraicGeometry.IsDominant f.hom] → Y.PartialMap Z → X.PartialMap Z

Composition of partial maps. The domain of f.comp g is the preimage of g.domain under f, viewed as an open subscheme of X. Requires f.hom to be dominant so that the domain is dense.

Defined in

Mathlib.AlgebraicGeometry.Birational.Composition

Cited by

15 results in Mathlib

Foundations

Depth 144 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PreirreducibleSpaceNonemptyAlgebraicGeometry.IsDominant