Mathlib Map

Theorems · Inductive type · algebraic geometry

AlgebraicGeometry.Scheme.PartialIso

AlgebraicGeometry.Scheme → AlgebraicGeometry.Scheme → Type u

A partial isomorphism from X to Y is an isomorphism between dense open subschemes of X and Y.

Defined in
Mathlib.AlgebraicGeometry.Birational.Birational
Cited by
32 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

AlgebraicGeometry.Scheme.PartialIso.source · cited by 30PartialIso.sourceAlgebraicGeometry.Scheme.PartialIso.target · cited by 28PartialIso.targetAlgebraicGeometry.Scheme.PartialIso.iso · cited by 17PartialIso.isoAlgebraicGeometry.Scheme.PartialIso.symm · cited by 11PartialIso.symmAlgebraicGeometry.Scheme.PartialIso.restrictSource · cited by 10PartialIso.restrictSourceAlgebraicGeometry.Scheme.BirationalOver · cited by 10Scheme.BirationalOverAlgebraicGeometry.Scheme.Opens.partialIsoOfDense · cited by 8Opens.partialIsoOfDenseAlgebraicGeometry.Scheme.PartialIso.IsOver · cited by 6PartialIso.IsOverAlgebraicGeometry.Scheme.PartialIso.trans · cited by 6PartialIso.transAlgebraicGeometry.Scheme.Hom.partialIso · cited by 5Hom.partialIsoAlgebraicGeometry.Scheme.PartialIso.refl · cited by 5PartialIso.reflAlgebraicGeometry.Scheme.PartialIso.restrictTarget · cited by 5PartialIso.restrictTargetAlgebraicGeometry.Scheme.Birational · cited by 5Scheme.BirationalAlgebraicGeometry.Scheme.PartialIso.ofIso · cited by 4PartialIso.ofIsoAlgebraicGeometry.Scheme.PartialIso.trans' · cited by 4PartialIso.trans'AlgebraicGeometry.Scheme · cited by 2540AlgebraicGeometry.SchemeScheme.PartialIsoCITED BYCITES

Cites1

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by57

Results whose statement or proof uses this declaration.