Local isomorphisms #
A local isomorphism of schemes is a morphism that is source-locally an open immersion.
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)
Instances
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.le_of_isLocalAtSource
(P : CategoryTheory.MorphismProperty Scheme)
[P.ContainsIdentities]
[IsLocalAtSource P]
:
IsLocalIso
is weaker than every source-Zariski-local property containing identities.
theorem
AlgebraicGeometry.IsLocalIso.eq_iInf :
@IsLocalIso = ⨅ (P : CategoryTheory.MorphismProperty Scheme), ⨅ (_ : P.ContainsIdentities), ⨅ (_ : IsLocalAtSource P), P
IsLocalIso
is the weakest source-Zariski-local property containing identities.