Documentation

TauCeti.AlgebraicGeometry.Morphisms.PureRelativeDimension

Morphisms of pure relative dimension #

A morphism of schemes has pure relative dimension d when it has relative dimension at most d and every irreducible component of every nonempty fibre has dimension exactly d. Empty fibres impose no component condition. The definition is expressed using set-theoretic fibres; Mathlib's homeomorphism between a scheme-theoretic fibre and the corresponding set-theoretic fibre gives the equivalent scheme-theoretic formulation.

The explicit dimension bound is included because the definition makes sense without a finiteness hypothesis. For locally finite type morphisms it follows mathematically from equidimensionality of the locally Noetherian fibres. Keeping it in the predicate makes the generally useful implication to RelativeDimensionLE available without silently assuming local finite type.

Locally quasi-finite morphisms supply the basic example: their fibres are discrete and therefore pure zero-dimensional. The property is invariant under isomorphisms of arrows and local on the target. For morphisms locally of finite type it is also local on the source: the fibres are then locally of finite type over a field, where a nonempty open part of an irreducible component has the dimension of the component, so pure-dimensionality of a fibre can be tested on an open cover. Without the finiteness hypothesis locality on the source fails already for Spec k[x]_(x) → Spec k: its only fibre is irreducible of dimension one, while its open generic point has dimension zero.

For morphisms locally of finite type the property is stable under arbitrary base change. The fibre of a base change is the base change of a fibre along an extension of residue fields, and a scheme locally of finite type over a field is pure-dimensional of dimension d exactly when its extension of scalars to a larger field is (TauCeti.AlgebraicGeometry.isPureDimensional_pullback_Spec_map_iff_of_field).

Main declarations #

References #

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

A morphism of schemes has pure relative dimension d if it has relative dimension at most d and every irreducible component of every set-theoretic fibre has Krull dimension d.

Instances
    source
    theorem TauCeti.AlgebraicGeometry.pureRelativeDimension_iff (d : ℕ) {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :
    PureRelativeDimension d f ↔ RelativeDimensionLE d f ∧ ∀ (y : ↥Y), IsPureDimensional d ↑(⇑f ⁻¹' {y})
    source
    theorem TauCeti.AlgebraicGeometry.pureRelativeDimension_iff_relativeDimensionLE_and_isPureDimensional_fiber {d : ℕ} {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :
    PureRelativeDimension d f ↔ RelativeDimensionLE d f ∧ ∀ (y : ↥Y), IsPureDimensional d ↥(AlgebraicGeometry.Scheme.Hom.fiber f y)

    A morphism has pure relative dimension d if and only if it has relative dimension at most d and every scheme-theoretic fibre is pure-dimensional of dimension d.

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

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

    source
    theorem TauCeti.AlgebraicGeometry.PureRelativeDimension.isPureDimensional_fiber {d : ℕ} {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [PureRelativeDimension d f] (y : ↥Y) :
    IsPureDimensional d ↥(AlgebraicGeometry.Scheme.Hom.fiber f y)

    Every scheme-theoretic fibre of a morphism of pure relative dimension d is pure-dimensional of dimension d.

    source
    @[instance 100]
    instance TauCeti.AlgebraicGeometry.PureRelativeDimension.of_locallyQuasiFinite {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyQuasiFinite f] :
    PureRelativeDimension 0 f

    A locally quasi-finite morphism has pure relative dimension zero.

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

    Having pure relative dimension d is invariant under isomorphisms of arrows.

    source
    instance TauCeti.AlgebraicGeometry.PureRelativeDimension.isOpenImmersion_comp {d : ℕ} {X Y Z : AlgebraicGeometry.Scheme} (i : Z ⟶ X) [AlgebraicGeometry.IsOpenImmersion i] (f : X ⟶ Y) [AlgebraicGeometry.LocallyOfFiniteType f] [PureRelativeDimension d f] :
    PureRelativeDimension d (CategoryTheory.CategoryStruct.comp i f)

    Precomposing a morphism locally of finite type with an open immersion preserves pure relative dimension.

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

    Having pure relative dimension d is local on the target.

    source
    theorem TauCeti.AlgebraicGeometry.PureRelativeDimension.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] [PureRelativeDimension d f] :
    PureRelativeDimension d snd

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

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

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

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

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

    source
    theorem TauCeti.AlgebraicGeometry.pureRelativeDimension_iff_of_openCover {d : ℕ} {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.LocallyOfFiniteType f] (𝒰 : X.OpenCover) :
    PureRelativeDimension d f ↔ ∀ (i : 𝒰.I₀), PureRelativeDimension d (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)

    A morphism locally of finite type has pure relative dimension d exactly when its restrictions to the members of an open cover of the source do.

    source
    theorem TauCeti.AlgebraicGeometry.pureRelativeDimension_iff_of_field {d : ℕ} {X : AlgebraicGeometry.Scheme} {K : Type u} [Field K] (f : X ⟶ AlgebraicGeometry.Spec ↧K) :
    PureRelativeDimension d f ↔ RelativeDimensionLE d f ∧ IsPureDimensional d ↥X

    Over a field, a morphism has pure relative dimension d exactly when its source is pure-dimensional of dimension d and the morphism has relative dimension at most d.