Documentation

Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

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.

source
instance Algebra.FormallyUnramified.isOpenImmersion_SpecMap_lmul {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] [FormallyUnramified R S] [EssFiniteType R S] :
AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (TensorProduct.lmul' R).toRingHom))

If S is a formally unramified R-algebra, essentially of finite type, the diagonal is an open immersion.

source
class AlgebraicGeometry.FormallyUnramified {X Y : Scheme} (f : X ⟶ Y) :
Prop

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.

Instances
    source
    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), (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e)).FormallyUnramified
    source
    instance AlgebraicGeometry.FormallyUnramified.instHasRingHomPropertyFormallyUnramified :
    HasRingHomProperty @FormallyUnramified fun {R S : Type u_1} [CommRing R] [CommRing S] => RingHom.FormallyUnramified
    source
    instance AlgebraicGeometry.FormallyUnramified.instIsStableUnderCompositionScheme :
    CategoryTheory.MorphismProperty.IsStableUnderComposition @FormallyUnramified
    source
    @[instance 900]
    instance AlgebraicGeometry.FormallyUnramified.instOfIsOpenImmersionDiagonalScheme {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion (CategoryTheory.Limits.pullback.diagonal f)] :
    FormallyUnramified 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.

    source
    theorem AlgebraicGeometry.FormallyUnramified.of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [FormallyUnramified (CategoryTheory.CategoryStruct.comp f g)] :
    FormallyUnramified f
    source
    instance AlgebraicGeometry.FormallyUnramified.instIsMultiplicativeScheme :
    CategoryTheory.MorphismProperty.IsMultiplicative @FormallyUnramified
    source
    instance AlgebraicGeometry.FormallyUnramified.instIsStableUnderBaseChangeScheme :
    CategoryTheory.MorphismProperty.IsStableUnderBaseChange @FormallyUnramified
    source
    theorem AlgebraicGeometry.FormallyUnramified.AlgebraicGeometry.FormallyUnramified.isOpenImmersion_diagonal {X Y : Scheme} (f : X ⟶ Y) [FormallyUnramified f] [LocallyOfFiniteType f] :
    IsOpenImmersion (CategoryTheory.Limits.pullback.diagonal f)

    The diagonal of a formally unramified morphism of finite type is an open immersion.