Affine chains in convex spaces

An affine k-chain in a convex space E is a formal integral combination of (k + 1)-tuples of points of E, the vertex tuples of affine k-simplices. This file equips affine chains with the simplicial boundary, the push-forward along maps, the cone from a point and the barycentric subdivision, and pushes affine chains of the standard simplex Δᵐ forward along a singular m-simplex to singular chains with coefficients in an object of a preadditive category.

These are the linear chains of Hatcher's proof of excision: operators on singular chains, such as the prism operator of barycentric subdivision, are defined on the standard simplex as affine chains and transported to singular chains along singular simplices.

Main definitions and results

• TauCeti.AffineChain.boundary: the boundary of affine chains, with TauCeti.AffineChain.boundary_boundary: ∂ ∂ = 0.
• TauCeti.AffineChain.map: the push-forward along a map of vertices.
• TauCeti.AffineChain.cone: the cone from a point b, with TauCeti.AffineChain.boundary_cone: ∂ (b · c) = c - b · ∂ c in positive degrees.
• TauCeti.AffineChain.subdivision: the barycentric subdivision, which commutes with the boundary (TauCeti.AffineChain.boundary_subdivision) and with affine maps (TauCeti.AffineChain.map_subdivision).
• TauCeti.AffineChain.singularChain: the push-forward of affine chains of Δᵐ along a singular m-simplex, compatible with the boundary, faces, subdivision and continuous maps.
• TauCeti.AffineChain.singularChain_subdivision: pushing forward commutes with subdivision.
• TauCeti.AffineChain.singularChain_subdivision_iterate: pushing forward commutes with iterated subdivision.

References

• A. Hatcher, Algebraic Topology, Section 2.1, proof of Proposition 2.21, step (1).

noncomputable def TauCeti.AffineChain.boundary (E : Type u_1) (k : ℕ) : ((Fin (k + 2) → E) →₀ ℤ) →ₗ[ℤ] (Fin (k + 1) → E) →₀ ℤ

The simplicial boundary of formal integral combinations of (k + 1)-tuples of vertices: the alternating sum of the tuples obtained by deleting one vertex.

Equations

• TauCeti.AffineChain.boundary E k = Finsupp.linearCombination ℤ fun (v : Fin (k + 2) → E) => ∑ i : Fin (k + 2), Finsupp.single (v ∘ i.succAbove) ((-1) ^ ↑i)

@[simp]

theorem TauCeti.AffineChain.boundary_single {E : Type u_1} {k : ℕ} (v : Fin (k + 2) → E) (a : ℤ) : (boundary E k) (Finsupp.single v a) = ∑ i : Fin (k + 2), Finsupp.single (v ∘ i.succAbove) (a * (-1) ^ ↑i)

theorem TauCeti.AffineChain.boundary_boundary {E : Type u_1} (k : ℕ) : boundary E k ∘ₗ boundary E (k + 1) = 0

The boundary of a boundary vanishes.

noncomputable def TauCeti.AffineChain.map {E : Type u_1} {F : Type u_2} (f : E → F) (k : ℕ) : ((Fin (k + 1) → E) →₀ ℤ) →ₗ[ℤ] (Fin (k + 1) → F) →₀ ℤ

The vertex tuples pushed forward along a map f : E → F.

Equations

• TauCeti.AffineChain.map f k = Finsupp.lmapDomain ℤ ℤ fun (x : Fin (k + 1) → E) => f ∘ x

@[simp]

theorem TauCeti.AffineChain.map_single {E : Type u_1} {F : Type u_2} (f : E → F) {k : ℕ} (v : Fin (k + 1) → E) (a : ℤ) : (map f k) (Finsupp.single v a) = Finsupp.single (f ∘ v) a

theorem TauCeti.AffineChain.map_comp {E : Type u_1} {F : Type u_2} {G : Type u_3} (g : F → G) (f : E → F) (k : ℕ) : map (g ∘ f) k = map g k ∘ₗ map f k

@[simp]

theorem TauCeti.AffineChain.map_id {E : Type u_1} (k : ℕ) : map id k = LinearMap.id

theorem TauCeti.AffineChain.map_boundary {E : Type u_1} {F : Type u_2} (f : E → F) {k : ℕ} (c : (Fin (k + 2) → E) →₀ ℤ) : (map f k) ((boundary E k) c) = (boundary F k) ((map f (k + 1)) c)

noncomputable def TauCeti.AffineChain.cone {E : Type u_1} (b : E) (k : ℕ) : ((Fin (k + 1) → E) →₀ ℤ) →ₗ[ℤ] (Fin (k + 2) → E) →₀ ℤ

The cone from a vertex b: the vertex b is put in front of every vertex tuple.

Equations

• TauCeti.AffineChain.cone b k = Finsupp.lmapDomain ℤ ℤ fun (v : Fin (k + 1) → E) => Fin.cons b v

@[simp]

theorem TauCeti.AffineChain.cone_single {E : Type u_1} (b : E) {k : ℕ} (v : Fin (k + 1) → E) (a : ℤ) : (cone b k) (Finsupp.single v a) = Finsupp.single (Fin.cons b v) a

theorem TauCeti.AffineChain.boundary_cone {E : Type u_1} (b : E) (k : ℕ) (c : (Fin (k + 2) → E) →₀ ℤ) : (boundary E (k + 1)) ((cone b (k + 1)) c) = c - (cone b k) ((boundary E k) c)

The boundary of a cone of a chain of positive degree is the chain minus the cone of its boundary.

noncomputable def TauCeti.AffineChain.subdivision (E : Type u_1) [Convexity.ConvexSpace ℝ E] (k : ℕ) : ((Fin (k + 1) → E) →₀ ℤ) →ₗ[ℤ] (Fin (k + 1) → E) →₀ ℤ

The barycentric subdivision of chains of vertex tuples in a convex space: the tuple v is replaced by the signed sum, over the permutations π, of the vertex tuples of the affine simplices StdSimplex.affineMapMk v ∘ BarycentricSubdivision.vertex π.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.AffineChain.subdivision_single {E : Type u_1} [Convexity.ConvexSpace ℝ E] {k : ℕ} (v : Fin (k + 1) → E) (a : ℤ) : (subdivision E k) (Finsupp.single v a) = ∑ π : Equiv.Perm (Fin (k + 1)), Finsupp.single (⇑(Convexity.StdSimplex.affineMapMk v) ∘ BarycentricSubdivision.vertex π) (a * ↑(Equiv.Perm.sign π))

@[simp]

theorem TauCeti.AffineChain.subdivision_zero {E : Type u_1} [Convexity.ConvexSpace ℝ E] : subdivision E 0 = LinearMap.id

The subdivision of 0-chains is the identity.

theorem TauCeti.AffineChain.boundary_subdivision {E : Type u_1} [Convexity.ConvexSpace ℝ E] (k : ℕ) : boundary E k ∘ₗ subdivision E (k + 1) = subdivision E k ∘ₗ boundary E k

The subdivision commutes with the boundary.

theorem TauCeti.AffineChain.map_subdivision {E : Type u_1} {F : Type u_2} [Convexity.ConvexSpace ℝ E] [Convexity.ConvexSpace ℝ F] (f : Convexity.ConvexSpace.AffineMap ℝ E F) {k : ℕ} (c : (Fin (k + 1) → E) →₀ ℤ) : (map (⇑f) k) ((subdivision E k) c) = (subdivision F k) ((map (⇑f) k) c)

The subdivision is natural under affine maps.

noncomputable def TauCeti.AffineChain.simplex (k : ℕ) : (Fin (k + 1) → Convexity.StdSimplex ℝ (Fin (k + 1))) →₀ ℤ

The vertex tuple of the standard k-simplex, as an affine k-chain of the standard k-simplex.

Equations

• TauCeti.AffineChain.simplex k = Finsupp.single Convexity.StdSimplex.single 1

theorem TauCeti.AffineChain.simplex_def (k : ℕ) : simplex k = Finsupp.single Convexity.StdSimplex.single 1

theorem TauCeti.AffineChain.map_affineMapMk_simplex {E : Type u_1} [Convexity.ConvexSpace ℝ E] {k : ℕ} (v : Fin (k + 1) → E) : (map (⇑(Convexity.StdSimplex.affineMapMk v)) k) (simplex k) = Finsupp.single v 1

noncomputable def TauCeti.AffineChain.singularChain {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] (R : C) {X : TopCat} {m : ℕ} (σ : C(Convexity.StdSimplex ℝ (Fin (m + 1)), ↑X)) (k : ℕ) : ((Fin (k + 1) → Convexity.StdSimplex ℝ (Fin (m + 1))) →₀ ℤ) →ₗ[ℤ] R ⟶ ((TopCat.toSSet.obj X).chainComplex R).X k

The singular chains with coefficients in R of the affine chains of Δᵐ pushed forward along a singular simplex σ : Δᵐ → X: a vertex tuple v is sent to the summand of the singular simplex σ ∘ StdSimplex.continuousAffineMapMk v.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.AffineChain.singularChain_single {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] {R : C} {X : TopCat} {m : ℕ} (σ : C(Convexity.StdSimplex ℝ (Fin (m + 1)), ↑X)) {k : ℕ} (v : Fin (k + 1) → Convexity.StdSimplex ℝ (Fin (m + 1))) (a : ℤ) : (singularChain R σ k) (Finsupp.single v a) = a • (TopCat.toSSet.obj X).ιChainComplex ((X.toSSetObjEquiv (Opposite.op { len := k })).symm (σ.comp (Convexity.StdSimplex.continuousAffineMapMk v)))

theorem TauCeti.AffineChain.singularChain_boundary {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] {R : C} {X : TopCat} {m : ℕ} (σ : C(Convexity.StdSimplex ℝ (Fin (m + 1)), ↑X)) {k : ℕ} (c : (Fin (k + 2) → Convexity.StdSimplex ℝ (Fin (m + 1))) →₀ ℤ) : (singularChain R σ k) ((boundary (Convexity.StdSimplex ℝ (Fin (m + 1))) k) c) = CategoryTheory.CategoryStruct.comp ((singularChain R σ (k + 1)) c) (((TopCat.toSSet.obj X).chainComplex R).d (k + 1) k)

Pushing affine chains forward along a singular simplex commutes with the boundary.

theorem TauCeti.AffineChain.singularChain_δ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] {R : C} {X : TopCat} {m : ℕ} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := m + 1 })) (j : Fin (m + 2)) {k : ℕ} (c : (Fin (k + 1) → Convexity.StdSimplex ℝ (Fin (m + 1))) →₀ ℤ) : (singularChain R ((X.toSSetObjEquiv (Opposite.op { len := m })) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (TopCat.toSSet.obj X) j)) σ)) k) c = (singularChain R ((X.toSSetObjEquiv (Opposite.op { len := m + 1 })) σ) k) ((map (Convexity.StdSimplex.map j.succAbove) k) c)

Pushing an affine chain forward along a facet of a singular simplex is pushing its image under the facet inclusion forward along the singular simplex.

theorem TauCeti.AffineChain.singularChain_simplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] {R : C} {X : TopCat} {n : ℕ} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) : (singularChain R ((X.toSSetObjEquiv (Opposite.op { len := n })) σ) n) (simplex n) = (TopCat.toSSet.obj X).ιChainComplex σ

Pushing the standard simplex forward along a singular simplex gives that singular simplex.

theorem TauCeti.AffineChain.singularChain_subdivision {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] {R : C} {X : TopCat} {m : ℕ} (σ : C(Convexity.StdSimplex ℝ (Fin (m + 1)), ↑X)) {k : ℕ} (c : (Fin (k + 1) → Convexity.StdSimplex ℝ (Fin (m + 1))) →₀ ℤ) : (singularChain R σ k) ((subdivision (Convexity.StdSimplex ℝ (Fin (m + 1))) k) c) = CategoryTheory.CategoryStruct.comp ((singularChain R σ k) c) (singularSubdivisionX R X k)

Pushing the subdivision of an affine chain forward along a singular simplex gives the barycentric subdivision of the pushed-forward chain.

theorem TauCeti.AffineChain.singularChain_subdivision_iterate {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] {R : C} {X : TopCat} {m k n : ℕ} (σ : C(Convexity.StdSimplex ℝ (Fin (m + 1)), ↑X)) (c : (Fin (k + 1) → Convexity.StdSimplex ℝ (Fin (m + 1))) →₀ ℤ) : (singularChain R σ k) ((⇑(subdivision (Convexity.StdSimplex ℝ (Fin (m + 1))) k))^[n] c) = CategoryTheory.CategoryStruct.comp ((singularChain R σ k) c) ((CategoryTheory.End.of (singularSubdivisionChainMap R X) ^ n).f k)

Pushing an iterated barycentric subdivision of an affine chain forward along a singular simplex is the corresponding iterate of the singular subdivision operator.

theorem TauCeti.AffineChain.singularChain_subdivision_simplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] {R : C} {X : TopCat} {n : ℕ} (σ : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) : (singularChain R ((X.toSSetObjEquiv (Opposite.op { len := n })) σ) n) ((subdivision (Convexity.StdSimplex ℝ (Fin ((Opposite.unop (Opposite.op { len := n })).len + 1))) n) (simplex n)) = CategoryTheory.CategoryStruct.comp ((TopCat.toSSet.obj X).ιChainComplex σ) (singularSubdivisionX R X n)

Pushing the subdivision of the standard simplex forward along a singular simplex gives the barycentric subdivision of that singular simplex.

theorem TauCeti.AffineChain.singularChain_comp_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasCoproducts C] {R : C} {X Y : TopCat} {m : ℕ} (σ : C(Convexity.StdSimplex ℝ (Fin (m + 1)), ↑X)) (f : X ⟶ Y) {k : ℕ} (c : (Fin (k + 1) → Convexity.StdSimplex ℝ (Fin (m + 1))) →₀ ℤ) : CategoryTheory.CategoryStruct.comp ((singularChain R σ k) c) ((SSet.chainComplexMap (TopCat.toSSet.map f) R).f k) = (singularChain R ((CategoryTheory.ConcreteCategory.hom f).comp σ) k) c

Pushing affine chains forward along a singular simplex commutes with continuous maps.