Unramified morphisms

A morphism of schemes is unramified when it is locally of finite type and formally unramified. This packages the two conditions as a morphism property, so geometric constructions such as the singular subscheme of a nodal family can state the usual unramifiedness condition directly. Since the diagonal of an unramified morphism is an open immersion, open immersions cancel against unramified morphisms on the right (TauCeti.AlgebraicGeometry.Unramified.isOpenImmersion_hasOfPostcompProperty). In particular, in a pullback square along an unramified morphism, the lift of an open immersion is an open immersion (TauCeti.AlgebraicGeometry.isOpenImmersion_lift_of_isPullback). Both conditions satisfy fpqc descent, hence so does unramifiedness (TauCeti.AlgebraicGeometry.Unramified.descendsAlong_surjective_inf_flat_inf_quasicompact).

Main definition

• TauCeti.AlgebraicGeometry.Unramified f: f is locally of finite type and formally unramified.

class TauCeti.AlgebraicGeometry.Unramified {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) extends AlgebraicGeometry.LocallyOfFiniteType f, AlgebraicGeometry.FormallyUnramified f : Prop

A morphism of schemes is unramified if it is locally of finite type and formally unramified.

• finiteType_appLE {U : Y.Opens} : IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FiniteType
• formallyUnramified_appLE {U : Y.Opens} : IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FormallyUnramified

theorem TauCeti.AlgebraicGeometry.unramified_iff {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : Unramified f ↔ AlgebraicGeometry.LocallyOfFiniteType f ∧ AlgebraicGeometry.FormallyUnramified f

theorem TauCeti.AlgebraicGeometry.unramified_eq : @Unramified = @AlgebraicGeometry.LocallyOfFiniteType ⊓ @AlgebraicGeometry.FormallyUnramified

instance TauCeti.AlgebraicGeometry.Unramified.instHasRingHomPropertyAndFiniteTypeFormallyUnramified : AlgebraicGeometry.HasRingHomProperty @Unramified fun {R S : Type u_1} [CommRing R] [CommRing S] (f : R →+* S) => f.FiniteType ∧ f.FormallyUnramified

theorem TauCeti.AlgebraicGeometry.Unramified.Spec_iff {R S : CommRingCat} {φ : R ⟶ S} : Unramified (AlgebraicGeometry.Spec.map φ) ↔ Algebra.Unramified ↑R ↑S

The affine criterion for an unramified morphism.

theorem TauCeti.AlgebraicGeometry.Unramified.of_comp {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [Unramified (CategoryTheory.CategoryStruct.comp f g)] : Unramified f

If a composite is unramified, then its first map is unramified.

instance TauCeti.AlgebraicGeometry.Unramified.instIsStableUnderCompositionScheme : CategoryTheory.MorphismProperty.IsStableUnderComposition @Unramified

instance TauCeti.AlgebraicGeometry.Unramified.isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @Unramified

instance TauCeti.AlgebraicGeometry.Unramified.instIsMultiplicativeScheme : CategoryTheory.MorphismProperty.IsMultiplicative @Unramified

instance TauCeti.AlgebraicGeometry.Unramified.unramified_comp {Y a✝ : AlgebraicGeometry.Scheme} {f : a✝ ⟶ Y} {Z : AlgebraicGeometry.Scheme} (g : Y ⟶ Z) [Unramified f] [Unramified g] : Unramified (CategoryTheory.CategoryStruct.comp f g)

instance TauCeti.AlgebraicGeometry.Unramified.instFstScheme {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [Unramified g] : Unramified (CategoryTheory.Limits.pullback.fst f g)

instance TauCeti.AlgebraicGeometry.Unramified.instSndScheme {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [Unramified f] : Unramified (CategoryTheory.Limits.pullback.snd f g)

@[instance 900]

instance TauCeti.AlgebraicGeometry.Unramified.of_mono {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.Mono f] [AlgebraicGeometry.LocallyOfFiniteType f] : Unramified f

A monomorphism locally of finite type is unramified.

@[instance 900]

instance TauCeti.AlgebraicGeometry.Unramified.instOfEtale {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Etale f] : Unramified f

instance TauCeti.AlgebraicGeometry.Unramified.isOpenImmersion_hasOfPostcompProperty : AlgebraicGeometry.IsOpenImmersion.HasOfPostcompProperty @Unramified

If f ≫ g is an open immersion and g is unramified, then f is an open immersion, since the diagonal of an unramified morphism is an open immersion. In particular, a section of an unramified morphism is an open immersion.

instance TauCeti.AlgebraicGeometry.Unramified.instMorphismRestrict {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (V : Y.Opens) [Unramified f] : Unramified (f ∣_ V)

instance TauCeti.AlgebraicGeometry.Unramified.instResLE {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : X.Opens) (V : Y.Opens) (e : U ≤ (TopologicalSpace.Opens.map f.base).obj V) [Unramified f] : Unramified (AlgebraicGeometry.Scheme.Hom.resLE f V U e)

instance TauCeti.AlgebraicGeometry.Unramified.descendsAlong_surjective_inf_flat_inf_quasicompact : CategoryTheory.MorphismProperty.DescendsAlong (@Unramified) (@AlgebraicGeometry.Surjective ⊓ @AlgebraicGeometry.Flat ⊓ @AlgebraicGeometry.QuasiCompact)

Unramified morphisms satisfy fpqc descent, since both being locally of finite type and being formally unramified do.

theorem TauCeti.AlgebraicGeometry.isOpenImmersion_lift_of_isPullback {Y Z S Z' W : AlgebraicGeometry.Scheme} {g : Z ⟶ S} {f : Y ⟶ S} [Unramified f] {p : Z' ⟶ Z} {g' : Z' ⟶ Y} (H : CategoryTheory.IsPullback p g' g f) {ι : W ⟶ Z} [AlgebraicGeometry.IsOpenImmersion ι] {j : W ⟶ Y} (hcomm : CategoryTheory.CategoryStruct.comp ι g = CategoryTheory.CategoryStruct.comp j f) : AlgebraicGeometry.IsOpenImmersion (H.lift ι j hcomm)

In a pullback square along an unramified morphism f : Y ⟶ S, the lift of an open immersion ι : W ⟶ Z together with a compatible j : W ⟶ Y is an open immersion: it is a section over W of the projection p : Z' ⟶ Z, which is unramified as a base change of f.