Formally unramified morphisms #
A morphism of schemes f : X ⟶ Y is formally unramified if for each affine U ⊆ Y and
V ⊆ f ⁻¹' U, the induced map Γ(Y, U) ⟶ Γ(X, V) is formally unramified.
We show that these properties are local, and are stable under compositions and base change.
A morphism of schemes f : X ⟶ Y is formally unramified if for each affine U ⊆ Y and
V ⊆ f ⁻¹' U, The induced map Γ(Y, U) ⟶ Γ(X, V) is formally unramified.
- formallyUnramified_of_affine_subset (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U) : (Scheme.Hom.appLE f (↑U) (↑V) e).hom.FormallyUnramified
Instances
theorem
AlgebraicGeometry.formallyUnramified_iff
{X Y : Scheme}
(f : X ⟶ Y)
:
FormallyUnramified f ↔ ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U),
(Scheme.Hom.appLE f (↑U) (↑V) e).hom.FormallyUnramified
instance
AlgebraicGeometry.FormallyUnramified.instHasRingHomPropertyFormallyUnramified :
HasRingHomProperty @FormallyUnramified fun {R S : Type u_1} [CommRing R] [CommRing S] => RingHom.FormallyUnramified
@[instance 900]
instance
AlgebraicGeometry.FormallyUnramified.instOfIsOpenImmersionDiagonalScheme
{X Y : Scheme}
(f : X ⟶ Y)
[IsOpenImmersion (CategoryTheory.Limits.pullback.diagonal f)]
:
f : X ⟶ S is formally unramified if X ⟶ X ×ₛ X is an open immersion.
In particular, monomorphisms (e.g. immersions) are formally unramified.
The converse is true if f is locally of finite type.
theorem
AlgebraicGeometry.FormallyUnramified.of_comp
{X Y Z : Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[FormallyUnramified (CategoryTheory.CategoryStruct.comp f g)]
: