A locally closed subset is closed in its open coborder. Its vanishing ideal therefore gives an actual closed subscheme of that open subscheme, and the composite immersion into the original scheme has precisely the given image.
This construction realizes a finite locally closed constructible partition as a ConstructibleStratification. Consequently every finite family of constructible subsets admits such an actual scheme stratification subordinate to it. No noetherianity or quasi-compactness assumption is required.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory
namespace EtaleCohomology
variable {X : Scheme.{u}} {s : Set X}def locallyClosedOpen (hs : IsLocallyClosed s) : X.OpensSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory
namespace EtaleCohomology
variable {X : Scheme.{u}} {s : Set X}def locallyClosedIdeal (hs : IsLocallyClosed s) :
(locallyClosedOpen hs).toScheme.IdealSheafDataThe induced subscheme of a locally closed subset, formed inside its coborder.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory
namespace EtaleCohomology
variable {X : Scheme.{u}} {s : Set X}def locallyClosedSubscheme (hs : IsLocallyClosed s) : Scheme.{u}The inclusion of the induced locally closed subscheme.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory
namespace EtaleCohomology
variable {X : Scheme.{u}} {s : Set X}def locallyClosedSubschemeι (hs : IsLocallyClosed s) : locallyClosedSubscheme hs ⟶ XThe induced locally closed subscheme is immersed in the original scheme.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory
namespace EtaleCohomology
variable {X : Scheme.{u}} {s : Set X}lemma locallyClosedSubschemeι_isImmersion (hs : IsLocallyClosed s) :
IsImmersion (locallyClosedSubschemeι hs)The induced subscheme has exactly the prescribed locally closed image.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory
namespace EtaleCohomology
variable {X : Scheme.{u}} {s : Set X}lemma range_locallyClosedSubschemeι (hs : IsLocallyClosed s) :
Set.range (locallyClosedSubschemeι hs) = sRealize a finite locally closed constructible partition by actual scheme strata.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory
namespace EtaleCohomology
variable {X : Scheme.{u}} {s : Set X}
namespace ConstructibleStratificationdef ofPartition {ι : Type u} [Finite ι] (p : ι → Set X)
(hp : ∀ i : ι, IsLocallyClosed (p i) ∧ Topology.IsConstructible (p i))
(hdisjoint : Pairwise (fun i j : ι => Disjoint (p i) (p j)))
(hcover : (⋃ i : ι, p i) = Set.univ) : ConstructibleStratification X where
I := ι
finite := inferInstance
stratum i := locallyClosedSubscheme (hp i).1
map i := locallyClosedSubschemeι (hp i).1
isImmersion i := locallyClosedSubschemeι_isImmersion (hp i).1
constructible_range i := by
rw [range_locallyClosedSubschemeι]
exact (hp i).2
disjoint := by
intro i j hij
rw [range_locallyClosedSubschemeι, range_locallyClosedSubschemeι]
exact hdisjoint hij
cover x := by
obtain ⟨i, hi⟩ := Set.mem_iUnion.mp (hcover.symm ▸ Set.mem_univ x)
refine ⟨i, ?_⟩
rw [range_locallyClosedSubschemeι]
exact hiThe geometric realization preserves each individual part of the partition.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory
namespace EtaleCohomology
variable {X : Scheme.{u}} {s : Set X}
namespace ConstructibleStratificationlemma ofPartition_range {ι : Type u} [Finite ι] (p : ι → Set X)
(hp : ∀ i : ι, IsLocallyClosed (p i) ∧ Topology.IsConstructible (p i))
(hdisjoint : Pairwise (fun i j : ι => Disjoint (p i) (p j)))
(hcover : (⋃ i : ι, p i) = Set.univ) (i : ι) :
Set.range ((ofPartition p hp hdisjoint hcover).map i) = p i :=
range_locallyClosedSubschemeι (hp i).1A finite family of constructible sets has a subordinate stratification by actual schemes.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v
open AlgebraicGeometry CategoryTheory
namespace EtaleCohomology
variable {X : Scheme.{u}} {s : Set X}
namespace ConstructibleStratificationtheorem exists_subordinate {ι : Type v} [Finite ι] (s : ι → Set X)
(hs : ∀ i : ι, Topology.IsConstructible (s i)) :
∃ S : ConstructibleStratification X, ∀ k : S.I, ∀ i : ι,
Set.range (S.map k) ⊆ s i ∨ Disjoint (Set.range (S.map k)) (s i)