Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.PartialMap.equiv_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 g : X.PartialMap Y} [AlgebraicGeometry.Scheme.PartialMap.IsOver S f]
  [AlgebraicGeometry.Scheme.PartialMap.IsOver S g],
  f.equiv g ↔ (f.restrict (f.domain ⊓ g.domain) ⋯ ⋯).hom = (g.restrict (f.domain ⊓ g.domain) ⋯ ⋯).hom

Two partial maps from reduced schemes to separated schemes are equivalent if and only if they are equal on the intersection of the domains.

Defined in

Mathlib.AlgebraicGeometry.Birational.RationalMap

Cited by

1 results in Mathlib

Foundations

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

Assumes

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