Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Hom.partialIso_iso

∀ {X U : AlgebraicGeometry.Scheme} (f : U ⟶ X) [inst : AlgebraicGeometry.IsOpenImmersion f]
  [inst_1 : AlgebraicGeometry.IsDominant f],
  (AlgebraicGeometry.Scheme.Hom.partialIso f).iso =
    U.topIso ≪≫
      AlgebraicGeometry.Scheme.Hom.isoOpensRange f ≪≫
        (↑(AlgebraicGeometry.Scheme.Hom.opensRange f)).topIso.symm ≪≫
          (↑(AlgebraicGeometry.Scheme.Hom.opensRange f)).isoOfEq ⋯ ≪≫
            ((AlgebraicGeometry.Scheme.Hom.opensRange f).partialIsoOfDense ⋯).iso

Defined in

Mathlib.AlgebraicGeometry.Birational.Birational

Cited by

1 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.IsOpenImmersionAlgebraicGeometry.IsDominant