From 6a3ff7a9e7a7b300bd46123cf1ad099b5cf1ef18 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 11 Jul 2024 16:57:03 +0200 Subject: [PATCH 1/2] comments --- CWcomplexes/Definition.lean | 97 ++++++++++++++++++++++++------------- CWcomplexes/Lemmas.lean | 4 ++ CWcomplexes/auxiliary.lean | 54 ++++++--------------- 3 files changed, 80 insertions(+), 75 deletions(-) diff --git a/CWcomplexes/Definition.lean b/CWcomplexes/Definition.lean index 292b70b..d3ee7c8 100644 --- a/CWcomplexes/Definition.lean +++ b/CWcomplexes/Definition.lean @@ -32,9 +32,15 @@ class CWComplex.{u} {X : Type u} [TopologicalSpace X] (C : Set X) where union : ⋃ (n : ℕ) (j : cell n), map n j '' closedBall 0 1 = C variable [T2Space X] (C : Set X) [hC : CWComplex C] - +/- Now that `CWComplex` is a class, try to remove `hC` everywhere, and instead make +`C` explicit if needed (for `map` it's probably fine to have `C` explicit, and have Lean infer `C` +from the type of `i : cell C n`, though sometimes you might have to give it explicitly with +`map (C := C)` +-/ namespace CWComplex + + /-- A non-standard definition of the levels useful for induction. The typical level is defined in terms of levelaux.-/ def levelaux (n : ℕ∞) : Set X := @@ -44,6 +50,10 @@ def levelaux (n : ℕ∞) : Set X := def level (n : ℕ∞) : Set X := hC.levelaux (n + 1) +-- I recommend to avoid a lemma like this (and subtraction on the natural numbers in general), +-- if possible. +-- When you want to apply tris, try to instead rewrite +-- it to `hC.levelaux (m + 1) = hC.level m` which is true by definition. lemma levelaux_eq_level_sub_one {n : ℕ∞} (npos : n ≠ 0) : hC.levelaux n = hC.level (n - 1) := by unfold level congrm (hC.levelaux ?_) @@ -75,7 +85,7 @@ class Finite.{u} {X : Type u} [TopologicalSpace X] (C : Set X) [cwcomplex : CWCo @[simp] lemma level_top : hC.level ⊤ = C := by simp only [level, top_add, levelaux_top] -lemma iUnion_map_sphere_subset_levelaux (l : ℕ) : ⋃ (j : hC.cell l), ↑(hC.map l j) '' sphere 0 1 ⊆ hC.levelaux l := by +lemma iUnion_map_sphere_subset_levelaux (l : ℕ) : ⋃ (j : hC.cell l), hC.map l j '' sphere 0 1 ⊆ hC.levelaux l := by rw [CWComplex.levelaux] norm_cast intro x xmem @@ -92,9 +102,12 @@ lemma iUnion_map_sphere_subset_levelaux (l : ℕ) : ⋃ (j : hC.cell l), ↑(hC. exact ⟨iltl, ⟨e, ymem⟩⟩ exact this xmeme +-- fix the statement lemma iUnion_map_sphere_subset_level (l : ℕ) : ⋃ (j : hC.cell l), ↑(hC.map l j) '' sphere 0 1 ⊆ hC.levelaux l := by simp only [level, iUnion_map_sphere_subset_levelaux] +-- rename: levelaux_mono (the idea is that this statement is equivalent to `Monotone (hC.levelaux)`, +-- even though you probably don't want to state it like that). lemma levelaux_subset_levelaux_of_le {n m : ℕ∞} (h : m ≤ n) : hC.levelaux m ⊆ hC.levelaux n := by repeat rw [CWComplex.levelaux] intro x xmem @@ -113,15 +126,9 @@ lemma level_subset_level_of_le {n m : ℕ∞} (h : m ≤ n) : hC.level m ⊆ hC. lemma iUnion_levelaux_eq_levelaux (n : ℕ∞) : ⋃ (m : ℕ) (hm : m < n + 1), hC.levelaux m = hC.levelaux n := by apply subset_antisymm - · intro x xmem - rw [mem_iUnion] at xmem - rcases xmem with ⟨m, xmemm⟩ - simp at xmemm - have h : m ≤ n := by - apply Order.le_of_lt_succ - rw [ENat.succ_def] - exact xmemm.1 - exact (hC.levelaux_subset_levelaux_of_le h) xmemm.2 + · simp_rw [iUnion_subset_iff] + intros i hi + exact levelaux_subset_levelaux_of_le _ (ENat.le_of_lt_add_one hi) · intro x xmem rw [mem_iUnion] by_cases h : n = ⊤ @@ -149,33 +156,44 @@ lemma iUnion_levelaux_eq_levelaux (n : ℕ∞) : ⋃ (m : ℕ) (hm : m < n + 1), rw [coemn] exact ⟨lt_add_one m, xmem⟩ +-- is this really missing? move to auxiliary +lemma ENat.add_coe_lt_add_coe_right {n m : ℕ∞} {k : ℕ} : n + k < m + k ↔ n < m := by + cases' n with n + · simp + cases' m with m + · norm_cast; simp [ENat.coe_lt_top, -Nat.cast_add] + · norm_cast; simp_all + +-- Here is a different proof, but this was more painful than I thought lemma iUnion_level_eq_level (n : ℕ∞) : ⋃ (m : ℕ) (hm : m < n + 1), hC.level m = hC.level n := by - ext x - rw [mem_iUnion] + simp_rw [level, ← iUnion_levelaux_eq_levelaux C (n + 1)] + ext; simp constructor - · intro ⟨i, hi⟩ - simp only [mem_iUnion, exists_prop] at hi - rw [← ENat.succ_def n] at hi - exact (hC.level_subset_level_of_le (Order.le_of_lt_succ hi.1)) hi.2 - · intro xmem - by_cases h : n = ⊤ - · rw [h, hC.level_top, ← hC.union, mem_iUnion] at xmem - rcases xmem with ⟨i, xmem⟩ - use i - simp only [h, top_add, Ne.lt_top (ENat.coe_ne_top i), iUnion_true] - rw [level, levelaux, mem_iUnion] - use i + · intro ⟨i, hin, hiC⟩ + refine ⟨i + 1, ?_, hiC⟩ + push_cast + exact ENat.add_coe_lt_add_coe_right.mpr hin + · intro ⟨i, hin, hiC⟩ + cases' i with i + · refine ⟨0, ?_, levelaux_subset_levelaux_of_le C (by norm_num) hiC⟩ norm_cast - rw [mem_iUnion, exists_prop] - exact ⟨lt_add_one i, xmem⟩ - · push_neg at h - let m := ENat.toNat n - have coemn: ↑m = n := ENat.coe_toNat h - use m - rw [mem_iUnion, exists_prop, ← coemn] - rw [← coemn] at xmem - norm_cast - exact ⟨lt_add_one m, xmem⟩ + -- this should be a lemma + rw [← ENat.one_le_iff_pos] + exact le_add_self + · refine ⟨i, ?_, hiC⟩ + push_cast + exact ENat.add_coe_lt_add_coe_right.mp hin + +/- separate out some lemmas, e.g. +hC.map m j '' closedBall 0 1 ⊆ hC.map m j '' ball 0 1 ∪ levelaux C m +and/or +levelaux C (m + 1) = levelaux C m ∪ ⋃ (j : hC.cell m), hC.map m j '' closedBall 0 1 +and/or +levelaux C (m + 1) = levelaux C m ∪ ⋃ (j : hC.cell m), hC.map m j '' ball 0 1 + +Maybe you're already doing some of that below, without relying on this? +Also, maybe the induction is a little easier if you just do the hard inclusion by induction (and the easy inclusion without induction) +-/ /- We can also define the levels using `ball` instead of `closedBall`, using assumption `mapsto`. -/ lemma iUnion_ball_eq_levelaux (n : ℕ∞) : ⋃ (m : ℕ) (hm : m < n) (j : hC.cell m), hC.map m j '' ball 0 1 = hC.levelaux n := by @@ -237,6 +255,7 @@ lemma iUnion_ball_eq_levelaux (n : ℕ∞) : ⋃ (m : ℕ) (hm : m < n) (j : hC. lemma union' : ⋃ (n : ℕ) (j : hC.cell n), hC.map n j '' ball 0 1 = C := by simp only [← hC.levelaux_top, ← hC.iUnion_ball_eq_levelaux, ENat.coe_lt_top, iUnion_true] +-- rename to `eq_cell_of_not_disjoint` or similar lemma not_disjoint_equal {n : ℕ} {j : hC.cell n} {m : ℕ} {i : hC.cell m} (notdisjoint: ¬ Disjoint (↑(hC.map n j) '' ball 0 1) (↑(hC.map m i) '' ball 0 1)) : (⟨n, j⟩ : (Σ n, hC.cell n)) = ⟨m, i⟩ := by by_contra h' @@ -262,6 +281,11 @@ lemma mapsto_sphere_levelaux (n : ℕ) (j : hC.cell n) (nnezero : n ≠ 0) : Map norm_cast exact ⟨iltn, ⟨j, xmem⟩⟩ +-- Use the command `#lint` here: it will tell you that `nnezero` is not used in the above proof. +-- I recommend writing `#lint` at the bottom of each of your files, and looking at the output. +-- (you can ignore the request for documentation strings, at least until you make a PR to mathlib) +-- This makes the case distinction in `exists_mem_ball_of_mem_levelaux` unnecessary. + lemma mapsto_sphere_level (n : ℕ) (j : hC.cell n) (nnezero : n ≠ 0) : MapsTo (hC.map n j) (sphere 0 1) (hC.level (Nat.pred n)) := by norm_cast rw [level, ← ENat.coe_one, ← ENat.coe_add, Nat.add_one, Nat.succ_pred nnezero] @@ -451,12 +475,15 @@ lemma closure_map_ball_eq_map_closedball {n : ℕ} {j : hC.cell n} : closure (hC apply ContinuousOn.image_closure this simp +-- I think this proof should be moved up, since it can be used to prove some easier estimates that are used earlier. + -- could this proof be simplified using `exists_mem_ball_of_mem_level`? lemma mapsto' (n : ℕ) (i : hC.cell n) : ∃ I : Π m, Finset (hC.cell m), MapsTo (hC.map n i) (sphere 0 1) (⋃ (m < n) (j ∈ I m), hC.map m j '' ball 0 1) := by induction' n using Nat.case_strong_induction_on with n hn · simp [sphere_zero_dim_empty, MapsTo] · rcases hC.mapsto (Nat.succ n) i with ⟨J, hJ⟩ + -- use the `choose` tactic on `hn` let p (x : Σ' (m : {m : ℕ // m ≤ n}), J m) := Classical.choose (hn x.1 (x.1).2 x.2) let I' m := if mltnsucc : m < Nat.succ n then (J m).toSet ∪ ⋃ (l : {l : ℕ // l ≤ n}) (y : J l), p ⟨⟨l, l.2⟩, y⟩ m else (J m).toSet have : ∀ m, Set.Finite (I' m) := by diff --git a/CWcomplexes/Lemmas.lean b/CWcomplexes/Lemmas.lean index 23cca24..196cfdb 100644 --- a/CWcomplexes/Lemmas.lean +++ b/CWcomplexes/Lemmas.lean @@ -10,6 +10,10 @@ namespace CWComplex lemma isClosed_level (n : ℕ∞) : IsClosed (hC.level n) := (hC.CWComplex_level n).isClosed +-- does `ℕ∞` have an induction principle with the cases `0` and `k + 1` (using that `⊤ + 1 = ⊤). +-- that would make this easier, because then you can just use the definition of level instead of +-- needing `levelaux_eq_level_sub_one` +-- Or even better: just prove `isClosed_level` and `CWComplex_level` also for `levelaux` lemma isClosed_levelaux (n : ℕ∞) : IsClosed (hC.levelaux n) := by by_cases nzero : n = 0 · rw [nzero, hC.levelaux_zero_eq_empty] diff --git a/CWcomplexes/auxiliary.lean b/CWcomplexes/auxiliary.lean index 37c2436..4978ccb 100644 --- a/CWcomplexes/auxiliary.lean +++ b/CWcomplexes/auxiliary.lean @@ -10,15 +10,12 @@ noncomputable section lemma aux1 (l : ℕ) {X : Type*} {s : ℕ → Type*} (Y : (m : ℕ) → s m → Set X): ⋃ m, ⋃ (_ : m < Nat.succ l), ⋃ j, Y m j = (⋃ (j : s l), Y l j) ∪ ⋃ m, ⋃ (_ : m < l), ⋃ j, Y m j := by - rw [Set.union_iUnion] - simp_rw [Nat.lt_succ_iff, le_iff_lt_or_eq, Set.iUnion_or, Set.union_comm, Set.iUnion_union_distrib] - congrm ?_ ∪ ⋃ i, ⋃ (_ : i < l), ⋃ j, Y i j ext - simp only [Set.iUnion_iUnion_eq_left, Set.mem_iUnion, exists_const] + simp [Nat.lt_add_one_iff, le_iff_lt_or_eq, or_and_right, exists_or, or_comm] -lemma ENat.coe_lt_top {n : ℕ} : ↑n < (⊤ : ℕ∞) := Ne.lt_top (ENat.coe_ne_top n) +lemma ENat.coe_lt_top {n : ℕ} : ↑n < (⊤ : ℕ∞) := (ENat.coe_ne_top n).lt_top ---use Set.subsingleton +-- reformulate using Set.subsingleton lemma isClosed_inter_singleton {X : Type*} [TopologicalSpace X] [T1Space X] {A : Set X} {a : X} : IsClosed (A ∩ {a}) := by by_cases h : a ∈ A · have : A ∩ {a} = {a} := by simp only [Set.inter_eq_right, Set.singleton_subset_iff, h] @@ -33,48 +30,30 @@ lemma sphere_zero_dim_empty {X : Type*} {h : PseudoMetricSpace (Fin 0 → X)}: ( lemma closed_in_finite {X : Type*} [t : TopologicalSpace X] {ι : Type*} [Finite ι] (A : Set X) (B : ι → Set X) (closed : ∀ i, IsClosed (B i)) (closedini : (∀ (i : ι), ∃ (C : t.Closeds), A ∩ B i = C.1 ∩ B i)) : ∃ (C : t.Closeds), A ∩ ⋃ i, B i = C.1 ∩ ⋃ i, B i := by - let C' i := B i ∩ (Classical.choose (closedini i)).1 + choose C₀ hC₀ using closedini + let C' i := B i ∩ C₀ i let C := ⋃ i, C' i have closedC : IsClosed C := by simp only [C, C'] apply isClosed_iUnion_of_finite - exact fun i ↦ IsClosed.inter (closed i) (Classical.choose (closedini i)).2 + exact fun i ↦ IsClosed.inter (closed i) (C₀ i).2 use ⟨C, closedC⟩ simp only [C, C'] rw [Set.inter_iUnion, Set.iUnion_inter] apply Set.iUnion_congr intro i - rw [Set.inter_comm (B i), Set.inter_assoc, Set.inter_eq_left.2 (Set.subset_iUnion _ i)] - exact Classical.choose_spec (closedini i) + rw [Set.inter_comm (B i), Set.inter_assoc, Set.inter_eq_left.2 (Set.subset_iUnion _ i), hC₀] + rfl --- I feel like this should be easier then this lemma inter_eq_inter_iff_compl {X : Type*} {A B C : Set X} : A ∩ B = C ∩ B ↔ Aᶜ ∩ B = Cᶜ ∩ B := by - constructor - · intro h - ext x - replace h := Set.ext_iff.1 h x - simp only [Set.mem_inter_iff, Set.mem_compl_iff, and_congr_left_iff] at h ⊢ - intro xmemB - apply Iff.not - exact h xmemB - · intro h - ext x - replace h := Set.ext_iff.1 h x - simp only [Set.mem_inter_iff, Set.mem_compl_iff, and_congr_left_iff] at h ⊢ - intro xmemB - rw [← Set.not_not_mem, ← @Set.not_not_mem _ x C] - apply Iff.not - exact h xmemB + constructor <;> (intro; simp_all [Set.ext_iff, not_iff_not]) def EquivFinMap {X : Type*} (m n : ℕ) : (Fin m → X) × (Fin n → X) ≃ (Fin (m + n) → X) := Equiv.trans (Equiv.sumArrowEquivProdArrow _ _ _).symm (Equiv.arrowCongr finSumFinEquiv (Equiv.refl _)) def HomeomorphFinMap1 {X: Type*} [TopologicalSpace X] (m n : ℕ) : (Fin m → X) × (Fin n → X) ≃ₜ (Fin m ⊕ Fin n → X) where - toFun := (Equiv.sumArrowEquivProdArrow _ _ _).symm - invFun := Equiv.sumArrowEquivProdArrow _ _ _ - left_inv := (Equiv.sumArrowEquivProdArrow _ _ _).right_inv - right_inv := (Equiv.sumArrowEquivProdArrow _ _ _).left_inv + toEquiv := (Equiv.sumArrowEquivProdArrow _ _ _).symm continuous_toFun := by - simp only [Equiv.sumArrowEquivProdArrow, Equiv.coe_fn_symm_mk] + simp_rw [Equiv.sumArrowEquivProdArrow, Equiv.toFun_as_coe, Equiv.coe_fn_symm_mk] apply continuous_pi intro i rcases i with i1 | i2 @@ -87,12 +66,9 @@ def HomeomorphFinMap1 {X: Type*} [TopologicalSpace X] (m n : ℕ) : (Fin m → X continuity --is it better to leave this or replace it by an explicit proof def HomeomorphFinMap2 {X: Type*} [TopologicalSpace X] (m n : ℕ) : (Fin m ⊕ Fin n → X) ≃ₜ (Fin (m + n) → X) where - toFun := Equiv.arrowCongr finSumFinEquiv (Equiv.refl _) - invFun := (Equiv.arrowCongr finSumFinEquiv (Equiv.refl _)).symm - left_inv := (Equiv.arrowCongr finSumFinEquiv (Equiv.refl _)).left_inv - right_inv := (Equiv.arrowCongr finSumFinEquiv (Equiv.refl _)).right_inv + toEquiv := Equiv.arrowCongr finSumFinEquiv (Equiv.refl _) -def HomeomorphFinMap {X: Type*} [TopologicalSpace X] (m n : ℕ) : (Fin m → X) × (Fin n → X) ≃ₜ (Fin (m + n) → X) := Homeomorph.trans (HomeomorphFinMap1 _ _) (HomeomorphFinMap2 _ _) +def HomeomorphFinMap {X: Type*} [TopologicalSpace X] (m n : ℕ) : (Fin m → X) × (Fin n → X) ≃ₜ (Fin (m + n) → X) := (HomeomorphFinMap1 _ _).trans (HomeomorphFinMap2 _ _) def IsometryEquivFinMap1 {X: Type*} [PseudoEMetricSpace X] (m n : ℕ) : (Fin m → X) × (Fin n → X) ≃ᵢ (Fin m ⊕ Fin n → X) where toFun := (Equiv.sumArrowEquivProdArrow _ _ _).symm @@ -187,6 +163,4 @@ lemma IsometryEquivFinMapR_image_sphere (m n : ℕ) : (IsometryEquivFinMap m n). rfl lemma prod_closedBall_eq_closedBall {X : Type*} [PseudoMetricSpace X] {m n : ℕ} (x : Fin m → X) (y : Fin n → X) : (Metric.closedBall x 1 : Set (Fin m → X)) ×ˢ (Metric.closedBall y 1 : Set (Fin n → X)) = (Metric.closedBall (x, y) 1: Set ((Fin m → X) × (Fin n → X))) := by - ext z - simp only [Set.mem_prod, Metric.mem_closedBall, PseudoMetricSpace.toDist, - Prod.pseudoMetricSpaceMax, sup_le_iff] + apply closedBall_prod_same -- found using loogle, query `Metric.closedBall, _ ×ˢ _`. `exact?` also finds this. From 288b6b8739f0637e08e2f4c9332bddd48b52175d Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 11 Jul 2024 17:29:43 +0200 Subject: [PATCH 2/2] some more comments --- CWcomplexes/Constructions.lean | 3 ++- CWcomplexes/Lemmas.lean | 6 ++++++ CWcomplexes/Product.lean | 2 ++ CWcomplexes/kification.lean | 10 ++++++++++ 4 files changed, 20 insertions(+), 1 deletion(-) diff --git a/CWcomplexes/Constructions.lean b/CWcomplexes/Constructions.lean index e83aa55..679e21b 100644 --- a/CWcomplexes/Constructions.lean +++ b/CWcomplexes/Constructions.lean @@ -114,7 +114,8 @@ instance CWComplex_level (n : ℕ∞) : CWComplex (hC.level n) where variable {D : Set X} (hD : CWComplex D) - +-- this instance will never work automatically, since type-class inference will not try to find +-- the `Disjoint C D` assumption. So just make it a definition instead instance CWComplex_disjointUnion (disjoint : Disjoint C D) : CWComplex (C ∪ D) where cell n := Sum (hC.cell n) (hD.cell n) map n i := diff --git a/CWcomplexes/Lemmas.lean b/CWcomplexes/Lemmas.lean index 196cfdb..72a55e3 100644 --- a/CWcomplexes/Lemmas.lean +++ b/CWcomplexes/Lemmas.lean @@ -120,6 +120,12 @@ lemma isDiscrete_level_zero {A : Set X} : IsClosed (A ∩ hC.level 0) := by rw [inter_assoc, hC.level_inter_image_closedBall_eq_level_inter_image_sphere (by norm_cast; exact Nat.zero_lt_succ n), ← inter_assoc] exact hC.isClosed_inter_sphere_succ_of_le_isClosed_inter_closedBall hn j +-- I recommend not using `Compacts` or `Closeds`, but just a set with an assumption that it is +-- compact/closed +-- I would prove this not by contradiction, but by applying +-- `IsCompact.elim_finite_subcover` +-- on the family `fun ⟨n, j⟩ ↦ map n j '' ball 0 1` which covers the compact set `A ∩ C` +-- I think also removes everything about `DiscreteTopology` in your proof... lemma compact_inter_finite (A : t.Compacts) : _root_.Finite (Σ (m : ℕ), {j : hC.cell m // ¬ Disjoint A.1 (↑(hC.map m j) '' ball 0 1)}) := by by_contra h simp only [TopologicalSpace.Compacts.carrier_eq_coe, not_disjoint_iff, SetLike.mem_coe, diff --git a/CWcomplexes/Product.lean b/CWcomplexes/Product.lean index d6a507c..c8ebf40 100644 --- a/CWcomplexes/Product.lean +++ b/CWcomplexes/Product.lean @@ -43,6 +43,8 @@ instance CWComplex_product : @CWComplex (X ×ₖ Y) instprodkification (C ×ˢ D cell n := (Σ' (m : ℕ) (l : ℕ) (hml : m + l = n), hC.cell m × hD.cell l) map n i := match i with | ⟨m, l, hmln, j, k⟩ => + /- Instead of a substitution here it will probably be more convenient to suitably compose with the equivalence + `Fin n ≃ Fin (m + l)` (wrapped inside the definition that `→` preserves equivalences). -/ hmln ▸ Equiv.transPartialEquiv ((IsometryEquivFinMap m l).symm).toEquiv (PartialEquiv.prod (hC.map m j) (hD.map l k)) source_eq n i := by rcases i with ⟨m, l, hmln, j, k⟩ diff --git a/CWcomplexes/kification.lean b/CWcomplexes/kification.lean index f657893..d0ff80a 100644 --- a/CWcomplexes/kification.lean +++ b/CWcomplexes/kification.lean @@ -6,6 +6,16 @@ noncomputable section namespace Kification +/- I think I already mentioned this: +it would be great if you define the concept of being a k-space. +Q: Is that related to `IsCompactlyGenerated` (about complete lattices) in Mathlib? I think not, +since that notion only captures compact open sets (`TopologicalSpace.Opens.isCompactElement_iff`). +and then show that +* `kification` is alaway k-space +* The `kification` of a k-space is homeomorph to itself +* you can do `CWComplex_product` if `X × Y` is a k-space. +* generally try to do most theorems below for k-spaces instead of "the k-ification of X". +-/ def kification (X : Type*) := X instance instkification {X : Type*} [t : TopologicalSpace X] : TopologicalSpace (kification X) where