OAI/AlgebraicTopology/IntegralHomology/Subdivision.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Singular subdivision, small-chain homotopies, and iterated mesh bounds.

  1. def OAI.Kaplansky.simplexTupleHull line 18

    Source documentation

    The ambient convex hull of a tuple's vertices.

    def simplexTupleHull {n : ℕ} (v : Fin (n+1) → StdSimplex ℝ κ) : Set (κ → ℝ) :=
…
  2. theorem OAI.Kaplansky.simplexTupleHull_vertex line 21
  3. theorem OAI.Kaplansky.simplexTupleHull_face line 24
  4. theorem OAI.Kaplansky.simplexTupleCenter_mem_hull line 32
  5. theorem OAI.Kaplansky.simplexTupleCenter_hull_dist_le line 43

    Source documentation

    The barycenter contraction estimate holds on the entire old convex hull.

    theorem simplexTupleCenter_hull_dist_le {n : ℕ} (v : Fin (n+2) → StdSimplex ℝ κ)
    (D : ℝ) (hv : ∀ i j, dist (v i) (v j) ≤ D)
    (x : StdSimplex ℝ κ) (hx : ⇑x.weights ∈ simplexTupleHull v) :
    dist (simplexTupleCenter n v) x ≤ ((n+1 : ℝ)/(n+2))*D := by
…

    Mentions: OAI.Kaplansky.simplexTupleHull, OAI.Kaplansky.simplexTupleCenter

  6. def OAI.Kaplansky.tupleHullMesh line 56

    Source documentation

    Support condition recording both the original hull and the new mesh.

    def tupleHullMesh {n m : ℕ} (v : Fin (n+1) → StdSimplex ℝ κ) (D : ℝ)
    (w : Fin (m+1) → StdSimplex ℝ κ) : Prop :=
…
  7. theorem OAI.Kaplansky.tupleSubdivision_mesh line 62

    Source documentation

    Every simplex in one barycentric subdivision has mesh at most n/(n+1) times the old vertex mesh. Support is expressed in the actual free chain group.

    theorem tupleSubdivision_mesh (n : ℕ) (v : Fin (n+1) → StdSimplex ℝ κ)
    (D : ℝ) (hD : 0 ≤ D) (hv : ∀ i j, dist (v i) (v j) ≤ D) :
    tupleSubdivisionMap simplexTupleCenter n (tupleGen v (1 : ℤ)) ∈
      tupleChainSpan (tupleHullMesh v (((n : ℝ)/(n+1))*D)) := by
…

    Mentions: OAI.Kaplansky.tupleSubdivisionMap, OAI.Kaplansky.simplexTupleCenter, OAI.Kaplansky.tupleGen, OAI.Kaplansky.tupleChainSpan, OAI.Kaplansky.tupleHullMesh

  8. def OAI.Kaplansky.singularSimplexTopMap line 111

    Source documentation

    The actual map represented by a singular simplex, with unlifted domain.

    def singularSimplexTopMap {X : TopCat.{0}} {n : ℕ}
    (σ : (TopCat.toSSet.obj X) _⦋n⦌) : standardSimplexSpace n ⟶ X :=
…

    Mentions: OAI.Kaplansky.standardSimplexSpace

  9. theorem OAI.Kaplansky.singularGen_map line 116
  10. theorem OAI.Kaplansky.singularGen_boundary line 124
  11. theorem OAI.Kaplansky.singularSimplexTopMap_face line 131
  12. theorem OAI.Kaplansky.singularSimplexTopMap_map line 137
  13. theorem OAI.Kaplansky.singularGen_identity_map line 142
  14. def OAI.Kaplansky.singularSubdivisionMap line 150

    Source documentation

    Barycentric subdivision on the existing integral singular chains.

    def singularSubdivisionMap (X : TopCat.{0}) (n : ℕ) :
    (integralSingularChains.obj X).X n ⟶ (integralSingularChains.obj X).X n :=
…
  15. theorem OAI.Kaplansky.singularGen_subdivision line 156
  16. theorem OAI.Kaplansky.singularSubdivisionMap_d line 163
  17. def OAI.Kaplansky.singularSubdivision line 176

    Source documentation

    Constructed chain endomorphism, with no subdivision or excision hypothesis.

    def singularSubdivision (X : TopCat.{0}) :
    integralSingularChains.obj X ⟶ integralSingularChains.obj X :=
…
  18. theorem OAI.Kaplansky.singularSubdivision_naturality line 181
  19. def OAI.Kaplansky.singularSubdivisionPrism line 194

    Source documentation

    The universal prism transported along each actual singular simplex.

    def singularSubdivisionPrism (X : TopCat.{0}) (n : ℕ) :
    (integralSingularChains.obj X).X n ⟶ (integralSingularChains.obj X).X (n+1) :=
…
  20. theorem OAI.Kaplansky.singularGen_prism line 200
  21. theorem OAI.Kaplansky.singularSubdivisionPrism_zero line 207
  22. theorem OAI.Kaplansky.singularSubdivisionMap_zero line 214
  23. theorem OAI.Kaplansky.singularSubdivisionPrism_equation line 221

    Source documentation

    The chain homotopy equation on actual singular chains in all positive degrees.

    theorem singularSubdivisionPrism_equation (X : TopCat.{0}) (n : ℕ) :
    singularSubdivisionPrism X (n+1) ≫ (integralSingularChains.obj X).d (n+2) (n+1) =
      𝟙 _ - singularSubdivisionMap X (n+1) -
      (integralSingularChains.obj X).d (n+1) n ≫ singularSubdivisionPrism X n := by
…

    Mentions: OAI.Kaplansky.singularSubdivisionPrism, OAI.Kaplansky.singularSubdivisionMap

  24. def OAI.Kaplansky.singularSubdivisionHomotopy line 238

    Source documentation

    An explicit homotopy between the identity and barycentric subdivision.

    def singularSubdivisionHomotopy (X : TopCat.{0}) :
    Homotopy (𝟙 (integralSingularChains.obj X)) (singularSubdivision X) :=
…

    Mentions: OAI.Kaplansky.singularSubdivision

  25. theorem OAI.Kaplansky.singularSubdivisionPrism_naturality line 247
  26. theorem OAI.Kaplansky.singularSubdivision_homologyMap line 256

    Source documentation

    Subdivision acts as the identity on actual integral singular homology.

    theorem singularSubdivision_homologyMap (X : TopCat.{0}) (n : ℕ) :
    HomologicalComplex.homologyMap (singularSubdivision X) n = 𝟙 _ := by
…

    Mentions: OAI.Kaplansky.singularSubdivision

  27. theorem OAI.Kaplansky.smallSimplex_carrier line 264

    Source documentation

    Every singular simplex inside the image of a small simplex remains small. The statement uses the entire simplex image, so it also controls the prism.

    theorem smallSimplex_carrier {n : ℕ} (σ : (smallSingularSet U V) _⦋n⦌) :
    SSet.Subcomplex.range (TopCat.toSSet.map (singularSimplexTopMap σ.val)) ≤
      singularSubset U ⊔ singularSubset V := by
…

    Mentions: OAI.Kaplansky.smallSingularSet, OAI.Kaplansky.singularSimplexTopMap, OAI.Kaplansky.singularSubset

  28. def OAI.Kaplansky.smallSimplexCarrier line 279
  29. def OAI.Kaplansky.smallSimplexChains line 284
  30. theorem OAI.Kaplansky.smallSimplexChains_inclusion line 289
  31. abbrev OAI.Kaplansky.smallSingularGen line 295
  32. theorem OAI.Kaplansky.smallSingularChains_hom_ext line 300

    Source documentation

    Maps from small chains are determined by their values on small singular simplices.

    theorem smallSingularChains_hom_ext {n : ℕ} {T : ModuleCat.{0} ℤ}
    {f g : (smallSingularChains U V).X n ⟶ T}
    (h : ∀ σ : (smallSingularSet U V) _⦋n⦌,
      smallSingularGen U V σ ≫ f = smallSingularGen U V σ ≫ g) : f = g :=
…

    Mentions: OAI.Kaplansky.smallSingularChains, OAI.Kaplansky.smallSingularSet, OAI.Kaplansky.smallSingularGen

  33. theorem OAI.Kaplansky.smallSingularGen_inclusion line 307
  34. def OAI.Kaplansky.smallSubdivisionMap line 313

    Source documentation

    Subdivision restricted to the actual small chain groups.

    def smallSubdivisionMap (n : ℕ) : (smallSingularChains U V).X n ⟶ (smallSingularChains U V).X n :=
…

    Mentions: OAI.Kaplansky.smallSingularChains

  35. def OAI.Kaplansky.smallSubdivisionPrism line 317

    Source documentation

    The prism restricted to the same small chain groups.

    def smallSubdivisionPrism (n : ℕ) :
    (smallSingularChains U V).X n ⟶ (smallSingularChains U V).X (n+1) :=
…

    Mentions: OAI.Kaplansky.smallSingularChains

  36. theorem OAI.Kaplansky.smallGen_subdivision line 322
  37. theorem OAI.Kaplansky.smallGen_prism line 328
  38. theorem OAI.Kaplansky.smallSubdivisionMap_inclusion line 334
  39. theorem OAI.Kaplansky.smallSubdivisionPrism_inclusion line 345
  40. theorem OAI.Kaplansky.smallSubdivisionMap_d line 356

    Source documentation

    The restriction remains a chain map, proved by injectivity of inclusion.

    theorem smallSubdivisionMap_d (n : ℕ) :
    smallSubdivisionMap U V (n+1) ≫ (smallSingularChains U V).d (n+1) n =
      (smallSingularChains U V).d (n+1) n ≫ smallSubdivisionMap U V n := by
…

    Mentions: OAI.Kaplansky.smallSubdivisionMap, OAI.Kaplansky.smallSingularChains

  41. def OAI.Kaplansky.smallSubdivision line 364
  42. theorem OAI.Kaplansky.simplexCombination_assoc line 372

    Source documentation

    Composition of affine interpolations is affine interpolation of the images.

    theorem simplexCombination_assoc {ι κ μ : Type} [Fintype ι] [Fintype κ] [Fintype μ]
    (w : κ → StdSimplex ℝ μ) (v : ι → StdSimplex ℝ κ) (t : StdSimplex ℝ ι) :
    simplexCombination w (simplexCombination v t) =
      simplexCombination (simplexCombination w ∘ v) t := by
…

    Mentions: OAI.Kaplansky.simplexCombination

  43. theorem OAI.Kaplansky.simplexTupleCenter_combination line 379
  44. theorem OAI.Kaplansky.simplexAffineChains_combination line 386

    Source documentation

    Naturality of interpolation for all affine simplex maps, not only cofaces.

    theorem simplexAffineChains_combination {k l : ℕ}
    (v : Fin (k+1) → StdSimplex ℝ (Fin (l+1))) :
    tupleChainMap (simplexCombination v) ≫ simplexAffineChains l =
      simplexAffineChains k ≫ integralSingularChains.map (TopCat.ofHom (simplexCombinationMap v)) := by
…

    Mentions: OAI.Kaplansky.tupleChainMap, OAI.Kaplansky.simplexCombination, OAI.Kaplansky.simplexAffineChains, OAI.Kaplansky.simplexCombinationMap

  45. theorem OAI.Kaplansky.simplexAffineChains_subdivision line 407

    Source documentation

    Interpolation intertwines tuple subdivision with singular subdivision. This is needed for iterating the geometric mesh estimate.

    theorem simplexAffineChains_subdivision (k : ℕ) :
    simplexAffineChains k ≫ singularSubdivision (standardSimplexSpace k) =
      tupleSubdivision simplexTupleCenter ≫ simplexAffineChains k := by
…

    Mentions: OAI.Kaplansky.simplexAffineChains, OAI.Kaplansky.singularSubdivision, OAI.Kaplansky.standardSimplexSpace, OAI.Kaplansky.tupleSubdivision, OAI.Kaplansky.simplexTupleCenter

  46. theorem OAI.Kaplansky.smallSubdivisionMap_zero line 436
  47. theorem OAI.Kaplansky.smallSubdivisionPrism_zero line 442
  48. theorem OAI.Kaplansky.smallSubdivisionPrism_equation line 448

    Source documentation

    The homotopy equation also holds before inclusion into full chains.

    theorem smallSubdivisionPrism_equation (n : ℕ) :
    smallSubdivisionPrism U V (n+1) ≫ (smallSingularChains U V).d (n+2) (n+1) =
      𝟙 _ - smallSubdivisionMap U V (n+1) -
      (smallSingularChains U V).d (n+1) n ≫ smallSubdivisionPrism U V n := by
…

    Mentions: OAI.Kaplansky.smallSubdivisionPrism, OAI.Kaplansky.smallSingularChains, OAI.Kaplansky.smallSubdivisionMap

  49. def OAI.Kaplansky.smallSubdivisionHomotopy line 460
  50. theorem OAI.Kaplansky.smallSubdivision_homologyMap line 469

    Source documentation

    Small-chain subdivision induces the identity on homology, without any cover hypothesis. Comparison to full homology still needs eventual smallness.

    theorem smallSubdivision_homologyMap (n : ℕ) :
    HomologicalComplex.homologyMap (smallSubdivision U V) n = 𝟙 _ := by
…

    Mentions: OAI.Kaplansky.smallSubdivision

  51. theorem OAI.Kaplansky.smallSubdivision_inclusion line 474
  52. def OAI.Kaplansky.tupleMeshSpan line 485
  53. theorem OAI.Kaplansky.tupleSubdivision_mem_mesh line 490

    Source documentation

    Subdivision contracts the mesh of an arbitrary supported affine chain.

    theorem tupleSubdivision_mem_mesh {n : ℕ} (D : ℝ) (hD : 0 ≤ D)
    {c : (tupleChains (StdSimplex ℝ κ)).X n} (hc : c ∈ tupleMeshSpan n D) :
    tupleSubdivisionMap simplexTupleCenter n c ∈ tupleMeshSpan n (((n : ℝ)/(n+1))*D) := by
…

    Mentions: OAI.Kaplansky.tupleChains, OAI.Kaplansky.tupleMeshSpan, OAI.Kaplansky.tupleSubdivisionMap, OAI.Kaplansky.simplexTupleCenter

  54. theorem OAI.Kaplansky.tupleSubdivision_iterate_mesh line 498

    Source documentation

    Actual geometric decay for every iterated barycentric subdivision, including repeated or degenerate vertices and the degree-zero case.

    theorem tupleSubdivision_iterate_mesh {n : ℕ} (D : ℝ) (hD : 0 ≤ D)
    {c : (tupleChains (StdSimplex ℝ κ)).X n} (hc : c ∈ tupleMeshSpan n D) (k : ℕ) :
    (tupleSubdivisionMap simplexTupleCenter n)^[k] c ∈
      tupleMeshSpan n (D * ((n : ℝ)/(n+1))^k) := by
…

    Mentions: OAI.Kaplansky.tupleChains, OAI.Kaplansky.tupleMeshSpan, OAI.Kaplansky.tupleSubdivisionMap, OAI.Kaplansky.simplexTupleCenter

  55. theorem OAI.Kaplansky.simplexVertices_mem_mesh line 512

    Source documentation

    The universal vertex tuple starts with mesh at most one in the actual sup metric of the library's standard simplex.

    theorem simplexVertices_mem_mesh (n : ℕ) :
    tupleGen (StdSimplex.single (R := ℝ) (X := Fin (n+1))) (1 : ℤ) ∈
…

    Mentions: OAI.Kaplansky.tupleGen

  56. theorem OAI.Kaplansky.universalTupleSubdivision_mesh line 525

    Source documentation

    Geometric mesh estimate for the universal subdivided simplex.

    theorem universalTupleSubdivision_mesh (n k : ℕ) :
    (tupleSubdivisionMap simplexTupleCenter n)^[k]
      (tupleGen (StdSimplex.single (R := ℝ) (X := Fin (n+1))) (1 : ℤ)) ∈
…

    Mentions: OAI.Kaplansky.tupleSubdivisionMap, OAI.Kaplansky.simplexTupleCenter, OAI.Kaplansky.tupleGen

  57. theorem OAI.Kaplansky.simplexMeshFactor_lt_one line 532

    Source documentation

    The mesh factor is strictly less than one in every fixed degree.

    theorem simplexMeshFactor_lt_one (n : ℕ) : (n : ℝ)/(n+1) < 1 := by
…
  58. theorem OAI.Kaplansky.singularSubdivision_iterate_gen line 543

    Source documentation

    Iteration on an actual singular simplex agrees with the constructed iterated affine subdivision inside its domain.

    theorem singularSubdivision_iterate_gen {X : TopCat.{0}} {n : ℕ}
    (σ : (TopCat.toSSet.obj X) _⦋n⦌) (k : ℕ) :
    (singularSubdivisionMap X n)^[k] (singularGen σ (1 : ℤ)) =
      (integralSingularChains.map (singularSimplexTopMap σ)).f n
        ((simplexAffineChains n).f n
          ((tupleSubdivisionMap simplexTupleCenter n)^[k]
            (tupleGen (StdSimplex.single (R := ℝ) (X := Fin (n+1))) (1 : ℤ)))) := by
…

    Mentions: OAI.Kaplansky.singularSubdivisionMap, OAI.Kaplansky.singularGen, OAI.Kaplansky.singularSimplexTopMap, OAI.Kaplansky.simplexAffineChains, OAI.Kaplansky.tupleSubdivisionMap, OAI.Kaplansky.simplexTupleCenter, OAI.Kaplansky.tupleGen

  59. theorem OAI.Kaplansky.small_singularGen_mem_range line 572

    Source documentation

    A singular generator that is small belongs to the actual image of the small-chain inclusion.

    theorem small_singularGen_mem_range {X : Type} [TopologicalSpace X] (U V : Set X)
    {n : ℕ} (σ : (TopCat.toSSet.obj (TopCat.of X)) _⦋n⦌)
    (hσ : σ ∈ (singularSubset U ⊔ singularSubset V).obj (Opposite.op ⦋n⦌)) :
    singularGen σ (1 : ℤ) ∈ LinearMap.range ((smallSingularChainInclusion U V).f n).hom := by
…

    Mentions: OAI.Kaplansky.singularSubset, OAI.Kaplansky.singularGen, OAI.Kaplansky.smallSingularChainInclusion