Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.PartialMap.equiv_toPartialMap_iff_of_isSeparated

∀ {X Y S : AlgebraicGeometry.Scheme} [inst : X.Over S] [inst_1 : Y.Over S] [AlgebraicGeometry.IsReduced X]
  [AlgebraicGeometry.IsSeparated (Y ↘ S)] {f : X.PartialMap Y} {g : X ⟶ Y}
  [AlgebraicGeometry.Scheme.PartialMap.IsOver S f] [AlgebraicGeometry.Scheme.Hom.IsOver g S],
  f.equiv (AlgebraicGeometry.Scheme.Hom.toPartialMap g) ↔ f.hom = CategoryTheory.CategoryStruct.comp f.domain.ι g

A partial map from a reduced scheme to a separated scheme is equivalent to a morphism if and only if it is equal to the restriction of the morphism.

Defined in

Mathlib.AlgebraicGeometry.Birational.RationalMap

Cited by

0 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.Scheme.OverAlgebraicGeometry.Scheme.OverAlgebraicGeometry.IsReducedAlgebraicGeometry.IsSeparatedAlgebraicGeometry.Scheme.PartialMap.IsOverAlgebraicGeometry.Scheme.Hom.IsOver