comments

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 :=

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

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]
@@ -116,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,

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⟩

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.

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