feat(Topology/KrullDimension): add subspace dimension inequality (#29728)

This PR proves that subspaces have Krull dimension at most that of the ambient space: dim(Y) ≤ dim(X) for Y ⊆ X (theorem topologicalKrullDim_subspace_le).

Supporting results about IrreducibleCloseds were refactored and moved from KrullDimension.lean to Closeds.lean for better modularity.
Note: Some code/documentation generated with AI assistance (Gemini).

Author: a-dangelo

Mathlib/Topology/KrullDimension.lean

@@ -1,9 +1,10 @@
 /-
 Copyright (c) 2024 Jujian Zhang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jujian Zhang, Fangming Li
+Authors: Jujian Zhang, Fangming Li, Alessandro D'Angelo
 -/
 import Mathlib.Order.KrullDimension
+import Mathlib.Topology.Irreducible
 import Mathlib.Topology.Homeomorph.Lemmas
 import Mathlib.Topology.Sets.Closeds
 
@@ -13,9 +14,18 @@ import Mathlib.Topology.Sets.Closeds
 The Krull dimension of a topological space is the order-theoretic Krull dimension applied to the
 collection of all its subsets that are closed and irreducible. Unfolding this definition, it is
 the length of longest series of closed irreducible subsets ordered by inclusion.
+
+## Main results
+
+- `topologicalKrullDim_subspace_le`: For any subspace Y ⊆ X, we have dim(Y) ≤ dim(X)
+
+## Implementation notes
+
+The proofs use order-preserving maps between posets of irreducible closed sets to establish
+dimension inequalities.
 -/
 
-open Order TopologicalSpace Topology
+open Set Function Order TopologicalSpace Topology TopologicalSpace.IrreducibleCloseds
 
 /--
 The Krull dimension of a topological space is the supremum of lengths of chains of
@@ -26,39 +36,28 @@ noncomputable def topologicalKrullDim (T : Type*) [TopologicalSpace T] : WithBot
 
 variable {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
 
-/--
-Map induced on irreducible closed subsets by a closed continuous map `f`.
-This is just a wrapper around the image of `f` together with proofs that it
-preserves irreducibility (by continuity) and closedness (since `f` is closed).
--/
-def IrreducibleCloseds.map {f : X → Y} (hf1 : Continuous f) (hf2 : IsClosedMap f)
-    (c : IrreducibleCloseds X) :
-    IrreducibleCloseds Y where
-  carrier := f '' c
-  isIrreducible' := c.isIrreducible.image f hf1.continuousOn
-  isClosed' := hf2 c c.isClosed
+/-!
+### Main dimension theorems -/
 
-/--
-Taking images under a closed embedding is strictly monotone on the preorder of irreducible closeds.
--/
-lemma IrreducibleCloseds.map_strictMono {f : X → Y} (hf : IsClosedEmbedding f) :
-    StrictMono (IrreducibleCloseds.map hf.continuous hf.isClosedMap) :=
-  fun ⦃_ _⦄ UltV ↦ hf.injective.image_strictMono UltV
+/-- If `f : Y → X` is inducing, then `dim(Y) ≤ dim(X)`. -/
+theorem IsInducing.topologicalKrullDim_le {f : Y → X} (hf : IsInducing f) :
+    topologicalKrullDim Y ≤ topologicalKrullDim X :=
+  krullDim_le_of_strictMono _ (map_strictMono_of_isInducing hf)
 
-/--
-If `f : X → Y` is a closed embedding, then the Krull dimension of `X` is less than or equal
-to the Krull dimension of `Y`.
--/
-theorem IsClosedEmbedding.topologicalKrullDim_le (f : X → Y) (hf : IsClosedEmbedding f) :
-    topologicalKrullDim X ≤ topologicalKrullDim Y :=
-  krullDim_le_of_strictMono _ (IrreducibleCloseds.map_strictMono hf)
+@[deprecated (since := "2025-10-19")]
+alias IsClosedEmbedding.topologicalKrullDim_le := IsInducing.topologicalKrullDim_le
 
 /-- The topological Krull dimension is invariant under homeomorphisms -/
 theorem IsHomeomorph.topologicalKrullDim_eq (f : X → Y) (h : IsHomeomorph f) :
     topologicalKrullDim X = topologicalKrullDim Y :=
   have fwd : topologicalKrullDim X ≤ topologicalKrullDim Y :=
-    IsClosedEmbedding.topologicalKrullDim_le f h.isClosedEmbedding
+    IsInducing.topologicalKrullDim_le h.isClosedEmbedding.toIsInducing
   have bwd : topologicalKrullDim Y ≤ topologicalKrullDim X :=
-    IsClosedEmbedding.topologicalKrullDim_le (h.homeomorph f).symm
-    (h.homeomorph f).symm.isClosedEmbedding
+    IsInducing.topologicalKrullDim_le (h.homeomorph f).symm.isClosedEmbedding.toIsInducing
   le_antisymm fwd bwd
+
+/-- The topological Krull dimension of any subspace is at most the dimension of the
+ambient space. -/
+theorem topologicalKrullDim_subspace_le (X : Type*) [TopologicalSpace X] (Y : Set X) :
+    topologicalKrullDim Y ≤ topologicalKrullDim X :=
+  IsInducing.topologicalKrullDim_le IsInducing.subtypeVal

Mathlib/Topology/Sets/Closeds.lean

@@ -19,7 +19,8 @@ For a topological space `α`,
 -/
 
 
-open Order OrderDual Set
+open Order OrderDual Set Topology
+
 
 variable {ι α β : Type*} [TopologicalSpace α] [TopologicalSpace β]
 
@@ -428,6 +429,39 @@ order isomorphism. -/
 def orderIsoSubtype' : IrreducibleCloseds α ≃o { x : Set α // IsClosed x ∧ IsIrreducible x } :=
   equivSubtype'.toOrderIso (fun _ _ h ↦ h) (fun _ _ h ↦ h)
 
+/-! ### Partial order structure on irreducible closed sets and maps thereof.-/
+
+/-- The map on irreducible closed sets induced by a continuous map `f`. -/
+def map (f : β → α) (hf : Continuous f)
+    (c : IrreducibleCloseds β) : IrreducibleCloseds α where
+  carrier := closure (f '' c)
+  isIrreducible' := c.isIrreducible.image f hf.continuousOn |>.closure
+  isClosed' := isClosed_closure
+
+@[simp]
+lemma coe_map (f : β → α) (hf : Continuous f) (s : IrreducibleCloseds β) :
+    (map f hf s : Set α) = closure (f '' s) :=
+  rfl
+
+lemma map_mono {f : β → α} (hf : Continuous f) : Monotone (map f hf) :=
+  fun _ _ h_le => closure_mono <| Set.image_mono h_le
+
+/-- The map `IrreducibleCloseds.map` is injective when `f` is inducing.
+This relies on the property of embeddings that a closed set in the domain is the preimage
+of the closure of its image. -/
+lemma map_injective_of_isInducing {f : β → α} (hf : IsInducing f) :
+    Function.Injective (map f hf.continuous) := by
+  intro A B h_images_eq
+  apply SetLike.coe_injective
+  replace h_images_eq : closure (f '' A) = closure (f '' B) := congr($h_images_eq)
+  rw [← A.isClosed.closure_eq, hf.closure_eq_preimage_closure_image, h_images_eq,
+    ← hf.closure_eq_preimage_closure_image, B.isClosed.closure_eq]
+
+/-- The map `IrreducibleCloseds.map` is strictly monotone when `f` is inducing. -/
+lemma map_strictMono_of_isInducing {f : β → α} (hf : IsInducing f) :
+    StrictMono (map f hf.continuous) :=
+  Monotone.strictMono_of_injective (map_mono hf.continuous) (map_injective_of_isInducing hf)
+
 end IrreducibleCloseds
 
 end TopologicalSpace