theorem toFreeAbelianGroup_eq_sum {Y : Type u_1} (f : Y →₀ ℤ) : Finsupp.toFreeAbelianGroup f = f.sum fun (x : Y) (n : ℤ) => n • FreeAbelianGroup.of x

The image of a Finsupp under Finsupp.toFreeAbelianGroup is the finite sum of the generators weighted by the corresponding integer coefficients.

theorem freeAbelianGroup_eq_sum {Y : Type u_1} (c : FreeAbelianGroup Y) : c = (FreeAbelianGroup.toFinsupp c).sum fun (x : Y) (n : ℤ) => n • FreeAbelianGroup.of x

Any element of a free abelian group can be written as the finite sum of its generators weighted by the integer coefficients given by its associated Finsupp.

theorem lift_eq_finsupp_sum {Y : Type u_1} {Z : Type u_2} [AddCommGroup Z] (f : Y → Z) (c : FreeAbelianGroup Y) : (FreeAbelianGroup.lift f) c = (FreeAbelianGroup.toFinsupp c).sum fun (x : Y) (n : ℤ) => n • f x

The lift of f : Y → Z along FreeAbelianGroup.lift evaluated at c equals the finite sum, over the support of c, of f applied to each generator scaled by its integer coefficient.

theorem support_finset_sum {Y : Type u_1} {Z : Type u_2} (s : Finset Y) (f : Y → FreeAbelianGroup Z) : (∑ i ∈ s, f i).support ⊆ s.biUnion fun (i : Y) => (f i).support

The support of a finite sum of free-abelian-group elements is contained in the union of the supports of the summands.

theorem support_lift_subset {Y : Type u_1} {Z : Type u_2} (f : Y → FreeAbelianGroup Z) (c : FreeAbelianGroup Y) : ((FreeAbelianGroup.lift f) c).support ⊆ c.support.biUnion fun (x : Y) => (f x).support

The support of FreeAbelianGroup.lift f c is contained in the union over the support of c of the supports of f x.

theorem lift_support_forall {Y : Type u_1} {Z : Type u_2} (f : Y → FreeAbelianGroup Z) (c : FreeAbelianGroup Y) (P : Z → Prop) (hP : ∀ x ∈ c.support, ∀ y ∈ (f x).support, P y) (y : Z) : y ∈ ((FreeAbelianGroup.lift f) c).support → P y

If a property P holds on the supports of f x for every x in the support of c, then it holds on the support of FreeAbelianGroup.lift f c.

noncomputable def AlgebraicTopologyI.barySubdivVertex (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (k i : Fin (n + 1)) : ℝ

The i-th barycentric coordinate of the k-th vertex of the simplex of the standard barycentric subdivision associated to the permutation π. It is 1/(k+1) when i is in the image under π of {0, …, k}, and 0 otherwise.

noncomputable def AlgebraicTopologyI.barySubdivMapFn (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (t : Fin (n + 1) → ℝ) (i : Fin (n + 1)) : ℝ

The underlying function of the barycentric subdivision map associated to a permutation π: it sends a barycentric coordinate vector t to the affine combination of the barycentric subdivision vertices weighted by t.

theorem AlgebraicTopologyI.barySubdivVertex_nonneg (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (k i : Fin (n + 1)) : 0 ≤ barySubdivVertex n π k i

The barycentric subdivision vertex coordinates are nonnegative.

theorem AlgebraicTopologyI.barySubdivVertex_sum (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (k : Fin (n + 1)) : ∑ i : Fin (n + 1), barySubdivVertex n π k i = 1

The barycentric coordinates of any vertex of the barycentric subdivision sum to one, exhibiting it as a point of the standard simplex.

theorem AlgebraicTopologyI.barySubdivMapFn_mem (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (t : Fin (n + 1) → ℝ) (ht : t ∈ stdSimplex ℝ (Fin (n + 1))) : barySubdivMapFn n π t ∈ stdSimplex ℝ (Fin (n + 1))

The barycentric subdivision map sends a point of the standard simplex to a point of the standard simplex.

theorem AlgebraicTopologyI.barySubdivMap_continuous (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : Continuous fun (t : ↑(stdSimplex ℝ (Fin (n + 1)))) => ⟨barySubdivMapFn n π ↑t, ⋯⟩

The barycentric subdivision map is continuous, as a self-map of the standard simplex.

noncomputable def AlgebraicTopologyI.barySubdivSimplex (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : SingularSimplex n ↑(stdSimplex ℝ (Fin (n + 1)))

The singular n-simplex on the standard n-simplex associated to a permutation π of {0,…,n}, given by the barycentric subdivision construction.

noncomputable def AlgebraicTopologyI.stdSubdivisionChain (n : ℕ) : SingularChains n ↑(stdSimplex ℝ (Fin (n + 1)))

The standard subdivision chain on the standard n-simplex, defined as the signed sum over permutations π of Fin (n+1) of the barycentric subdivision simplices, with sign given by Equiv.Perm.sign π.

noncomputable def AlgebraicTopologyI.subdivisionOp (n : ℕ) (X : Type u_2) [TopologicalSpace X] : SingularChains n X →+ SingularChains n X

The subdivision operator $ : S_n(X) → S_n(X), defined on a singular simplex σ as the image of the standard subdivision chain under σ, and extended additively.

noncomputable def AlgebraicTopologyI.iterateSubdivision {X : Type u_1} [TopologicalSpace X] {n : ℕ} (k : ℕ) (c : SingularChains n X) : SingularChains n X

The k-fold iterate $^k c of the subdivision operator applied to a chain c.

noncomputable def AlgebraicTopologyI.supportOfChain {X : Type u_1} [TopologicalSpace X] {n : ℕ} (c : SingularChains n X) : Finset (SingularSimplex n X)

The (finite) set of singular simplices that appear with nonzero coefficient in the chain c.

def AlgebraicTopologyI.IsSmallChain {X : Type u_1} [TopologicalSpace X] (𝒜 : Set (Set X)) {n : ℕ} (c : SingularChains n X) : Prop

A chain is 𝒜-small if every singular simplex appearing in its support is 𝒜-small (i.e. has image contained in some member of 𝒜).

theorem AlgebraicTopologyI.isSmallChain_zero {X : Type u_1} [TopologicalSpace X] (𝒜 : Set (Set X)) (n : ℕ) : IsSmallChain 𝒜 0

The zero chain is vacuously 𝒜-small.

theorem AlgebraicTopologyI.isSmallChain_add {X : Type u_1} [TopologicalSpace X] {𝒜 : Set (Set X)} {n : ℕ} {a b : SingularChains n X} (ha : IsSmallChain 𝒜 a) (hb : IsSmallChain 𝒜 b) : IsSmallChain 𝒜 (a + b)

The sum of two 𝒜-small chains is 𝒜-small.

theorem AlgebraicTopologyI.iterateSubdivision_add {X : Type u_1} [TopologicalSpace X] {n : ℕ} (k : ℕ) (a b : SingularChains n X) : iterateSubdivision k (a + b) = iterateSubdivision k a + iterateSubdivision k b

The iterated subdivision operator is additive.

theorem AlgebraicTopologyI.range_subset_of_mem_support_map {Y : Type u_2} {Z : Type u_3} [TopologicalSpace Y] [TopologicalSpace Z] {n : ℕ} (σ : C(Y, Z)) (c : SingularChains n Y) (τ : SingularSimplex n Z) (hτ : τ ∈ FreeAbelianGroup.support ((SingularChains.map σ) c)) : Set.range (have this := τ; ⇑this) ⊆ Set.range ⇑σ

Every singular simplex appearing in the support of SingularChains.map σ c has image contained in the range of σ.

theorem AlgebraicTopologyI.isSmallChain_subdivisionOp {X : Type u_1} [TopologicalSpace X] {𝒜 : Set (Set X)} {n : ℕ} {c : SingularChains n X} (h : IsSmallChain 𝒜 c) : IsSmallChain 𝒜 ((subdivisionOp n X) c)

The subdivision operator preserves 𝒜-smallness: if c is 𝒜-small then so is $c.

theorem AlgebraicTopologyI.isSmallChain_iterateSubdivision_succ {X : Type u_1} [TopologicalSpace X] {𝒜 : Set (Set X)} {n : ℕ} {c : SingularChains n X} {k : ℕ} (h : IsSmallChain 𝒜 (iterateSubdivision k c)) : IsSmallChain 𝒜 (iterateSubdivision (k + 1) c)

If the k-th iterate of the subdivision operator applied to c is 𝒜-small, then so is the (k+1)-th iterate.

theorem AlgebraicTopologyI.isSmallChain_iterateSubdivision_mono {X : Type u_1} [TopologicalSpace X] {𝒜 : Set (Set X)} {n : ℕ} {c : SingularChains n X} {k : ℕ} (h : IsSmallChain 𝒜 (iterateSubdivision k c)) (j : ℕ) : IsSmallChain 𝒜 (iterateSubdivision (k + j) c)

Monotonicity: once an iterate of the subdivision operator applied to c is 𝒜-small, all subsequent iterates remain 𝒜-small.

theorem AlgebraicTopologyI.diam_iterateSubdivision_le (n k : ℕ) (τ : SingularSimplex n ↑(stdSimplex ℝ (Fin (n + 1)))) : τ ∈ supportOfChain (iterateSubdivision k (FreeAbelianGroup.of (ContinuousMap.id ↑(stdSimplex ℝ (Fin (n + 1)))))) → Metric.diam (Set.range (have this := τ; ⇑this)) ≤ (↑n / (↑n + 1)) ^ k

Diameter shrinkage: every simplex appearing in the k-fold subdivision of the identity simplex on Δⁿ has image of diameter at most (n/(n+1))^k.

theorem AlgebraicTopologyI.subdiv_diam_eventually_small (n : ℕ) (ε : ℝ) (hε : 0 < ε) : ∃ (k : ℕ), ∀ τ ∈ supportOfChain (iterateSubdivision k (FreeAbelianGroup.of (ContinuousMap.id ↑(stdSimplex ℝ (Fin (n + 1)))))), Metric.diam (Set.range (have this := τ; ⇑this)) < ε

For any ε > 0, some iterate of the subdivision operator applied to the identity simplex on Δⁿ consists of simplices each of which has image of diameter less than ε.

theorem AlgebraicTopologyI.subdiv_eventually_refines_open_cover (n : ℕ) (𝒰 : Set (Set ↑(stdSimplex ℝ (Fin (n + 1))))) (h𝒰_open : ∀ U ∈ 𝒰, IsOpen U) (h𝒰_cover : Set.univ ⊆ ⋃₀ 𝒰) : ∃ (k : ℕ), ∀ τ ∈ supportOfChain (iterateSubdivision k (FreeAbelianGroup.of (ContinuousMap.id ↑(stdSimplex ℝ (Fin (n + 1)))))), ∃ U ∈ 𝒰, Set.range (have this := τ; ⇑this) ⊆ U

Combining diameter shrinkage with the Lebesgue covering lemma: for any open cover 𝒰 of the standard simplex, some iterate of the subdivision operator applied to the identity simplex consists of simplices each of which is contained in some U ∈ 𝒰.

theorem AlgebraicTopologyI.SingularChains.map_comp' {n : ℕ} {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] (f : C(Y, Z)) (g : C(X, Y)) (s : SingularChains n X) : (map (f.comp g)) s = (map f) ((map g) s)

Functoriality of SingularChains.map: the chain-level map associated to a composition of continuous maps is the composition of the chain-level maps.

theorem AlgebraicTopologyI.subdivisionOp_map_comm (n : ℕ) {Y : Type u_2} {X : Type u_3} [TopologicalSpace Y] [TopologicalSpace X] (f : C(Y, X)) (c : SingularChains n Y) : (subdivisionOp n X) ((SingularChains.map f) c) = (SingularChains.map f) ((subdivisionOp n Y) c)

Naturality of the subdivision operator with respect to continuous maps: $ commutes with SingularChains.map f.

theorem AlgebraicTopologyI.subdivisionOp_naturality (n : ℕ) {X : Type u_2} [TopologicalSpace X] (σ : SingularSimplex n X) (k : ℕ) : iterateSubdivision k (FreeAbelianGroup.of σ) = (SingularChains.map (have this := σ; this)) (iterateSubdivision k (FreeAbelianGroup.of (ContinuousMap.id ↑(stdSimplex ℝ (Fin (n + 1))))))

Iterated naturality: the k-fold subdivision of a singular simplex σ equals the pushforward under σ of the k-fold subdivision of the identity simplex on Δⁿ.

theorem AlgebraicTopologyI.iterateSubdivision_eventually_small_pullback (n : ℕ) {X : Type u_2} [TopologicalSpace X] (σ : SingularSimplex n X) (𝒜 : Set (Set X)) (h𝒜 : IsCover 𝒜) : ∃ (k : ℕ), IsSmallChain 𝒜 (iterateSubdivision k (FreeAbelianGroup.of σ))

Single-simplex form of Lemma 13.2: for a cover 𝒜 of X and any singular simplex σ, some iterate of the subdivision operator sends σ to an 𝒜-small chain.

theorem AlgebraicTopologyI.exists_isSmallChain_iterateSubdivision_of_simplex {X : Type u_2} [TopologicalSpace X] {𝒜 : Set (Set X)} (h𝒜 : IsCover 𝒜) {n : ℕ} (σ : SingularSimplex n X) : ∃ (k : ℕ), IsSmallChain 𝒜 (iterateSubdivision k (FreeAbelianGroup.of σ))

Convenience restatement of iterateSubdivision_eventually_small_pullback.

theorem AlgebraicTopologyI.exists_iterateSubdivision_isSmallChain {X : Type u_2} [TopologicalSpace X] {A : Set (Set X)} (hA : IsCover A) {n : ℕ} (c : SingularChains n X) : ∃ (k : ℕ), IsSmallChain A (iterateSubdivision k c)

Lemma 13.2 of Miller's Algebraic Topology I: for any cover 𝒜 of a space X and any singular chain c, some iterate of the subdivision operator sends c to an 𝒜-small chain.