Morphisms of relative dimension at most d

A morphism of schemes f : X ⟶ Y has relative dimension at most d if every scheme-theoretic fibre f.fiber y has Krull dimension at most d. This is the fibrewise dimension bound in the definition of a family of curves: a proper, flat, finitely presented morphism of relative dimension at most one.

The fibre f.fiber y is homeomorphic to the set-theoretic fibre f ⁻¹' {y}, so the condition is topological. It is invariant under isomorphisms and local on both the source and the target in the Zariski topology. For a morphism locally of finite type it is stable under arbitrary base change: the fibre of a base change at y' is the base change of the fibre at the image of y' along the extension of residue fields, which does not change the Krull dimension of a scheme locally of finite type over a field. Without a finiteness hypothesis the bound is not stable under base change: Spec K → Spec k has relative dimension zero for every field extension K / k, while Spec (K ⊗[k] K) can have positive dimension when K / k is transcendental.

Relative dimensions add up under composition of morphisms locally of finite type. The input is the fibrewise dimension inequality: if f : X ⟶ Y is a morphism of locally Noetherian schemes of relative dimension at most d, then dim X ≤ dim Y + d. On affine charts this is the bound dim S ≤ dim R + d for a Noetherian algebra S over a Noetherian ring R whose fibres κ(p) ⊗[R] S have dimension at most d (ringKrullDim_le_ringKrullDim_add_of_ringKrullDim_fiber_le). The fibre of f ≫ g over a point z is the base change of f along the fibre of g over z, a scheme locally of finite type over the field κ(z), so the inequality bounds its dimension by e + d.

Main declarations

• TauCeti.AlgebraicGeometry.RelativeDimensionLE d f: every fibre of f has Krull dimension at most d.
• TauCeti.AlgebraicGeometry.relativeDimensionLE_iff_topologicalKrullDim_preimage_le: the condition in terms of set-theoretic fibres.
• TauCeti.AlgebraicGeometry.topologicalKrullDim_fiber_inter_eq: in a fibre of a morphism locally of finite type, a nonempty open part of an irreducible component has the dimension of the component.
• TauCeti.AlgebraicGeometry.isOpenEmbedding_fiber: the fibre of the restriction of a morphism to an open subscheme is an open subspace of the fibre of the morphism.
• TauCeti.AlgebraicGeometry.RelativeDimensionLE.isZariskiLocalAtSource and TauCeti.AlgebraicGeometry.RelativeDimensionLE.isZariskiLocalAtTarget: locality.
• TauCeti.AlgebraicGeometry.RelativeDimensionLE.of_isPullback: stability under base change of morphisms locally of finite type.
• TauCeti.AlgebraicGeometry.relativeDimensionLE_iff_of_field: over a field, the condition bounds the Krull dimension of the source.
• TauCeti.AlgebraicGeometry.relativeDimensionLE_SpecMap_iff: for Spec S ⟶ Spec R, the condition bounds the Krull dimensions of the fibre rings κ(p) ⊗[R] S.
• TauCeti.AlgebraicGeometry.topologicalKrullDim_le_add_of_relativeDimensionLE: for a morphism of locally Noetherian schemes of relative dimension at most d, dim X ≤ dim Y + d.
• TauCeti.AlgebraicGeometry.RelativeDimensionLE.comp: relative dimensions at most d and e compose to relative dimension at most d + e for morphisms locally of finite type.

References

• Stacks Project, Tag 02NI
• Stacks Project, Tag 0C59
• Stacks Project, Tag 00OM, the local form of the fibrewise dimension inequality

class TauCeti.AlgebraicGeometry.RelativeDimensionLE (d : ℕ) {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : Prop

A morphism of schemes f : X ⟶ Y has relative dimension at most d if every scheme-theoretic fibre f.fiber y has Krull dimension at most d.

• topologicalKrullDim_fiber_le (y : ↥Y) : topologicalKrullDim ↥(AlgebraicGeometry.Scheme.Hom.fiber f y) ≤ ↑d

theorem TauCeti.AlgebraicGeometry.relativeDimensionLE_iff_topologicalKrullDim_preimage_le {d : ℕ} {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : RelativeDimensionLE d f ↔ ∀ (y : ↥Y), topologicalKrullDim ↑(⇑f ⁻¹' {y}) ≤ ↑d

A morphism has relative dimension at most d if and only if every set-theoretic fibre has Krull dimension at most d.

theorem TauCeti.AlgebraicGeometry.RelativeDimensionLE.topologicalKrullDim_preimage_le {d : ℕ} {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [RelativeDimensionLE d f] (y : ↥Y) : topologicalKrullDim ↑(⇑f ⁻¹' {y}) ≤ ↑d

Every set-theoretic fibre of a morphism of relative dimension at most d has Krull dimension at most d.

theorem TauCeti.AlgebraicGeometry.RelativeDimensionLE.mono {d e : ℕ} {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [RelativeDimensionLE d f] (hde : d ≤ e) : RelativeDimensionLE e f

A morphism of relative dimension at most d has relative dimension at most every e ≥ d.

theorem TauCeti.AlgebraicGeometry.topologicalKrullDim_fiber_inter_eq {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyOfFiniteType f] (y : ↥Y) (C : Set ↥(AlgebraicGeometry.Scheme.Hom.fiber f y)) : C ∈ irreducibleComponents ↥(AlgebraicGeometry.Scheme.Hom.fiber f y) → ∀ (U : Set ↥(AlgebraicGeometry.Scheme.Hom.fiber f y)), IsOpen U → (C ∩ U).Nonempty → topologicalKrullDim ↑(C ∩ U) = topologicalKrullDim ↑C

In a fibre of a morphism locally of finite type, a nonempty open part of an irreducible component has the dimension of the component.

theorem TauCeti.AlgebraicGeometry.isOpenEmbedding_fiber {X Y Z : AlgebraicGeometry.Scheme} (i : Z ⟶ X) [AlgebraicGeometry.IsOpenImmersion i] (f : X ⟶ Y) (y : ↥Y) : Topology.IsOpenEmbedding (⇑(AlgebraicGeometry.Scheme.Hom.fiberHomeo f y).symm ∘ (⇑f ⁻¹' {y}).restrictPreimage ⇑i)

The fibre over y of the restriction of f along an open immersion i is an open subspace of the scheme-theoretic fibre of f over y.

instance TauCeti.AlgebraicGeometry.RelativeDimensionLE.isPreimmersion_comp {d : ℕ} {X Y Z : AlgebraicGeometry.Scheme} (i : Z ⟶ X) [AlgebraicGeometry.IsPreimmersion i] (f : X ⟶ Y) [RelativeDimensionLE d f] : RelativeDimensionLE d (CategoryTheory.CategoryStruct.comp i f)

Precomposing with a preimmersion, such as an open or closed immersion, preserves the bound on the relative dimension.

theorem TauCeti.AlgebraicGeometry.relativeDimensionLE_comp_iff_of_injective {d : ℕ} {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) (hg : Function.Injective ⇑g) : RelativeDimensionLE d (CategoryTheory.CategoryStruct.comp f g) ↔ RelativeDimensionLE d f

Postcomposing with a morphism that is injective on points does not change the relative dimension.

instance TauCeti.AlgebraicGeometry.RelativeDimensionLE.comp_isPreimmersion {d : ℕ} {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [RelativeDimensionLE d f] (g : Y ⟶ Z) [AlgebraicGeometry.IsPreimmersion g] : RelativeDimensionLE d (CategoryTheory.CategoryStruct.comp f g)

Postcomposing with a preimmersion, such as an open or closed immersion, preserves the bound on the relative dimension.

@[instance 100]

instance TauCeti.AlgebraicGeometry.RelativeDimensionLE.of_locallyQuasiFinite {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyQuasiFinite f] : RelativeDimensionLE 0 f

A locally quasi-finite morphism, such as a finite morphism or an immersion, has relative dimension zero: its fibres are discrete.

instance TauCeti.AlgebraicGeometry.RelativeDimensionLE.respectsIso (d : ℕ) : CategoryTheory.MorphismProperty.RespectsIso (@RelativeDimensionLE d)

Having relative dimension at most d is invariant under isomorphisms of arrows.

instance TauCeti.AlgebraicGeometry.RelativeDimensionLE.isZariskiLocalAtSource (d : ℕ) : AlgebraicGeometry.IsZariskiLocalAtSource (@RelativeDimensionLE d)

Having relative dimension at most d is local on the source.

instance TauCeti.AlgebraicGeometry.RelativeDimensionLE.isZariskiLocalAtTarget (d : ℕ) : AlgebraicGeometry.IsZariskiLocalAtTarget (@RelativeDimensionLE d)

Having relative dimension at most d is local on the target.

theorem TauCeti.AlgebraicGeometry.RelativeDimensionLE.of_isPullback {d : ℕ} {X Y Z P : AlgebraicGeometry.Scheme} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} (h : CategoryTheory.IsPullback fst snd f g) [AlgebraicGeometry.LocallyOfFiniteType f] [RelativeDimensionLE d f] : RelativeDimensionLE d snd

Having relative dimension at most d is stable under base change of morphisms locally of finite type.

instance TauCeti.AlgebraicGeometry.RelativeDimensionLE.pullback_snd {d : ℕ} {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.LocallyOfFiniteType f] [RelativeDimensionLE d f] : RelativeDimensionLE d (CategoryTheory.Limits.pullback.snd f g)

The base change pullback.snd f g of a morphism f locally of finite type has relative dimension at most that of f.

instance TauCeti.AlgebraicGeometry.RelativeDimensionLE.pullback_fst {d : ℕ} {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.LocallyOfFiniteType g] [RelativeDimensionLE d g] : RelativeDimensionLE d (CategoryTheory.Limits.pullback.fst f g)

The base change pullback.fst f g of a morphism g locally of finite type has relative dimension at most that of g.

theorem TauCeti.AlgebraicGeometry.relativeDimensionLE_SpecMap_iff {d : ℕ} (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] : RelativeDimensionLE d (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S))) ↔ ∀ (p : Ideal R) [inst : p.IsPrime], ringKrullDim (p.Fiber S) ≤ ↑d

The morphism Spec S ⟶ Spec R induced by an R-algebra S has relative dimension at most d if and only if every fibre ring κ(p) ⊗[R] S has Krull dimension at most d.

theorem TauCeti.AlgebraicGeometry.topologicalKrullDim_le_add_of_relativeDimensionLE {d : ℕ} {X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] [AlgebraicGeometry.IsLocallyNoetherian Y] (f : X ⟶ Y) [RelativeDimensionLE d f] : topologicalKrullDim ↥X ≤ topologicalKrullDim ↥Y + ↑d

If f : X ⟶ Y is a morphism of locally Noetherian schemes of relative dimension at most d, then the Krull dimension of X is at most the Krull dimension of Y plus d.

instance TauCeti.AlgebraicGeometry.RelativeDimensionLE.comp {d e : ℕ} {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.LocallyOfFiniteType f] [AlgebraicGeometry.LocallyOfFiniteType g] [RelativeDimensionLE d f] [RelativeDimensionLE e g] : RelativeDimensionLE (d + e) (CategoryTheory.CategoryStruct.comp f g)

If f : X ⟶ Y and g : Y ⟶ Z are locally of finite type of relative dimensions at most d and e, then f ≫ g has relative dimension at most d + e.

theorem TauCeti.AlgebraicGeometry.relativeDimensionLE_iff_of_field {d : ℕ} {X : AlgebraicGeometry.Scheme} {K : Type u} [Field K] (f : X ⟶ AlgebraicGeometry.Spec ↧K) : RelativeDimensionLE d f ↔ topologicalKrullDim ↥X ≤ ↑d

A scheme over a field has relative dimension at most d over it if and only if its Krull dimension is at most d.