Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.PartialMap.equiv_iff_of_isSeparated_of_le

∀ {X Y S : AlgebraicGeometry.Scheme} [inst : X.Over S] [inst_1 : Y.Over S] [AlgebraicGeometry.IsReduced X]
  [AlgebraicGeometry.IsSeparated (Y ↘ S)] {f g : X.PartialMap Y} [AlgebraicGeometry.Scheme.PartialMap.IsOver S f]
  [AlgebraicGeometry.Scheme.PartialMap.IsOver S g] {W : X.Opens} (hW : Dense ↑W) (hWl : W ≤ f.domain)
  (hWr : W ≤ g.domain), f.equiv g ↔ (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom

Two partial maps from reduced schemes to separated schemes are equivalent if and only if they are equal on any open dense subset.

Defined in

Mathlib.AlgebraicGeometry.Birational.RationalMap

Cited by

2 results in Mathlib

Foundations

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

Assumes

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