Documentation

Mathlib.AlgebraicGeometry.Morphisms.LocalIso

Local isomorphisms #

A local isomorphism of schemes is a morphism that is source-locally an open immersion.

class AlgebraicGeometry.IsLocalIso {X Y : Scheme} (f : X Y) :

A local isomorphism of schemes is a morphism that is (Zariski-)source-locally an open immersion.

Instances

    IsLocalIso is weaker than every source-Zariski-local property containing identities.

    IsLocalIso is the weakest source-Zariski-local property containing identities.