SmallChains.lean`

28 declarations, 0 contain sorry, 0 declared as axioms

Simplicial gluing, small singular subcomplexes, and cover meshes.

def OAI.Kaplansky.integralSimplicialChains line 24
Source documentation
Integral simplicial chains, using the same free-chain construction as the preserved integral singular chain complex.
```
def integralSimplicialChains : SSet.{0} ⥤ ChainComplex (ModuleCat.{0} ℤ) ℕ :=
…
```
instance OAI.Kaplansky.integralSimplicialChains_preservesColimitsOfShape line 27
instance OAI.Kaplansky.integralSimplicialChains_preservesMonomorphisms line 36

theorem OAI.Kaplansky.subcomplexChains_isPushout line 47

Source documentation

Chains in a union of subcomplexes form the actual pushout over their intersection. No topological excision assertion is used.

theorem subcomplexChains_isPushout :
    IsPushout
      (integralSimplicialChains.map (SSet.Subcomplex.homOfLE (inf_le_left : U ⊓ V ≤ U)))
      (integralSimplicialChains.map (SSet.Subcomplex.homOfLE (inf_le_right : U ⊓ V ≤ V)))
      (integralSimplicialChains.map (SSet.Subcomplex.homOfLE (le_sup_left : U ≤ U ⊔ V)))
      (integralSimplicialChains.map (SSet.Subcomplex.homOfLE (le_sup_right : V ≤ U ⊔ V))) := by
…

def OAI.Kaplansky.subcomplexChainSequence line 56
theorem OAI.Kaplansky.subcomplexChainSequence_shortExact line 59

def OAI.Kaplansky.subcomplexRelativeChainIso line 71

Source documentation

The chain-level relative excision map for a union of simplicial subcomplexes. The map is an isomorphism before taking homology.

def subcomplexRelativeChainIso :
    cokernel (integralSimplicialChains.map
      (SSet.Subcomplex.homOfLE (inf_le_left : U ⊓ V ≤ U))) ≅
    cokernel (integralSimplicialChains.map
      (SSet.Subcomplex.homOfLE (le_sup_right : V ≤ U ⊔ V))) := by
…

def OAI.Kaplansky.singularSimplexMap line 84
def OAI.Kaplansky.singularSubset line 90
Source documentation
Singular simplices whose entire image lies in the specified subspace.
```
def singularSubset (U : Set X) : (TopCat.toSSet.obj (TopCat.of X)).Subcomplex :=
…
```
theorem OAI.Kaplansky.mem_singularSubset_iff line 93
theorem OAI.Kaplansky.singularSubset_mono line 104
theorem OAI.Kaplansky.singularSubset_inter line 110
theorem OAI.Kaplansky.singularSubset_univ line 119
def OAI.Kaplansky.singularSubsetIso line 125
Source documentation
Identification with singular simplices of the actual subspace, including its inherited topology, rather than a replacement chain theory.
```
def singularSubsetIso (U : Set X) :
    TopCat.toSSet.obj (TopCat.of U) ≅ (singularSubset U).toSSet := by
…
```
Mentions: OAI.Kaplansky.singularSubset
theorem OAI.Kaplansky.singularSubsetIso_hom_ι line 133
def OAI.Kaplansky.singularSubsetChainsIso line 137
def OAI.Kaplansky.smallSingularSet line 144
Source documentation
The complex of simplices small for the two-set family. Its simplices lie wholly in one member, which need not hold for an arbitrary singular simplex.
```
def smallSingularSet (U V : Set X) : SSet.{0} :=
…
```
def OAI.Kaplansky.smallSingularChains line 147
def OAI.Kaplansky.smallSingularChainInclusion line 150
instance OAI.Kaplansky.(instance at line 154) line 154
theorem OAI.Kaplansky.mem_smallSingularSet_iff line 157
def OAI.Kaplansky.smallSingularChainSequence line 167
Source documentation
Proven gluing sequence for actual small singular chains. A quasi-isomorphism from small to full chains is a separate subdivision theorem.
```
def smallSingularChainSequence (U V : Set X) :=
…
```
theorem OAI.Kaplansky.smallSingularChainSequence_shortExact line 170

theorem OAI.Kaplansky.continuousMap_cover_mesh line 182

Source documentation

A sufficiently small subset of the domain of one singular simplex is carried into one member of a two-set open cover.

theorem continuousMap_cover_mesh (σ : C(P, X)) (U V : Set X)
    (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) :
    ∃ δ > 0, ∀ s : Set P, (∀ a ∈ s, ∀ b ∈ s, dist a b < δ) →
      (∀ a ∈ s, σ a ∈ U) ∨ (∀ a ∈ s, σ a ∈ V) := by
…

theorem OAI.Kaplansky.finite_continuousMaps_cover_mesh line 211

Source documentation

A single positive mesh works simultaneously for a finite collection of continuous simplices, as required for a finite singular chain.

theorem finite_continuousMaps_cover_mesh {ι : Type} (F : Finset ι) (σ : ι → C(P, X))
    (U V : Set X) (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) :
    ∃ δ > 0, ∀ i ∈ F, ∀ s : Set P, (∀ a ∈ s, ∀ b ∈ s, dist a b < δ) →
      (∀ a ∈ s, σ i a ∈ U) ∨ (∀ a ∈ s, σ i a ∈ V) := by
…

theorem OAI.Kaplansky.finite_continuousMaps_eventually_small line 229

Source documentation

Geometric decay of mesh supplies one subdivision depth for an entire finite chain. This proves the compactness/limit step; construction of a subdivision chain operator with this bound remains separate.

theorem finite_continuousMaps_eventually_small {ι : Type} (F : Finset ι)
    (σ : ι → C(P, X)) (U V : Set X) (hU : IsOpen U) (hV : IsOpen V)
    (hUV : U ∪ V = Set.univ) (L c : ℝ) (hc₀ : 0 ≤ c) (hc₁ : c < 1) :
    ∃ N : ℕ, ∀ k ≥ N, ∀ i ∈ F, ∀ s : Set P,
      (∀ a ∈ s, ∀ b ∈ s, dist a b ≤ L * c ^ k) →
      (∀ a ∈ s, σ i a ∈ U) ∨ (∀ a ∈ s, σ i a ∈ V) := by
…

instance OAI.Kaplansky.standardSimplexMetricSpace line 245

theorem OAI.Kaplansky.singularSimplices_cover_mesh line 252

Source documentation

The finite mesh estimate applies to the actual standard-simplex coordinates of the library's singular simplices.

theorem singularSimplices_cover_mesh (n : ℕ)
    (F : Finset ((TopCat.toSSet.obj (TopCat.of X)).obj (Opposite.op ⦋n⦌)))
    (U V : Set X) (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) :
    ∃ δ > 0, ∀ σ ∈ F, ∀ s : Set (Convexity.StdSimplex ℝ (Fin (n+1))),
      (∀ a ∈ s, ∀ b ∈ s, dist a b < δ) →
      (∀ a ∈ s, TopCat.toSSetObjEquiv (TopCat.of X) (Opposite.op ⦋n⦌) σ a ∈ U) ∨
      (∀ a ∈ s, TopCat.toSSetObjEquiv (TopCat.of X) (Opposite.op ⦋n⦌) σ a ∈ V) :=
…