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) : Prop

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

• exists_isOpenImmersion (x : ↥X) : ∃ (U : X.Opens), x ∈ U ∧ IsOpenImmersion (CategoryTheory.CategoryStruct.comp U.ι f)

theorem AlgebraicGeometry.isLocalIso_iff {X Y : Scheme} (f : X ⟶ Y) : IsLocalIso f ↔ ∀ (x : ↥X), ∃ (U : X.Opens), x ∈ U ∧ IsOpenImmersion (CategoryTheory.CategoryStruct.comp U.ι f)

theorem AlgebraicGeometry.IsLocalIso.eq_sourceLocalClosure_isOpenImmersion : @IsLocalIso = sourceLocalClosure IsOpenImmersion IsOpenImmersion

instance AlgebraicGeometry.IsLocalIso.instIsZariskiLocalAtSource : IsZariskiLocalAtSource @IsLocalIso

instance AlgebraicGeometry.IsLocalIso.instIsMultiplicativeScheme : CategoryTheory.MorphismProperty.IsMultiplicative @IsLocalIso

instance AlgebraicGeometry.IsLocalIso.instIsStableUnderBaseChangeScheme : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @IsLocalIso

theorem AlgebraicGeometry.IsLocalIso.le_of_isZariskiLocalAtSource (P : CategoryTheory.MorphismProperty Scheme) [P.ContainsIdentities] [IsZariskiLocalAtSource P] : @IsLocalIso ≤ P

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

@[deprecated AlgebraicGeometry.IsLocalIso.le_of_isZariskiLocalAtSource (since := "2025-10-07")]

theorem AlgebraicGeometry.IsLocalIso.le_of_isLocalAtSource (P : CategoryTheory.MorphismProperty Scheme) [P.ContainsIdentities] [IsZariskiLocalAtSource P] : @IsLocalIso ≤ P

Alias of AlgebraicGeometry.IsLocalIso.le_of_isZariskiLocalAtSource.

---

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

theorem AlgebraicGeometry.IsLocalIso.eq_iInf : @IsLocalIso = ⨅ (P : CategoryTheory.MorphismProperty Scheme), ⨅ (_ : P.ContainsIdentities), ⨅ (_ : IsZariskiLocalAtSource P), P

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