5.23 Spectral spaces to 5.30 Topological groups, rings…

Section5.23 Spectral spaces #

Section 5.23 of the Stacks Project, Tag 08YF. 14 tags here are carried by 18 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0901, a lemma

Tag 0901 in the Stacks Project.

withConstructibleTopology_t2_totallyDisconnected_compact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/ConstructibleProfinite.lean, line 97. References: EGA IV (1.9.15), “(ii)(iii) suff, spectral”.

Stacks 0901. For a spectral space X, the constructible topology on X is Hausdorff, totally disconnected and quasi-compact.

theorem withConstructibleTopology_t2_totallyDisconnected_compact (X : Type*) [TopologicalSpace X]
  [SpectralSpace X] :
    T2Space (WithConstructibleTopology X) ∧
      TotallyDisconnectedSpace (WithConstructibleTopology X) ∧
        CompactSpace (WithConstructibleTopology X)

Tag 0A2S, a lemma

Tag 0A2S in the Stacks Project.

spectralMap_continuous_withConstructibleTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/SpectralMaps.lean, line 667. The attribute's comment: “continuity in the constructible topology”. References: EGA IV (1.9.14), “iii, special case”.

Stacks 0A2S (continuity in the constructible topology). A spectral map f : X → Y is continuous for the constructible topologies on X and Y.

theorem spectralMap_continuous_withConstructibleTopology
    (f : X → Y) (hf : IsSpectralMap f) :
    Continuous
      (fun x : WithConstructibleTopologyTypeSynonym X =>
        WithConstructibleTopologyTypeSynonym.of (f (WithConstructibleTopologyTypeSynonym.out
            x)))

spectralMap_fibre_isCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/SpectralMaps.lean, line 685. The attribute's comment: “quasi-compact fibres”.

Stacks 0A2S (quasi-compact fibres). The fibres of a spectral map between spectral spaces are quasi-compact.

theorem spectralMap_fibre_isCompact
    (f : X → Y) (hf : IsSpectralMap f) (y : Y) :
    IsCompact (f ⁻¹' {y})

spectralMap_range_isClosed_withConstructibleTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/SpectralMaps.lean, line 703. The attribute's comment: “closed image in the constructible topology”. References: EGA IV (1.9.14), “iv, special case”.

Stacks 0A2S (closed image in the constructible topology). The image of a spectral map between spectral spaces is closed in the constructible topology on the target.

theorem spectralMap_range_isClosed_withConstructibleTopology
    (f : X → Y) (hf : IsSpectralMap f) :
    IsClosed (Set.range (fun x => WithConstructibleTopologyTypeSynonym.of (f x)))

Tag 0G1J, a lemma

Tag 0G1J in the Stacks Project.

TopologicalSpace.isSpectralMap_iff_continuous_constructibleTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/SpectralMapConstructible.lean, line 108. References: EGA IV (1.9.14), “(iii)”.

Stacks 0G1J. Let X and Y be spectral spaces and let f : X → Y be continuous. Then f is a spectral map if and only if it is continuous for the constructible topologies on X and Y.

theorem isSpectralMap_iff_continuous_constructibleTopology
    [SpectralSpace X] [SpectralSpace Y] (f : X → Y) (hf : Continuous f) :
    IsSpectralMap f ↔ Continuous[constructibleTopology X, constructibleTopology Y] f

Tag 0902, a lemma

Tag 0902 in the Stacks Project.

spectralSpace_of_isClosed_constructibleTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/ConstructiblyClosed.lean, line 286. References: SGA 4 IV (9.1.11), “partial”.

Stacks 0902. For a spectral space X and a subset E ⊆ X closed in the constructible topology on X, the set E with the subspace topology inherited from X is a spectral space.

theorem spectralSpace_of_isClosed_constructibleTopology
    {X : Type*} [TopologicalSpace X] [SpectralSpace X]
    (E : Set X)
    (hE : @IsClosed X (constructibleTopology X) E) :
    SpectralSpace E

Tag 0903, a lemma

Tag 0903 in the Stacks Project.

specializes_and_isClosed_and_isOpen_of_constructible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/ConstructiblyClosedStable.lean, line 162.

Stacks 0903. For a spectral space X: a point of the closure of a constructibly closed set is a specialization of a point of that set; a constructibly closed set stable under specialization is closed; and a constructibly open set stable under generalization is open.

theorem specializes_and_isClosed_and_isOpen_of_constructible [SpectralSpace X] :
    (∀ {E : Set X}, IsClosed[constructibleTopology X] E →
        ∀ {x : X}, x ∈ closure E → ∃ y ∈ E, y ⤳ x) ∧
      (∀ {E : Set X}, IsClosed[constructibleTopology X] E →
        StableUnderSpecialization E → IsClosed E) ∧
      (∀ {E' : Set X}, IsOpen[constructibleTopology X] E' →
        StableUnderGeneralization E' → IsOpen E')

Tag 0904, a lemma

Tag 0904 in the Stacks Project.

Topology.exists_specializes_or_exists_disjoint_nhds, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/Generization.lean, line 82.

Stacks 0904. For any two points x, y of a spectral space, either there is a point z specializing to both (equivalently, x and y both lie in closure {z}), or x and y have disjoint open neighbourhoods.

theorem exists_specializes_or_exists_disjoint_nhds [SpectralSpace X] (x y : X) :
    (∃ z : X, z ⤳ x ∧ z ⤳ y) ∨
      ∃ U V : Set X, IsOpen U ∧ IsOpen V ∧ x ∈ U ∧ y ∈ V ∧ Disjoint U V

Tag 0905, a lemma

Tag 0905 in the Stacks Project.

spectralSpace_profinite_of_t2, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/ProfiniteCharacterization.lean, line 219.

Stacks 0905. A Hausdorff spectral space is profinite: it is both Hausdorff and totally disconnected (quasi-compactness is automatic from SpectralSpace).

theorem spectralSpace_profinite_of_t2 [SpectralSpace X] [T2Space X] :
    T2Space X ∧ TotallyDisconnectedSpace X

Tag 0906, a lemma

Tag 0906 in the Stacks Project.

connectedComponents_isProfinite, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/ComponentSpace.lean, line 286.

Stacks 0906. For a spectral space X the space of connected components π₀(X) = ConnectedComponents X is profinite: Hausdorff, quasi-compact and totally disconnected.

theorem connectedComponents_isProfinite
    (X : Type*) [TopologicalSpace X] [SpectralSpace X] :
    T2Space (ConnectedComponents X) ∧
    CompactSpace (ConnectedComponents X) ∧
    TotallyDisconnectedSpace (ConnectedComponents X)

Tag 0907, a lemma

Tag 0907 in the Stacks Project.

prod_spectralSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/Products.lean, line 165.

The product of two spectral spaces is a spectral space.

theorem prod_spectralSpace (X Y : Type*)
    [TopologicalSpace X] [TopologicalSpace Y]
    [SpectralSpace X] [SpectralSpace Y] :
    SpectralSpace (X × Y)

Tag 09XU, a lemma

Tag 09XU in the Stacks Project.

Topology.isHomeomorph_of_isSpectralMap_of_bijective, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/BijectionHomeomorph.lean, line 223.

Stacks 09XU. Let f : X → Y be a spectral, bijective map of spectral topological spaces. If generalizations or specializations lift along f, then f is a homeomorphism.

theorem isHomeomorph_of_isSpectralMap_of_bijective [SpectralSpace X] [SpectralSpace Y]
    {f : X → Y} (hspec : IsSpectralMap f) (hbij : Function.Bijective f)
    (hlift : GeneralizingMap f ∨ SpecializingMap f) : IsHomeomorph f

Tag 09XV, a lemma

Tag 09XV in the Stacks Project.

spectralSpace_inverseLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/InverseLimitFiniteSober.lean, line 181.

Stacks 09XV. The inverse limit of a directed inverse system of finite sober topological spaces is a spectral topological space. Here a sober space in the sense of the Stacks project is a space that is both T0Space and QuasiSober.

theorem spectralSpace_inverseLimit [Nonempty I] [IsDirectedOrder I] [∀ i, Finite (X i)]
    [∀ i, T0Space (X i)] [∀ i, QuasiSober (X i)]
    (hf : ∀ ⦃i j : I⦄ (h : i ≤ j), Continuous (f h)) :
    SpectralSpace (inverseLimit f)

Tag 09XW, a lemma

Tag 09XW in the Stacks Project.

Topology.spectralSpace_iff_exists_isClosed_withConstructibleTopology, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/SierpinskiEmbedding.lean, line 577.

A topological space is spectral if and only if it is homeomorphic to a subset of a product of copies of the Sierpinski space which is closed for the constructible topology of that product.

theorem spectralSpace_iff_exists_isClosed_withConstructibleTopology (X : Type u)
    [TopologicalSpace X] :
    SpectralSpace X ↔
      ∃ (I : Type u) (S : Set (SierpinskiProduct I)),
        IsClosed[constructibleTopology (SierpinskiProduct I)] S ∧ Nonempty (X ≃ₜ S)

Tag 09XX, a lemma

Tag 09XX in the Stacks Project.

spectralSpace_iff_isDirectedInverseLimitOfFiniteSober, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/AsDirectedInverseLimit.lean, line 175.

A topological space is spectral if and only if it is a directed inverse limit of finite sober topological spaces.

theorem spectralSpace_iff_isDirectedInverseLimitOfFiniteSober
    (X : Type u) [TopologicalSpace X] :
    SpectralSpace X ↔ IsDirectedInverseLimitOfFiniteSober X

Tag 0A2T, a lemma

Tag 0A2T in the Stacks Project.

UniversalSoberMap.compactSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/UniversalSoberMap.lean, line 291. The attribute's comment: “part (1): quasi-compactness”.

Statement (1). If X is quasi-compact, then so is X'. This is the first part of Stacks Project Lemma 5.23.15 (tag 0A2T).

theorem UniversalSoberMap.compactSpace
    {X X' : Type*} [TopologicalSpace X] [TopologicalSpace X']
    (c : UniversalSoberMap X X') [CompactSpace X] :
    CompactSpace X'

UniversalSoberMap.spectralSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/UniversalSoberMap.lean, line 385. The attribute's comment: “part (2): spectral”.

Statement (2). If X is quasi-compact, has a basis of quasi-compact opens, and the intersection of any two quasi-compact opens of X is quasi-compact, then X' is a spectral topological space. This is the second part of Stacks Project Lemma 5.23.15 (tag 0A2T).

theorem UniversalSoberMap.spectralSpace
    {X X' : Type*} [TopologicalSpace X] [TopologicalSpace X']
    (c : UniversalSoberMap X X')
    [CompactSpace X] [PrespectralSpace X] [QuasiSeparatedSpace X] :
    SpectralSpace X'

UniversalSoberMap.noetherianSpectralSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/UniversalSoberMap.lean, line 415. The attribute's comment: “part (3): Noetherian spectral”.

Statement (3). If X is Noetherian, then X' is a Noetherian spectral space. This is the third part of Stacks Project Lemma 5.23.15 (tag 0A2T).

theorem UniversalSoberMap.noetherianSpectralSpace
    {X X' : Type*} [TopologicalSpace X] [TopologicalSpace X']
    (c : UniversalSoberMap X X') [NoetherianSpace X] :
    NoetherianSpace X' ∧ SpectralSpace X'

Sources

LeanwithConstructibleTopology_t2_totallyDisconnected_compact · spectralMap_continuous_withConstructibleTopology · spectralMap_fibre_isCompact · spectralMap_range_isClosed_withConstructibleTopology · TopologicalSpace.isSpectralMap_iff_continuous_constructibleTopology · spectralSpace_of_isClosed_constructibleTopology · specializes_and_isClosed_and_isOpen_of_constructible · Topology.exists_specializes_or_exists_disjoint_nhds

Section5.24 Limits of spectral spaces #

Section 5.24 of the Stacks Project, Tag 0A2U. 8 tags here are carried by 20 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0A2V, a lemma

Tag 0A2V in the Stacks Project.

SpectralLimits.isCompact_limitSubset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/LimitQuasiCompact.lean, line 133. The attribute's comment: “part (1)”.

Stacks 0A2V (1). For a diagram of spectral spaces along spectral maps and subsets Z j ⊆ F.obj j closed in the constructible topology, the subset {x ∈ lim F | ∀ j, π j x ∈ Z j} of the limit is quasi-compact for the limit topology.

theorem isCompact_limitSubset
    (hF : ∀ {j i : J} (a : j ⟶ i), IsSpectralMap (F.map a).hom) (Z : ∀ j, Set (F.obj j))
    (hZ_closed : ∀ j, @IsClosed _ (constructibleTopology (F.obj j)) (Z j)) :
    IsCompact (limitSubset F Z)

SpectralLimits.compactSpace_limit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/LimitQuasiCompact.lean, line 173. The attribute's comment: “part (2)”.

Stacks 0A2V (2). The limit of a diagram of spectral spaces along spectral maps is quasi-compact. This is part (1) with Z j = univ.

theorem compactSpace_limit (hF : ∀ {j i : J} (a : j ⟶ i), IsSpectralMap (F.map a).hom) :
    CompactSpace ((limit F : TopCat.{max v u}))

Tag 0A2W, a lemma

Tag 0A2W in the Stacks Project.

SpectralLimits.nonempty_limitSet_inter_of_isClosed_constructible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/LimitNonempty.lean, line 135. The attribute's comment: “part (1)”.

A compatible cofiltered system of nonempty constructibly closed subsets of a spectral diagram has nonempty limit.

theorem nonempty_limitSet_inter_of_isClosed_constructible [IsCofiltered I]
    (Z : ∀ i, Set (F.obj i)) (hZ_ne : ∀ i, (Z i).Nonempty)
    (hZ_cl : ∀ i, @IsClosed (F.obj i) (constructibleTopology (F.obj i)) (Z i))
    (hZ_comp : ∀ ⦃j i : I⦄ (a : j ⟶ i), F.map a '' Z j ⊆ Z i) :
    { x : ∀ i, F.obj i | x ∈ limitSet F ∧ ∀ i, x i ∈ Z i }.Nonempty

SpectralLimits.nonempty_limitSet, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/LimitNonempty.lean, line 168. The attribute's comment: “part (2)”.

The cofiltered limit of a diagram of nonempty spectral spaces is nonempty.

theorem nonempty_limitSet [IsCofiltered I] (hX_ne : ∀ i, Nonempty (F.obj i)) :
    (limitSet F).Nonempty

Tag 0A2X, a lemma

Tag 0A2X in the Stacks Project.

SpectralLimits.preimage_limit_π_subset_iff_exists_map_preimage_subset, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/LimitConstructible.lean, line 250.

Let J be a small cofiltered category and let F : J ⥤ TopCat be a diagram of spectral spaces such that, for every morphism a : j ⟶ i in J, the underlying map F.map a : F.obj j → F.obj i is a spectral map. Let X := limit F with projections π_i := limit.π F i : X → F.obj i. For every object i : J and any subsets E, G ⊂ F.obj i where E is closed in the constructible topology and G is open in the constructible topology, we have π_i ⁻¹' E ⊆ π_i ⁻¹' G ↔ ∃ (j : J) (a : j ⟶ i), (F.map a) ⁻¹' E ⊆ (F.map a) ⁻¹' G.

theorem preimage_limit_π_subset_iff_exists_map_preimage_subset
    {J : Type u} [SmallCategory J] [IsCofiltered J]
    (F : J ⥤ TopCat.{u})
    (hF_spec : ∀ j, SpectralSpace (F.obj j))
    (hF_map : ∀ {i j : J} (a : j ⟶ i), IsSpectralMap (F.map a))
    (i : J) (E G : Set (F.obj i))
    (hE : @IsClosed _ (constructibleTopology (F.obj i)) E)
    (hG : @IsOpen _ (constructibleTopology (F.obj i)) G) :
    ((limit.π F i) ⁻¹' E ⊆ (limit.π F i) ⁻¹' G) ↔
      (∃ (j : J) (a : j ⟶ i), (F.map a) ⁻¹' E ⊆ (F.map a) ⁻¹' G)

Tag 0A2Y, a lemma

Tag 0A2Y in the Stacks Project.

descend_isConstructible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/DescentConstructible.lean, line 108. References: EGA IV (8.3.11), “partial”.

For a cofiltered diagram D of spectral spaces with spectral transition maps, every constructible subset E of the inverse limit D.invLimit is the preimage under some projection D.projFun i of a constructible subset of D.F.obj i.

theorem descend_isConstructible
    {E : Set D.invLimit} (hE : IsConstructible E) :
    ∃ (i : J) (E_i : Set (D.F.obj i)), IsConstructible E_i ∧ D.projFun i ⁻¹' E_i = E

descend_isConstructible_isOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/DescentConstructible.lean, line 168. The attribute's comment: “open refinement”. References: EGA IV (8.3.12), “open case”; EGA IV (8.3.11), “partial”.

If the constructible subset of the inverse limit is moreover open, the constructible subset it descends from on the factor can be chosen open.

theorem descend_isConstructible_isOpen
    {E : Set D.invLimit} (hE : IsConstructible E) (hEopen : IsOpen E) :
    ∃ (i : J) (E_i : Set (D.F.obj i)),
      IsConstructible E_i ∧ IsOpen E_i ∧ D.projFun i ⁻¹' E_i = E

descend_isConstructible_isClosed, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/DescentConstructible.lean, line 179. The attribute's comment: “closed refinement”. References: EGA IV (8.3.12), “resp. closed case”; EGA IV (8.3.11), “partial”.

If the constructible subset of the inverse limit is moreover closed, the constructible subset it descends from on the factor can be chosen closed.

theorem descend_isConstructible_isClosed
    {E : Set D.invLimit} (hE : IsConstructible E) (hEcl : IsClosed E) :
    ∃ (i : J) (E_i : Set (D.F.obj i)),
      IsConstructible E_i ∧ IsClosed E_i ∧ D.projFun i ⁻¹' E_i = E

Tag 0A2Z, a lemma

Tag 0A2Z in the Stacks Project.

spectralDiagram_invLimit_spectralSpace, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/InverseLimits.lean, line 542. The attribute's comment: “inverse limit is spectral”.

Stacks 0A2Z (inverse limit is spectral). The inverse limit of a cofiltered diagram of spectral spaces with spectral transition maps is a spectral topological space.

theorem spectralDiagram_invLimit_spectralSpace
    {J : Type v} [Category.{v'} J] [IsCofiltered J] (D : SpectralDiagram.{v, u} J) :
    SpectralSpace D.invLimit

spectralDiagram_proj_isSpectralMap, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/InverseLimits.lean, line 551. The attribute's comment: “projections are spectral”.

Stacks 0A2Z (projections are spectral). Each projection from the inverse limit of a cofiltered diagram of spectral spaces to a component of the diagram is a spectral map.

theorem spectralDiagram_proj_isSpectralMap
    {J : Type v} [Category.{v'} J] [IsCofiltered J] (D : SpectralDiagram.{v, u} J) (j : J) :
    IsSpectralMap (D.projFun j)

Tag 0A30, a lemma

Tag 0A30 in the Stacks Project.

SpectralLimits.descent_of_quasiCompact_opens, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/LimitOpenDescent.lean, line 179. The attribute's comment: “part (1): descent of quasi-compact opens”.

For every quasi-compact open U of the limit lim F, there exist an index i and a quasi-compact open Ui of F.obj i whose preimage under the projection equals U.

theorem descent_of_quasiCompact_opens
    [∀ i, SpectralSpace (F.obj i)]
    (hF : ∀ ⦃i j : J⦄ (a : i ⟶ j), IsSpectralMap (F.map a))
    (U : Set ((limit F : TopCat))) (hUopen : IsOpen U) (hUcpt : IsCompact U) :
    ∃ (i : J) (Ui : Set (F.obj i)), IsOpen Ui ∧ IsCompact Ui ∧
      (limit.π F i) ⁻¹' Ui = U

SpectralLimits.descent_of_inclusions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/LimitOpenDescent.lean, line 325. The attribute's comment: “part (2): descent of inclusions”.

If two quasi-compact opens Ui ⊆ F.obj i and Uj ⊆ F.obj j have nested preimages in the limit, the inclusion already holds after pulling back along a span a : k ⟶ i, b : k ⟶ j.

theorem descent_of_inclusions
    [∀ i, SpectralSpace (F.obj i)]
    (hF : ∀ ⦃i j : J⦄ (a : i ⟶ j), IsSpectralMap (F.map a))
    (i j : J) (Ui : Set (F.obj i)) (Uj : Set (F.obj j))
    (hUi_open : IsOpen Ui) (hUi_cpt : IsCompact Ui)
    (hUj_open : IsOpen Uj) (hUj_cpt : IsCompact Uj)
    (h : (limit.π F i) ⁻¹' Ui ⊆ (limit.π F j) ⁻¹' Uj) :
    ∃ (k : J) (a : k ⟶ i) (b : k ⟶ j),
      (F.map a) ⁻¹' Ui ⊆ (F.map b) ⁻¹' Uj

SpectralLimits.descent_of_finite_unions, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/LimitOpenDescent.lean, line 387. The attribute's comment: “part (3): descent of finite unions”.

If, in the limit, the preimage of a quasi-compact open Ui equals the union of the preimages of finitely many quasi-compact opens U s (s : Fin n), then this equality already holds after pulling back along some j ⟶ i.

theorem descent_of_finite_unions
    [∀ i, SpectralSpace (F.obj i)]
    (hF : ∀ ⦃i j : J⦄ (a : i ⟶ j), IsSpectralMap (F.map a))
    (i : J) (n : ℕ) (Ui : Set (F.obj i)) (U : Fin n → Set (F.obj i))
    (hUi_open : IsOpen Ui) (hUi_cpt : IsCompact Ui)
    (hU : ∀ s, IsOpen (U s) ∧ IsCompact (U s))
    (h : (limit.π F i) ⁻¹' Ui = ⋃ s, (limit.π F i) ⁻¹' (U s)) :
    ∃ (j : J) (a : j ⟶ i),
      (F.map a) ⁻¹' Ui = ⋃ s, (F.map a) ⁻¹' (U s)

SpectralLimits.descent_of_finite_intersections, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/LimitOpenDescent.lean, line 420. The attribute's comment: “part (4): descent of finite intersections”.

If, in the limit, the preimage of a quasi-compact open Ui equals the intersection of the preimages of finitely many quasi-compact opens U s (s : Fin n), then this equality already holds after pulling back along some j ⟶ i.

theorem descent_of_finite_intersections
    [∀ i, SpectralSpace (F.obj i)]
    (hF : ∀ ⦃i j : J⦄ (a : i ⟶ j), IsSpectralMap (F.map a))
    (i : J) (n : ℕ) (Ui : Set (F.obj i)) (U : Fin n → Set (F.obj i))
    (hUi_open : IsOpen Ui) (hUi_cpt : IsCompact Ui)
    (hU : ∀ s, IsOpen (U s) ∧ IsCompact (U s))
    (h : (limit.π F i) ⁻¹' Ui = ⋂ s, (limit.π F i) ⁻¹' (U s)) :
    ∃ (j : J) (a : j ⟶ i),
      (F.map a) ⁻¹' Ui = ⋂ s, (F.map a) ⁻¹' (U s)

Tag 0A31, a lemma

Tag 0A31 in the Stacks Project.

SpectralSubset.characterizations_equiv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/QuasiCompactOpenInter.lean, line 282. The attribute's comment: “equivalence of the five characterizations”.

Stacks 0A31, the equivalence. For a subset W of a spectral space the five conditions (1) intersection of constructibles and stable under generalization, (2) quasi-compact and stable under generalization, (3) the generalizations of a quasi-compact set, (4) an intersection of quasi-compact opens, (5) a directed intersection of quasi-compact opens, are all equivalent.

theorem characterizations_equiv [SpectralSpace X] (W : Set X) :
    (IsStableInterConstructible W ↔ IsStableCompact W) ∧
      (IsStableCompact W ↔ IsGeneralizationsOfCompact W) ∧
        (IsGeneralizationsOfCompact W ↔ IsInterCompactOpen W) ∧
          (IsInterCompactOpen W ↔ IsDirectedInterCompactOpen W)

SpectralSubset.spectralSpace_of_isStableCompact, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/QuasiCompactOpenInter.lean, line 301. The attribute's comment: “conclusion (a): W is spectral”.

Conclusion (a): under the equivalent conditions, W (with the subspace topology) is itself a spectral space.

theorem spectralSpace_of_isStableCompact [SpectralSpace X] (W : Set X) (h : IsStableCompact W) :
    SpectralSpace W

SpectralSubset.exists_homeomorph_invLimit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/QuasiCompactOpenInter.lean, line 358. The attribute's comment: “conclusion (b): W ≅ lim U_i”.

Conclusion (b): the canonical map W → InvLimit U is a homeomorphism.

theorem exists_homeomorph_invLimit
    {I : Type*} [Nonempty I] (U : I → Set X)
    (hdir : ∀ i j, ∃ k, U k ⊆ U i ∩ U j)
    (W : Set X) (hWeq : W = ⋂ i, U i) :
    ∃ φ : W ≃ₜ InvLimit U,
      ∀ w : W, ∀ i, ((φ w).1 i : X) = (w : X)

SpectralSubset.exists_subset_of_subset_isOpen, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/QuasiCompactOpenInter.lean, line 396. The attribute's comment: “conclusion (c): some U_i ⊆ V”.

Conclusion (c): with the family U_i from condition (5), every open subset V of X containing W contains some U_i.

theorem exists_subset_of_subset_isOpen [SpectralSpace X]
    {I : Type*} [Nonempty I] (U : I → Set X)
    (hU : ∀ i, IsOpen (U i) ∧ IsCompact (U i))
    (hdir : ∀ i j, ∃ k, U k ⊆ U i ∩ U j)
    (W : Set X) (hWeq : W = ⋂ i, U i)
    (V : Set X) (hVopen : IsOpen V) (hWV : W ⊆ V) :
    ∃ i, U i ⊆ V

Tag 0AP0, a lemma

Tag 0AP0 in the Stacks Project.

isLimit_diffLimitCone, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/LimitGeneralizations.lean, line 350.

Stacks 0AP0. For a spectral space X, a monotone family U indexed by a nonempty codirected order and specGen E = ⋂ i, U i, the cone diffLimitCone with apex specGen E \ E is a limit cone of the diagram (U i \ E)_i: the canonical map specGen E \ E ⟶ lim_i (U i \ E) is a homeomorphism.

theorem isLimit_diffLimitCone [SpectralSpace X] [Nonempty I] [IsCodirectedOrder I]
    {E : Set X}
    (hmono : ∀ ⦃i j : I⦄, i ≤ j → U i ⊆ U j)
    (hWeq : specGen E = ⋂ i, U i) :
    Nonempty (IsLimit (diffLimitCone U E hmono (fun i => hWeq ▸ Set.iInter_subset U i)))

isSpectral_specGen_diff_constructible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Spectral/LimitGeneralizations.lean, line 364.

Stacks 0AP0. If X is a spectral space and E ⊆ X is a constructible subset, then the set specGen E \ E of points specializing into E but not lying in E, equipped with the subspace topology, is a spectral space.

theorem isSpectral_specGen_diff_constructible [SpectralSpace X] {E : Set X}
    (hE : Topology.IsConstructible E) : SpectralSpace ↥(specGen E \ E)

Sources

LeanSpectralLimits.isCompact_limitSubset · SpectralLimits.compactSpace_limit · SpectralLimits.nonempty_limitSet_inter_of_isClosed_constructible · SpectralLimits.nonempty_limitSet · SpectralLimits.preimage_limit_π_subset_iff_exists_map_preimage_subset · descend_isConstructible · descend_isConstructible_isOpen · descend_isConstructible_isClosed

Section5.25 Stone-Čech compactification #

Section 5.25 of the Stacks Project, Tag 0908. 2 tags here are carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0909, a lemma

Tag 0909 in the Stacks Project.

mk_le_mk_set_set_of_denseRange, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Compactification/CardinalityBound.lean, line 106.

Stacks 0909. If f : X → Y is a continuous map of topological spaces with dense image and Y is Hausdorff, then #Y ≤ #P(P(X)).

theorem mk_le_mk_set_set_of_denseRange
    {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y]
    (f : X → Y) (hf : Continuous f) (hd : DenseRange f) :
    Cardinal.mk Y ≤ Cardinal.mk (Set (Set X))

Tag 090A, a lemma

Tag 090A in the Stacks Project.

exists_compactification_and_isOpenEmbedding_stoneCechUnit, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Compactification/OnePoint.lean, line 220.

Stacks 090A. For a Hausdorff, locally quasi-compact space X: (1) there exists a compact Hausdorff space X* and an open embedding f : X → X* whose range has singleton complement, and (2) the canonical map X → StoneCech X is also an open embedding.

theorem exists_compactification_and_isOpenEmbedding_stoneCechUnit [WeaklyLocallyCompactSpace X]
  [T2Space X] :
    (∃ (Xstar : Type u) (_ : TopologicalSpace Xstar)
      (_ : CompactSpace Xstar) (_ : T2Space Xstar)
      (f : X → Xstar) (p : Xstar),
        IsOpenEmbedding f ∧ (range f)ᶜ = {p}) ∧
    IsOpenEmbedding (stoneCechUnit : X → StoneCech X)

Sources

Leanmk_le_mk_set_set_of_denseRange · exists_compactification_and_isOpenEmbedding_stoneCechUnit

Section5.26 Extremally disconnected spaces #

Section 5.26 of the Stacks Project, Tag 08YH. 10 tags here are carried by 7 declarations of the repository (all in StacksFrontier) and 6 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 08YI, a definition

Tag 08YI in the Stacks Project.

Declarations registered for the tag:

ExtremallyDisconnected registered with add_to_stacks in StacksCore/Topology/ExtremallyDisconnected/Defs.lean, line 20 (StacksCore): “extremally disconnected spaces”.
ExtremallyDisconnected.open_closure registered with add_to_stacks in StacksCore/Topology/ExtremallyDisconnected/Defs.lean, line 21 (StacksCore): “the closure of every open subset is open”.

Tag 08YJ, a lemma

Tag 08YJ in the Stacks Project.

Declarations registered for the tag:

image_subset_closure_compl_image_compl_of_isOpen registered with add_to_stacks in StacksCore/Topology/ExtremallyDisconnected/OpenImage.lean, line 21 (StacksCore): “images of opens under a map that is onto no proper closed subset”.

Tag 08YK, a lemma

Tag 08YK in the Stacks Project.

Declarations registered for the tag:

ExtremallyDisconnected.disjoint_closure_of_disjoint_isOpen registered with add_to_stacks in StacksCore/Topology/ExtremallyDisconnected/DisjointClosures.lean, line 19 (StacksCore): “disjoint open subsets of an extremally disconnected space have disjoint closures”.

Tag 08YL, a lemma

Tag 08YL in the Stacks Project.

Declarations registered for the tag:

ExtremallyDisconnected.homeoCompactToT2 registered with add_to_stacks in StacksCore/Topology/ExtremallyDisconnected/Surjection.lean, line 20 (StacksCore).

Tag 08YM, a lemma

Tag 08YM in the Stacks Project.

Declarations registered for the tag:

exists_compact_surjective_zorn_subset registered with add_to_stacks in StacksCore/Topology/ExtremallyDisconnected/MinimalSubset.lean, line 24 (StacksCore): “a minimal quasi-compact subset that still surjects”.

Tag 08YN, a proposition

Tag 08YN in the Stacks Project.

extremallyDisconnected_tfae, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/ExtremallyDisconnected/Characterization.lean, line 70.

For a quasi-compact Hausdorff space X the following are equivalent: X is extremally disconnected; every continuous surjection onto X from a quasi-compact Hausdorff space has a continuous section; X is projective among quasi-compact Hausdorff spaces, which is Mathlib's CompactT2.Projective.

theorem extremallyDisconnected_tfae (X : Type u) [TopologicalSpace X] [CompactSpace X] [T2Space X] :
    List.TFAE
      [ ExtremallyDisconnected X,
        HasContinuousSectionFromCompactT2 X,
        CompactT2.Projective X ]

Tag 090B, a lemma

Tag 090B in the Stacks Project.

rainwater_lemma, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/ExtremallyDisconnected/Rainwater.lean, line 49.

Stacks 090B (Rainwater's lemma). Let f : X → X be a surjective continuous selfmap of a Hausdorff topological space. If f is not id_X, then there exists a proper closed subset E ⊂ X such that X = E ∪ f(E).

theorem rainwater_lemma
    {X : Type*} [TopologicalSpace X] [T2Space X]
    (f : X → X) (hf_cont : Continuous f) (hf_surj : Function.Surjective f)
    (hf_ne_id : f ≠ id) :
    ∃ E : Set X, IsClosed E ∧ E ≠ Set.univ ∧ Set.univ = E ∪ f '' E

Tag 090C, an example

Tag 090C in the Stacks Project.

stoneCech_extremallyDisconnected_of_discrete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/ExtremallyDisconnected/StoneCech.lean, line 59.

Stacks 090C. The Stone–Čech compactification of a discrete topological space is extremally disconnected.

theorem stoneCech_extremallyDisconnected_of_discrete
    (X : Type*) [TopologicalSpace X] [DiscreteTopology X] :
    ExtremallyDisconnected (StoneCech X)

stoneCech_totallyDisconnected_of_discrete, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/ExtremallyDisconnected/StoneCech.lean, line 67.

Stacks 090C. The Stone–Čech compactification of a discrete topological space is totally disconnected.

theorem stoneCech_totallyDisconnected_of_discrete
    (X : Type*) [TopologicalSpace X] [DiscreteTopology X] :
    TotallyDisconnectedSpace (StoneCech X)

Tag 090D, a lemma

Tag 090D in the Stacks Project.

exists_extremallyDisconnected_cover, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/ExtremallyDisconnected/Cover.lean, line 87.

Stacks 090D, existence half. Every compact Hausdorff space X admits a continuous surjection from a compact Hausdorff extremally disconnected space.

theorem exists_extremallyDisconnected_cover
    (X : Type u) [TopologicalSpace X] [CompactSpace X] [T2Space X] :
    ∃ (X' : Type u) (_ : TopologicalSpace X') (_ : CompactSpace X')
        (_ : T2Space X') (_ : ExtremallyDisconnected X')
        (π : X' → X), Continuous π ∧ Function.Surjective π

minimal_cover_unique, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/ExtremallyDisconnected/Cover.lean, line 107.

Stacks 090D, uniqueness half. If π' : X' → X and π'' : X'' → X are two minimal extremally disconnected covers of a compact Hausdorff space X, then there is a homeomorphism X' ≃ₜ X'' lying over X.

Here "minimal" means: no proper closed subset surjects onto X.

theorem minimal_cover_unique
    {X X' X'' : Type u}
    [TopologicalSpace X] [CompactSpace X] [T2Space X]
    [TopologicalSpace X'] [CompactSpace X'] [T2Space X'] [ExtremallyDisconnected X']
    [TopologicalSpace X''] [CompactSpace X''] [T2Space X''] [ExtremallyDisconnected X'']
    {π' : X' → X} (π'_cont : Continuous π') (π'_surj : Function.Surjective π')
    (π'_min : ∀ E : Set X', IsClosed E → E ≠ univ → π' '' E ≠ univ)
    {π'' : X'' → X} (π''_cont : Continuous π'') (π''_surj : Function.Surjective π'')
    (π''_min : ∀ E : Set X'', IsClosed E → E ≠ univ → π'' '' E ≠ univ) :
    ∃ φ : X' ≃ₜ X'', π'' ∘ φ = π'

Tag 090E, a remark

Tag 090E in the Stacks Project.

minimal_cover_card_le, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/ExtremallyDisconnected/CoverCardinality.lean, line 58.

Stacks 090E. Let X be a quasi-compact Hausdorff space and let π : X' → X be a minimal quasi-compact Hausdorff extremally disconnected cover of X, minimality meaning that no proper closed subset of X' surjects onto X. If #X ≤ κ then #X' ≤ 2 ^ (2 ^ κ).

The infiniteness hypothesis _hκ on κ is present only to match the source; it is not used.

theorem minimal_cover_card_le
    {X X' : Type u}
    [TopologicalSpace X] [CompactSpace X] [T2Space X]
    [TopologicalSpace X'] [CompactSpace X'] [T2Space X'] [ExtremallyDisconnected X']
    {π : X' → X} (π_surj : Function.Surjective π)
    (π_min : ∀ E : Set X', IsClosed E → E ≠ univ → π '' E ≠ univ)
    {κ : Cardinal.{u}} (_hκ : Cardinal.aleph0 ≤ κ) (hX : Cardinal.mk X ≤ κ) :
    Cardinal.mk X' ≤ (2 : Cardinal.{u}) ^ ((2 : Cardinal.{u}) ^ κ)

Sources

LeanExtremallyDisconnected · ExtremallyDisconnected.open_closure · image_subset_closure_compl_image_compl_of_isOpen · ExtremallyDisconnected.disjoint_closure_of_disjoint_isOpen · ExtremallyDisconnected.homeoCompactToT2 · exists_compact_surjective_zorn_subset · extremallyDisconnected_tfae · rainwater_lemma

Section5.27 Miscellany #

Section 5.27 of the Stacks Project, Tag 0067. 2 tags here are carried by 2 declarations of the repository (all in StacksFrontier), quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0069, a lemma

Tag 0069 in the Stacks Project.

locallyCompactSpace_and_isRetrocompact_and_hasCofinalCompactRefinements, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Bases/QuasiCompactOpens.lean, line 114. References: EGA 0 (9.1.6), “second conjunct”.

Stacks 0069. Under hypotheses (H1) and (H2), X is locally quasi-compact, every quasi-compact open of X is retrocompact, and every quasi-compact open of X has a cofinal system of finite open coverings by quasi-compact opens with quasi-compact pairwise intersections.

theorem locallyCompactSpace_and_isRetrocompact_and_hasCofinalCompactRefinements
    (h1 : PrespectralSpace X) (h2 : QuasiSeparatedSpace X) :
    LocallyCompactSpace X ∧
    (∀ {U : Set X}, IsOpen U → IsCompact U → IsRetrocompact U) ∧
    (∀ {U : Set X}, IsOpen U → IsCompact U → HasCofinalCompactRefinements U)

Tag 06RM, a definition

Tag 06RM in the Stacks Project.

IsIsolatedPoint, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Separation/IsolatedPoint.lean, line 20.

Stacks 06RM. A point x of a topological space X is isolated if {x} is open in X.

def IsIsolatedPoint {X : Type*} [TopologicalSpace X] (x : X) : Prop

Sources

LeanlocallyCompactSpace_and_isRetrocompact_and_hasCofinalCompactRefinements · IsIsolatedPoint

Section5.28 Partitions and stratifications #

Section 5.28 of the Stacks Project, Tag 09XY. 8 tags here are carried by 9 declarations of the repository (all in StacksFrontier) and 1 registered declaration, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 09XZ, a definition

Tag 09XZ in the Stacks Project.

IsTopologicalPartition, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Stratification/Partition.lean, line 63.

Stacks 09XZ. A topological partition of X is a set-theoretic partition of X all of whose parts are locally closed.

def IsTopologicalPartition (c : Set (Set X)) : Prop

local_Refines, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Stratification/Partition.lean, line 70.

Stacks 09XZ. A collection P of subsets of X refines a collection Q when every member of P is contained in some member of Q.

def local_Refines (P Q : Set (Set X)) : Prop

Tag 09Y0, a definition

Tag 09Y0 in the Stacks Project.

IsGoodStratification, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Stratification/Good.lean, line 66.

Stacks 09Y0. A good stratification of a topological space X, indexed by I, is a family of subsets S : I → Set X which forms a partition (the sets are pairwise disjoint, each nonempty, and their union covers X) and which satisfies the frontier condition: if S i ∩ closure (S j) ≠ ∅, then S i ⊆ closure (S j).

structure IsGoodStratification {X : Type*} [TopologicalSpace X] {I : Type*}
    (S : I → Set X) : Prop

Tag 09Y1, a definition

Tag 09Y1 in the Stacks Project.

Stratification, a structure in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Stratification/Defs.lean, line 56.

A stratification of a topological space X, indexed by a partially ordered type I, is an indexed family strata : I → Set X whose members are pairwise disjoint and cover X (a partition X = ∐_{i} X_i), and such that the closure of each stratum is contained in the union of the strata at lower or equal indices.

structure Stratification (X : Type*) [TopologicalSpace X]
    (I : Type*) [PartialOrder I]

Tag 0BDS, a definition

Tag 0BDS in the Stacks Project.

Declarations registered for the tag:

LocallyFinite registered with add_to_stacks in StacksCore/Topology/Stratification/LocallyFiniteFamily.lean, line 22 (StacksCore): “a locally finite collection of subsets”. References: EGA IV (3.1.6), “more general”; EGA IV (21.10.1), “partial”.

Tag 09Y2, a remark

Tag 09Y2 in the Stacks Project.

closedZ_of_locallyFiniteStratification, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Stratification/LocallyFinite.lean, line 156. The attribute's comment: “(1)”.

Stacks 09Y2 (1). Let X be a locally finite stratification of α with partial order ≤ on I, and for each i let Z i = ⋃ (j ≤ i) X j. Then each Z i is closed, and for all i, j one has Z i ∩ Z j = ⋃ (k ≤ i ∧ k ≤ j) Z k.

theorem closedZ_of_locallyFiniteStratification [PartialOrder I] {X : I → Set α}
    (h : IsLocallyFiniteStratification X)
    (Z : I → Set α) (hZ : ∀ i, Z i = ⋃ j ∈ {j | j ≤ i}, X j) :
    (∀ i, IsClosed (Z i)) ∧
    (∀ i j, Z i ∩ Z j = ⋃ k ∈ {k | k ≤ i ∧ k ≤ j}, Z k)

locallyFiniteStratification_of_closedZ, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Stratification/LocallyFinite.lean, line 229. The attribute's comment: “(2)”.

Stacks 09Y2 (2). Let I be a partially ordered set and {Z i} a family of closed subsets of α that cover α, are locally finite, and satisfy Z i ∩ Z j = ⋃ (k ≤ i ∧ k ≤ j) Z k. Then the sets X i = Z i \ ⋃ (j < i) Z j, with the partial order ≤ on I, form a locally finite stratification of α.

theorem locallyFiniteStratification_of_closedZ [PartialOrder I] {Z : I → Set α}
    (hclosed : ∀ i, IsClosed (Z i))
    (hcover : ⋃ i, Z i = Set.univ)
    (hlf : LocallyFinite Z)
    (hint : ∀ i j, Z i ∩ Z j = ⋃ k ∈ {k | k ≤ i ∧ k ≤ j}, Z k)
    (X : I → Set α) (hX : ∀ i, X i = Z i \ ⋃ j ∈ {j | j < i}, Z j) :
    IsLocallyFiniteStratification X

Tag 09Y3, a lemma

Tag 09Y3 in the Stacks Project.

exists_finite_stratification_refining_finite_partition, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Stratification/RefinePartition.lean, line 337.

Stacks 09Y3. Every finite partition of a topological space by locally closed subsets is refined by a finite stratification.

theorem exists_finite_stratification_refining_finite_partition
    {X : Type*} [TopologicalSpace X] {ι : Type*} [Finite ι] (P : TopPartition X ι) :
    ∃ (κ : Type) (_ : Finite κ) (_ : PartialOrder κ) (S : TopStratification X κ),
      S.toTopPartition.Refines P

Tag 09Y4, a lemma

Tag 09Y4 in the Stacks Project.

exists_finiteStratification_refining_constructible, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Stratification/RefineConstructible.lean, line 449.

Stacks 09Y4. If a topological space X is covered by a finite family T₁, …, Tₙ of constructible subsets, then there exists a finite stratification X = ⨆ Xᵢ such that each stratum is constructible and each Tₖ is a union of strata.

theorem exists_finiteStratification_refining_constructible
    {n : ℕ} (T : Fin n → Set X)
    (hT : ∀ k, Topology.IsConstructible (T k))
    (_hcover : ⋃ k, T k = Set.univ) :
    ∃ (𝒮 : FiniteStratification X),
      (∀ i, Topology.IsConstructible (𝒮.S i)) ∧
      (∀ k, ∃ I : Set 𝒮.ι, T k = ⋃ i ∈ I, 𝒮.S i)

Tag 09Y5, a lemma

Tag 09Y5 in the Stacks Project.

main_theorem09Y5, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Stratification/PartitionRefinement.lean, line 481.

Let X be a Noetherian topological space. Any finite partition of X can be refined by a finite good stratification of X.

theorem main_theorem09Y5 (X : Type u) [TopologicalSpace X]
    [TopologicalSpace.NoetherianSpace X]
    (P : TopPartitionOpenCover.{u, v} X) (hP : P.IsFinite) :
    ∃ P' : TopPartitionOpenCover.{u, u} X,
      P'.IsFinite ∧ P'.IsGood ∧ P'.Refines P

Sources

LeanIsTopologicalPartition · local_Refines · IsGoodStratification · Stratification · LocallyFinite · closedZ_of_locallyFiniteStratification · locallyFiniteStratification_of_closedZ · exists_finite_stratification_refining_finite_partition

Section5.29 Colimits of spaces #

Section 5.29 of the Stacks Project, Tag 0B1W. 1 tag here is carried by 2 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0B1X, a lemma

Tag 0B1X in the Stacks Project.

Declarations registered for the tag:

TopCat.topCat_hasColimits registered with add_to_stacks in StacksCore/Topology/Limits/Colimits.lean, line 21 (StacksCore): “the category of topological spaces has colimits”.
TopCat.forget_preservesColimits registered with add_to_stacks in StacksCore/Topology/Limits/Colimits.lean, line 22 (StacksCore): “the forgetful functor to sets commutes with colimits”.

Sources

LeanTopCat.topCat_hasColimits · TopCat.forget_preservesColimits

Section5.30 Topological groups, rings, modules #

Section 5.30 of the Stacks Project, Tag 0B1Y. 12 tags here are carried by 19 declarations of the repository (all in StacksFrontier) and 12 registered declarations, quoted below from AxiomMath/Stacks at commit 5ed82d14.

Tag 0B1Z, a definition

Tag 0B1Z in the Stacks Project.

Declarations registered for the tag:

IsTopologicalGroup registered with add_to_stacks in StacksFrontier/Topology/Algebra/Group.lean, line 13 (StacksFrontier): “a topological group”.
ContinuousMonoidHom registered with add_to_stacks in StacksFrontier/Topology/Algebra/Group.lean, line 14 (StacksFrontier): “a homomorphism of topological groups”.

Tag 0BMC, an example

Tag 0BMC in the Stacks Project.

mapTopology_nhds_hasBasis, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AutomorphismGroup.lean, line 152.

Stacks 0BMC. For every f : E → E, the family { U_S S f | S : Finset E } of sets of maps agreeing with f on a finite subset S is a basis of neighbourhoods of f in the product (equivalently, when E is discrete, the compact-open) topology.

theorem mapTopology_nhds_hasBasis (f : E → E) :
    (nhds f).HasBasis (fun _ : Finset E => True) (fun S => U_S S f)

continuous_action, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AutomorphismGroup.lean, line 161.

Stacks 0BMC. The action map Map(E, E) × E → E, (f, e) ↦ f e, is continuous when E carries the discrete topology and Map(E, E) = (E → E) carries the product (= compact-open) topology.

theorem continuous_action :
    Continuous (fun p : (E → E) × E => p.1 p.2)

continuous_iff_uncurry_continuous, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AutomorphismGroup.lean, line 169.

Stacks 0BMC. A map g : X → (E → E) is continuous if and only if the uncurried map X × E → E, (x, e) ↦ g x e, is continuous.

theorem continuous_iff_uncurry_continuous
    {X : Type*} [TopologicalSpace X] (g : X → (E → E)) :
    Continuous g ↔ Continuous (fun p : X × E => g p.1 p.2)

continuous_comp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AutomorphismGroup.lean, line 178.

Stacks 0BMC. Composition Map(E, E) × Map(E, E) → Map(E, E), (f, g) ↦ f ∘ g, is continuous.

theorem continuous_comp :
    Continuous (fun p : (E → E) × (E → E) => p.1 ∘ p.2)

continuous_perm_inv, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AutomorphismGroup.lean, line 198.

Stacks 0BMC. Inversion σ ↦ σ⁻¹ on Aut(E) = Equiv.Perm E is continuous.

theorem continuous_perm_inv :
    Continuous (fun σ : Equiv.Perm E => σ⁻¹)

isTopologicalGroup_aut, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/AutomorphismGroup.lean, line 206.

Stacks 0BMC. Aut(E) = Equiv.Perm E, with the subspace topology induced from Map(E, E), is a topological group.

theorem isTopologicalGroup_aut :
    IsTopologicalGroup (Equiv.Perm E)

Tag 0B20, a lemma

Tag 0B20 in the Stacks Project.

TopCat.hasLimits_grp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/GroupLimits.lean, line 46. The attribute's comment: “part (1): existence of limits”.

Stacks 0B20, part (1). The category of topological groups has all small limits. This is Mathlib's HasLimitsOfShape J (Grp C), obtained from the fact that Grp.forget TopCat creates limits.

theorem hasLimits_grp : HasLimits (Grp TopCat.{u})

TopCat.preservesLimits_grpForget, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/GroupLimits.lean, line 52. The attribute's comment: “part (a): commutes with forgetful to TopCat”.

Stacks 0B20, part (a). The forgetful functor from topological groups to topological spaces preserves all small limits; indeed Mathlib shows it creates them.

theorem preservesLimits_grpForget : PreservesLimits (Grp.forget TopCat.{u})

TopCat.preservesLimits_forgetGrp, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/GroupLimits.lean, line 58. The attribute's comment: “part (b): commutes with forgetful to Grp”.

Stacks 0B20, part (b). The forgetful functor from topological groups to groups preserves all small limits.

theorem preservesLimits_forgetGrp : PreservesLimits (forgetGrp.{u})

Tag 0BR1, a lemma

Tag 0BR1 in the Stacks Project.

Stacks.Chapter05.Tag_0BR1.tfae_profinite_group, a theorem in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/ProfiniteGroup.lean, line 86. References: SGA 1 V (5.1); SGA 4 IV (2.7.2), “more general”.

Stacks 0BR1. For a topological group G, the following are equivalent: G is profinite as a topological space; G is a limit of a diagram of finite discrete topological groups; G is a cofiltered limit of finite discrete topological groups.

theorem tfae_profinite_group (G : Type u) [Group G] [TopologicalSpace G]
    [IsTopologicalGroup G] :
    List.TFAE
      [ IsProfiniteTop G,
        IsLimitOfFiniteDiscreteGroups G,
        IsCofilteredLimitOfFiniteDiscreteGroups G ]

Tag 0BR2, a definition

Tag 0BR2 in the Stacks Project.

Declarations registered for the tag:

ProfiniteGrp registered with add_to_stacks in StacksFrontier/Topology/Algebra/ProfiniteGroupCharacterization.lean, line 16 (StacksFrontier): “a profinite group”. References: SGA 1 V (5.1); SGA 4 IV (2.7.2).
ProfiniteGrp.of registered with add_to_stacks in StacksFrontier/Topology/Algebra/ProfiniteGroupCharacterization.lean, line 19 (StacksFrontier): “the profinite group attached to a compact, Hausdorff, totally disconnected topological group”.

Tag 0B21, a lemma

Tag 0B21 in the Stacks Project.

TopGrp.forgetToGrpCat_preservesColimits, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/GroupColimits.lean, line 122. The attribute's comment: “commutation with the forgetful functor to groups”.

Stacks 0B21, second part. Colimits of topological groups commute with the forgetful functor to the category of groups: the forgetful functor is a left adjoint, hence preserves colimits.

instance forgetToGrpCat_preservesColimits : PreservesColimits forgetToGrpCat.{u}

TopGrp.hasColimits, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/GroupColimits.lean, line 221. The attribute's comment: “existence of colimits”.

Stacks 0B21, first part. The category of topological groups has colimits.

noncomputable instance hasColimits : HasColimits TopGrp.{u}

Tag 0B22, a definition

Tag 0B22 in the Stacks Project.

StacksTopologicalRing, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/Ring.lean, line 65. References: EGA 0 (3.1.4).

Stacks 0B22. A ring R equipped with a topology is a topological ring if addition \((x, y) \mapsto x + y\) and multiplication \((x, y) \mapsto x \cdot y\) are continuous as maps \(R \times R \to R\).

def StacksTopologicalRing (R : Type*) [Ring R] [TopologicalSpace R] : Prop

StacksTopologicalRingHom, a def in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/Ring.lean, line 73. References: EGA 0 (20.3.1), “Hom. cont(A,B)”; EGA 0 (3.1.4); SGA 3 VIIB (0.1.3).

Stacks 0B22. A bundled ring homomorphism f : R →+* S between topological rings is a homomorphism of topological rings if its underlying function is continuous.

def StacksTopologicalRingHom
    {R S : Type*} [Ring R] [Ring S] [TopologicalSpace R] [TopologicalSpace S]
    [IsTopologicalRing R] [IsTopologicalRing S]
    (f : R →+* S) : Prop

Tag 0B23, a lemma

Tag 0B23 in the Stacks Project.

TopCommRingCat.hasLimits, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/RingLimits.lean, line 85. The attribute's comment: “existence of limits”.

Stacks 0B23. The category of topological rings has all small limits.

instance hasLimits : HasLimits TopCommRingCat.{u}

TopCommRingCat.preservesLimits_forget₂TopCat, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/RingLimits.lean, line 95. The attribute's comment: “part (a): commutes with forgetful to TopCat”.

Stacks 0B23, part (a). The forgetful functor to topological spaces preserves all small limits: it carries TopCommRingCat.limitCone to TopCat.limitCone.

instance preservesLimits_forget₂TopCat :
    PreservesLimits (forget₂ TopCommRingCat.{u} TopCat.{u})

TopCommRingCat.preservesLimits_forget₂CommRingCat, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/RingLimits.lean, line 108. The attribute's comment: “part (b): commutes with forgetful to CommRing”.

Stacks 0B23, part (b). The forgetful functor to rings preserves all small limits: the image of TopCommRingCat.limitCone is the subring of sections of the underlying diagram of rings, which is a limit there for the same reason.

instance preservesLimits_forget₂CommRingCat :
    PreservesLimits (forget₂ TopCommRingCat.{u} CommRingCat.{u})

Tag 0B24, a lemma

Tag 0B24 in the Stacks Project.

TopCommRingCat.hasColimits, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/RingColimits.lean, line 167. The attribute's comment: “part (1): existence of colimits”.

Stacks 0B24, part (1). The category of topological rings has all small colimits.

noncomputable instance hasColimits : HasColimits TopCommRingCat.{u}

TopCommRingCat.preservesColimits_forget₂CommRingCat, an instance in StacksFrontier (drafted, not yet reviewed), declared in StacksFrontier/Topology/Algebra/RingColimits.lean, line 175. The attribute's comment: “part (2): commutes with forgetful to CommRing”.

Stacks 0B24, part (2). The forgetful functor from topological rings to rings preserves all small colimits, by the indiscrete-topology lift TopCommRingCat.indiscreteCocone.

noncomputable instance preservesColimits_forget₂CommRingCat :
    PreservesColimits (forget₂ TopCommRingCat.{u} CommRingCat.{u})

Tag 0B25, a definition

Tag 0B25 in the Stacks Project.

Declarations registered for the tag:

TopModuleCat registered with add_to_stacks in StacksFrontier/Topology/Algebra/Module.lean, line 52 (StacksFrontier): “(1), topological modules: the objects of this category are exactly the modules over a topological ring equipped with a topology making addition and scalar multiplication continuous. The IsTopologicalAddGroup field is no strengthening of the source: over a ring -x = (-1) • x, so continuity of negation follows from ContinuousSMul.”.
TopModuleCat.of registered with add_to_stacks in StacksFrontier/Topology/Algebra/Module.lean, line 57 (StacksFrontier): “(1), a topological module built from exactly the source's two conditions: of takes only [ContinuousAdd M] and [ContinuousSMul R M], deriving ContinuousNeg M from -x = (-1 : R) • x.”.
ContinuousLinearMap registered with add_to_stacks in StacksFrontier/Topology/Algebra/Module.lean, line 61 (StacksFrontier): “(2), homomorphisms of topological modules: an R-linear map bundled with a proof that its underlying function is continuous.”. References: EGA 0 (18.5.3), “partial”; EGA 0 (19.1.1); SGA 3 VIIB (0.2); SGA 3 VIIB (0.2.2); SGA 3 VIIB (0.3.6); SGA 3 VIIB (0.5.B); SGA 3 VIIB (1.3.5.A); SGA 6 II (AppII.3.0.2).

Tag 0B26, a lemma

Tag 0B26 in the Stacks Project.

Declarations registered for the tag:

TopModuleCat.instHasLimits registered with add_to_stacks in StacksFrontier/Topology/Algebra/ModuleLimits.lean, line 22 (StacksFrontier): “the category of topological modules has limits”.
TopModuleCat.isLimit registered with add_to_stacks in StacksFrontier/Topology/Algebra/ModuleLimits.lean, line 23 (StacksFrontier): “limits are computed on the underlying modules”.
TopModuleCat.instPreservesLimitsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier registered with add_to_stacks in StacksFrontier/Topology/Algebra/ModuleLimits.lean, line 24 (StacksFrontier): “the forgetful functor to topological spaces preserves limits”.

Tag 0B27, a lemma

Tag 0B27 in the Stacks Project.

Declarations registered for the tag:

TopModuleCat.instHasColimits registered with add_to_stacks in StacksFrontier/Topology/Algebra/ModuleColimits.lean, line 49 (StacksFrontier): “existence of colimits”.
TopModuleCat.isColimit registered with add_to_stacks in StacksFrontier/Topology/Algebra/ModuleColimits.lean, line 50 (StacksFrontier): “compatibility with the forgetful functor: a colimit cocone on the underlying R-modules, given the coinduced topology, is a colimit cocone of topological R-modules”.

Sources

LeanIsTopologicalGroup · ContinuousMonoidHom · mapTopology_nhds_hasBasis · continuous_action · continuous_iff_uncurry_continuous · continuous_comp · continuous_perm_inv · isTopologicalGroup_aut

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

5.23 Spectral spaces to 5.30 Topological groups, rings…

Section5.23 Spectral spaces#

Tag 0901, a lemma

Tag 0A2S, a lemma

Tag 0G1J, a lemma

Tag 0902, a lemma

Tag 0903, a lemma

Tag 0904, a lemma

Tag 0905, a lemma

Tag 0906, a lemma

Tag 0907, a lemma

Tag 09XU, a lemma

Tag 09XV, a lemma

Tag 09XW, a lemma

Tag 09XX, a lemma

Tag 0A2T, a lemma

Sources

Section5.24 Limits of spectral spaces#

Tag 0A2V, a lemma

Tag 0A2W, a lemma

Tag 0A2X, a lemma

Tag 0A2Y, a lemma

Tag 0A2Z, a lemma

Tag 0A30, a lemma

Tag 0A31, a lemma

Tag 0AP0, a lemma

Sources

Section5.25 Stone-Čech compactification#

Tag 0909, a lemma

Tag 090A, a lemma

Sources

Section5.26 Extremally disconnected spaces#

Tag 08YI, a definition

Tag 08YJ, a lemma

Tag 08YK, a lemma

Tag 08YL, a lemma

Tag 08YM, a lemma

Tag 08YN, a proposition

Tag 090B, a lemma

Tag 090C, an example

Tag 090D, a lemma

Tag 090E, a remark

Sources

Section5.27 Miscellany#

Tag 0069, a lemma

Tag 06RM, a definition

Sources

Section5.28 Partitions and stratifications#

Tag 09XZ, a definition

Tag 09Y0, a definition

Tag 09Y1, a definition

Tag 0BDS, a definition

Tag 09Y2, a remark

Tag 09Y3, a lemma

Tag 09Y4, a lemma

Tag 09Y5, a lemma

Sources

Section5.29 Colimits of spaces#

Tag 0B1X, a lemma

Sources

Section5.30 Topological groups, rings, modules#

Tag 0B1Z, a definition

Tag 0BMC, an example

Tag 0B20, a lemma

Tag 0BR1, a lemma

Tag 0BR2, a definition

Tag 0B21, a lemma

Tag 0B22, a definition

Tag 0B23, a lemma

Tag 0B24, a lemma

Tag 0B25, a definition

Tag 0B26, a lemma

Tag 0B27, a lemma

Sources

Section5.23 Spectral spaces #

Section5.24 Limits of spectral spaces #

Section5.25 Stone-Čech compactification #

Section5.26 Extremally disconnected spaces #

Section5.27 Miscellany #

Section5.28 Partitions and stratifications #

Section5.29 Colimits of spaces #

Section5.30 Topological groups, rings, modules #