Smallness.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

Eventual smallness of generators and chains and comparison on homology.

theorem OAI.Kaplansky.singularGen_eventually_small line 20

Source documentation

Every actual singular simplex becomes a chain of small simplices after sufficiently many applications of the constructed subdivision operator.

theorem singularGen_eventually_small (hU : IsOpen U) (hV : IsOpen V)
    (hUV : U ∪ V = Set.univ) {n : ℕ}
    (σ : (TopCat.toSSet.obj (TopCat.of X)) _⦋n⦌) :
    ∃ N : ℕ, ∀ k ≥ N, (singularSubdivisionMap (TopCat.of X) n)^[k]
      (singularGen σ (1 : ℤ)) ∈ LinearMap.range ((smallSingularChainInclusion U V).f n).hom := by
…

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

theorem OAI.Kaplansky.singularChain_submodule_eq_top line 61
Source documentation
Every singular chain is generated by finitely many integral simplex generators. This uses the actual coproduct universal property, with no support premise.
```
theorem singularChain_submodule_eq_top {X : TopCat.{0}} (n : ℕ)
    (S : Submodule ℤ ((integralSingularChains.obj X).X n))
    (hS : ∀ σ : (TopCat.toSSet.obj X) _⦋n⦌, singularGen σ (1 : ℤ) ∈ S) : S = ⊤ := by
…
```
Mentions: OAI.Kaplansky.singularGen
def OAI.Kaplansky.eventuallySmallChains line 82
Source documentation
Chains whose iterated subdivisions eventually lie in the actual image of the small-chain inclusion.
```
def eventuallySmallChains (n : ℕ) : Submodule ℤ ((integralSingularChains.obj (TopCat.of X)).X n) where
…
```

theorem OAI.Kaplansky.singularChain_eventually_small line 106

Source documentation

The actual open-cover smallness theorem for every finite singular chain.

theorem singularChain_eventually_small (hU : IsOpen U) (hV : IsOpen V)
    (hUV : U ∪ V = Set.univ) (n : ℕ)
    (a : (integralSingularChains.obj (TopCat.of X)).X n) :
    ∃ N : ℕ, ∀ k ≥ N, (singularSubdivisionMap (TopCat.of X) n)^[k] a ∈
      LinearMap.range ((smallSingularChainInclusion U V).f n).hom := by
…

Mentions: OAI.Kaplansky.singularSubdivisionMap, OAI.Kaplansky.smallSingularChainInclusion

theorem OAI.Kaplansky.chainNext_nat line 122

def OAI.Kaplansky.chainCycle line 126

Source documentation

An actual cycle represented by its underlying chain.

def chainCycle (K : ChainComplex (ModuleCat.{0} ℤ) ℕ) (n : ℕ)
    (a : K.X n) (ha : K.d n (n-1) a = 0) : K.cycles n :=
…

theorem OAI.Kaplansky.chainCycle_i line 133
theorem OAI.Kaplansky.chain_cycle_boundary_zero line 140

theorem OAI.Kaplansky.chain_homologyπ_eq_zero_iff line 145

Source documentation

A homology class is zero exactly when its representative cycle is a boundary.

theorem chain_homologyπ_eq_zero_iff (K : ChainComplex (ModuleCat.{0} ℤ) ℕ) (n : ℕ)
    (z : K.cycles n) : K.homologyπ n z = 0 ↔
      ∃ b : K.X (n+1), K.d (n+1) n b = K.iCycles n z := by
…

theorem OAI.Kaplansky.chain_cyclesMap_i line 159
theorem OAI.Kaplansky.chain_homologyMap_π line 165

def OAI.Kaplansky.chainIterate line 171

Source documentation

Iterates of an actual chain endomorphism.

def chainIterate {K : ChainComplex (ModuleCat.{0} ℤ) ℕ} (s : K ⟶ K) : ℕ → (K ⟶ K)
  | 0 => 𝟙 _
  | k+1 => chainIterate s k ≫ s

@[simp]

theorem OAI.Kaplansky.chainIterate_f_apply line 176
theorem OAI.Kaplansky.chainIterate_homologyMap line 184
theorem OAI.Kaplansky.chainIterate_commute line 191

theorem OAI.Kaplansky.quasiIso_of_eventual_image line 206

Source documentation

A monomorphic chain comparison is a quasi-isomorphism if compatible endomorphisms induce the identity on homology and eventually carry every chain into its image. All premises are discharged by subdivision below.

theorem quasiIso_of_eventual_image
    {P Q : ChainComplex (ModuleCat.{0} ℤ) ℕ} (f : P ⟶ Q) [Mono f]
    (s : P ⟶ P) (t : Q ⟶ Q) (hcomm : s ≫ f = f ≫ t)
    (hs : ∀ n, homologyMap s n = 𝟙 _) (ht : ∀ n, homologyMap t n = 𝟙 _)
    (hevent : ∀ n (a : Q.X n), ∃ k, (chainIterate t k).f n a ∈ LinearMap.range (f.f n).hom) :
    QuasiIso f := by
…

Mentions: OAI.Kaplansky.chainIterate

theorem OAI.Kaplansky.smallSingularChainInclusion_quasiIso line 256
Source documentation
The two-set open-cover theorem for the actual integral singular chain complex: the inclusion of small chains is a quasi-isomorphism.
```
theorem smallSingularChainInclusion_quasiIso {X : Type} [TopologicalSpace X]
    (U V : Set X) (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) :
    QuasiIso (smallSingularChainInclusion U V) := by
…
```
Mentions: OAI.Kaplansky.smallSingularChainInclusion