Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.PartialMap.equiv_iff_of_domain_eq_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},
  f.domain = g.domain →
    ∀ [AlgebraicGeometry.Scheme.PartialMap.IsOver S f] [AlgebraicGeometry.Scheme.PartialMap.IsOver S g],
      f.equiv g ↔ f = g

Two partial maps from reduced schemes to separated schemes with the same domain are equivalent if and only if they are equal.

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