Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.PartialIso.restrictSource_iso

∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialIso Y) (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.source),
  (f.restrictSource U hU hU').iso =
    (AlgebraicGeometry.Scheme.Opens.isoOfLE hU').symm ≪≫
      AlgebraicGeometry.Scheme.Hom.isoImage f.iso.hom ((TopologicalSpace.Opens.map f.source.ι.base).obj U) ≪≫
        AlgebraicGeometry.Scheme.Hom.isoImage f.target.ι
          ((AlgebraicGeometry.Scheme.Hom.opensFunctor f.iso.hom).obj
            ((TopologicalSpace.Opens.map f.source.ι.base).obj U))

Defined in

Mathlib.AlgebraicGeometry.Birational.Birational

Cited by

0 results in Mathlib

Foundations

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