Pure-dimensional topological spaces

A topological space is pure-dimensional of dimension d when every irreducible component has Krull dimension d. Empty spaces are pure-dimensional of every dimension, since they have no irreducible components. Thus empty fibres automatically satisfy the pure-dimensional component condition in the definition of a morphism of pure relative dimension.

The property is invariant under homeomorphisms. A discrete space is pure-dimensional of dimension zero: every irreducible component is nonempty and discrete, hence has Krull dimension zero.

Pure dimension is local on spaces in which every nonempty open part Z ∩ U of an irreducible component Z has the Krull dimension of Z, such as schemes locally of finite type over a field: the irreducible components of an open subspace are the traces of the components of the whole space that meet it. Without that hypothesis this fails: the spectrum of a discrete valuation ring is irreducible of dimension one, while its generic point is an open subspace of dimension zero.

Main declarations

• TauCeti.IsPureDimensional: every irreducible component has the prescribed Krull dimension.
• TauCeti.isPureDimensional_iff: the defining condition on irreducible components.
• TauCeti.IsPureDimensional.homeomorph: invariance under homeomorphisms.
• Homeomorph.isPureDimensional_iff: a homeomorphism preserves pure dimension.
• TauCeti.isPureDimensional_zero_of_discreteTopology: discrete spaces have pure dimension zero.
• TauCeti.IsPureDimensional.of_isOpenEmbedding and TauCeti.isPureDimensional_iff_forall_of_isOpenEmbedding: locality of pure dimension on spaces whose irreducible components have all nonempty open parts of full dimension.

References

• Stacks Project, Tag 02NI

def TauCeti.IsPureDimensional (d : ℕ) (X : Type u_1) [TopologicalSpace X] : Prop

A topological space is pure-dimensional of dimension d if every irreducible component has topological Krull dimension d.

Equations

• TauCeti.IsPureDimensional d X = ∀ Z ∈ irreducibleComponents X, topologicalKrullDim ↑Z = ↑d

theorem TauCeti.isPureDimensional_iff {d : ℕ} {X : Type u_1} [TopologicalSpace X] : IsPureDimensional d X ↔ ∀ Z ∈ irreducibleComponents X, topologicalKrullDim ↑Z = ↑d

A space is pure-dimensional of dimension d exactly when each of its irreducible components has Krull dimension d.

@[simp]

theorem TauCeti.isPureDimensional_of_isEmpty (d : ℕ) (X : Type u_1) [TopologicalSpace X] [IsEmpty X] : IsPureDimensional d X

An empty space is pure-dimensional of every dimension.

theorem TauCeti.IsPureDimensional.homeomorph {d : ℕ} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (hX : IsPureDimensional d X) (e : X ≃ₜ Y) : IsPureDimensional d Y

Pure dimension is preserved by a homeomorphism.

theorem Homeomorph.isPureDimensional_iff {d : ℕ} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (e : X ≃ₜ Y) : TauCeti.IsPureDimensional d X ↔ TauCeti.IsPureDimensional d Y

Pure dimension is invariant under a homeomorphism.

theorem TauCeti.isPureDimensional_zero_of_discreteTopology (X : Type u_1) [TopologicalSpace X] [DiscreteTopology X] : IsPureDimensional 0 X

A discrete topological space is pure-dimensional of dimension zero.

theorem TauCeti.IsPureDimensional.of_isOpenEmbedding {d : ℕ} {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (hX : IsPureDimensional d X) (hdim : ∀ Z ∈ irreducibleComponents X, ∀ (U : Set X), IsOpen U → (Z ∩ U).Nonempty → topologicalKrullDim ↑(Z ∩ U) = topologicalKrullDim ↑Z) {e : Y → X} (he : Topology.IsOpenEmbedding e) : IsPureDimensional d Y

Let X be a space in which every nonempty open part of an irreducible component has the Krull dimension of the component. If X is pure-dimensional, then so is every open subspace.

theorem TauCeti.isPureDimensional_iff_forall_of_isOpenEmbedding {d : ℕ} {X : Type u_1} [TopologicalSpace X] {ι : Type u_3} {Y : ι → Type u_4} [(i : ι) → TopologicalSpace (Y i)] (hdim : ∀ Z ∈ irreducibleComponents X, ∀ (U : Set X), IsOpen U → (Z ∩ U).Nonempty → topologicalKrullDim ↑(Z ∩ U) = topologicalKrullDim ↑Z) (e : (i : ι) → Y i → X) (he : ∀ (i : ι), Topology.IsOpenEmbedding (e i)) (hcover : ∀ (x : X), ∃ (i : ι), x ∈ Set.range (e i)) : IsPureDimensional d X ↔ ∀ (i : ι), IsPureDimensional d (Y i)

Let X be a space in which every nonempty open part of an irreducible component has the Krull dimension of the component. Given open embeddings whose ranges cover X, the space X is pure-dimensional exactly when each of their domains is.