@@ -3,6 +3,7 @@ Copyright (c) 2024 Yaël Dillies. All rights reserved.
33Released under Apache 2.0 license as described in the file LICENSE.
44Authors: Yaël Dillies
55-/
6+ import Mathlib.Tactic.StacksAttribute
67import Mathlib.Topology.Compactness.Compact
78import Mathlib.Topology.Separation.Basic
89import LeanCamCombi.GrowthInGroups.BooleanSubalgebra
@@ -13,36 +14,36 @@ import LeanCamCombi.GrowthInGroups.BooleanSubalgebra
1314
1415open Set
1516
16- variable {α : Type *} [TopologicalSpace α] {s t : Set α} {a : α}
17+ variable {α β : Type *} [TopologicalSpace α] [TopologicalSpace β] {s t : Set α} (f : α → β) {a : α}
1718
1819/-! ### Retrocompact sets -/
1920
20- def IsRetrocompact (s : Set α) : Prop := ∀ ⦃U⦄, IsCompact U → IsOpen U → IsCompact (s ∩ U)
21+ def IsRetroCompact (s : Set α) : Prop := ∀ ⦃U⦄, IsCompact U → IsOpen U → IsCompact (s ∩ U)
2122
22- @[simp] lemma IsRetrocompact .emptyIsRetrocompact (∅ : Set α) := by simp [IsRetrocompact ]
23+ @[simp] lemma IsRetroCompact .emptyIsRetroCompact (∅ : Set α) := by simp [IsRetroCompact ]
2324
24- @[simp] lemma IsRetrocompact .singletonIsRetrocompact {a} :=
25+ @[simp] lemma IsRetroCompact .singletonIsRetroCompact {a} :=
2526 fun _ _ _ ↦ Subsingleton.singleton_inter.isCompact
2627
27- lemma IsRetrocompact .unionIsRetrocompact s) (ht : IsRetrocompact t) :
28- IsRetrocompact (s ∪ t : Set α) :=
28+ lemma IsRetroCompact .unionIsRetroCompact s) (ht : IsRetroCompact t) :
29+ IsRetroCompact (s ∪ t : Set α) :=
2930 fun _U hUcomp hUopen ↦ union_inter_distrib_right .. ▸ (hs hUcomp hUopen).union (ht hUcomp hUopen)
3031
31- lemma IsRetrocompact .interIsRetrocompact s) (ht : IsRetrocompact t) :
32- IsRetrocompact (s ∩ t : Set α) :=
32+ lemma IsRetroCompact .interIsRetroCompact s) (ht : IsRetroCompact t) :
33+ IsRetroCompact (s ∩ t : Set α) :=
3334 fun _U hUcomp hUopen ↦ inter_inter_distrib_right .. ▸ (hs hUcomp hUopen).inter (ht hUcomp hUopen)
3435
35- lemma IsRetrocompact .inter_isOpenIsRetrocompact s) (ht : IsRetrocompact t)
36- (htopen : IsOpen t) : IsRetrocompact (s ∩ t : Set α) :=
36+ lemma IsRetroCompact .inter_isOpenIsRetroCompact s) (ht : IsRetroCompact t)
37+ (htopen : IsOpen t) : IsRetroCompact (s ∩ t : Set α) :=
3738 fun _U hUcomp hUopen ↦ inter_assoc .. ▸ hs (ht hUcomp hUopen) (htopen.inter hUopen)
3839
39- lemma IsRetrocompact .isOpen_interIsRetrocompact s) (ht : IsRetrocompact t)
40- (hsopen : IsOpen s) : IsRetrocompact (s ∩ t : Set α) :=
40+ lemma IsRetroCompact .isOpen_interIsRetroCompact s) (ht : IsRetroCompact t)
41+ (hsopen : IsOpen s) : IsRetroCompact (s ∩ t : Set α) :=
4142 inter_comm .. ▸ ht.inter_isOpen hs hsopen
4243
4344def IsConstructible (s : Set α) : Prop :=
4445 ∃ F : Set (Set α × Set α), F.Finite ∧ ⋃ UV ∈ F, UV.1 \ UV.2 = s ∧
45- ∀ UV ∈ F, IsOpen UV.1 ∧ IsOpen UV.2 ∧ IsRetrocompact UV.1 ∧ IsRetrocompact UV.2
46+ ∀ UV ∈ F, IsOpen UV.1 ∧ IsOpen UV.2 ∧ IsRetroCompact UV.1 ∧ IsRetroCompact UV.2
4647
4748@[simp] lemma IsConstructible.empty : IsConstructible (∅ : Set α) := ⟨∅, by simp⟩
4849
@@ -68,4 +69,55 @@ lemma IsConstructible.union (hs : IsConstructible s) (ht : IsConstructible t) :
6869
6970def IsLocallyConstructible (s : Set α) : Prop :=
7071 ∃ F : Set (Set α × Set α), F.Finite ∧ ⋃ UV ∈ F, UV.1 \ UV.2 = s ∧
71- ∀ UV ∈ F, IsOpen UV.1 ∧ IsOpen UV.2 ∧ IsRetrocompact UV.1 ∧ IsRetrocompact UV.2
72+ ∀ UV ∈ F, IsOpen UV.1 ∧ IsOpen UV.2 ∧ IsRetroCompact UV.1 ∧ IsRetroCompact UV.2
73+
74+ lemma IsRetroCompact.isCompact [CompactSpace α] {s : Set α} (hs : IsRetroCompact s) :
75+ IsCompact s := by
76+ simpa using hs CompactSpace.isCompact_univ
77+
78+ lemma IsRetroCompact.isConstructible {s : Set α} (hs : IsRetroCompact s)
79+ (hs' : IsOpen s) : IsConstructible s := sorry
80+
81+
82+ @[stacks 09YD]
83+ lemma IsConstructible.image_of_isOpenEmbedding {s : Set α} (hs : IsConstructible s)
84+ (hf : IsOpenEmbedding f) (hf' : IsRetroCompact (Set.range f)) : IsConstructible (f '' s) :=
85+ sorry
86+
87+ @[stacks 005J]
88+ lemma IsConstructible.preimage_of_isOpenEmbedding {s : Set β} (hs : IsConstructible s)
89+ (hf : IsOpenEmbedding f) : IsConstructible (f ⁻¹' s) :=
90+ sorry
91+
92+ @[stacks 09YG]
93+ lemma IsConstructible.image_of_isClosedEmbedding {s : Set α} (hs : IsConstructible s)
94+ (hf : IsClosedEmbedding f) (hf' : IsRetroCompact (Set.range f)ᶜ) : IsConstructible (f '' s) :=
95+ sorry
96+
97+ @[stacks 09YE]
98+ lemma IsConstructible.preimage_of_isClosedEmbedding {s : Set β} (hs : IsConstructible s)
99+ (hf : IsClosedEmbedding f) (hf' : IsCompact (Set.range f)ᶜ) : IsConstructible (f ⁻¹' s) :=
100+ sorry
101+
102+ variable {ι} (b : ι → Set α) (hb : TopologicalSpace.IsTopologicalBasis (Set.range b))
103+
104+ include hb in
105+ lemma isRetroCompact_iff_isCompact_of_isTopologicalBasis [CompactSpace α]
106+ (hb' : ∀ i j, IsCompact (b i ∩ b j))
107+ {U : Set α} (hU : IsOpen U) :
108+ IsRetroCompact U ↔ IsCompact U := by
109+ refine ⟨IsRetroCompact.isCompact, fun hU' {V} hV' hV ↦ ?_⟩
110+ have hb'' : ∀ i, IsCompact (b i) := fun i ↦ by simpa using hb' i i
111+ obtain ⟨s, hs, rfl⟩ :=
112+ (isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis b hb hb'' U).mp ⟨hU', hU⟩
113+ obtain ⟨t, ht, rfl⟩ :=
114+ (isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis b hb hb'' V).mp ⟨hV', hV⟩
115+ simp only [Set.iUnion_inter, Set.inter_iUnion]
116+ exact ht.isCompact_biUnion fun _ _ ↦ hs.isCompact_biUnion fun _ _ ↦ (hb' _ _)
117+
118+ include hb in
119+ lemma IsConstructible.induction_of_isTopologicalBasis
120+ (P : Set α → Prop )
121+ (hP : ∀ i s, Set.Finite s → P (b i \ ⋃ j ∈ s, b j))
122+ (hP' : ∀ s t, P s → P t → P (s ∪ t))
123+ (s : Set α) (hs : IsConstructible s) : P s := sorry
0 commit comments