Barycentric Subdivision Cone

1. The normalized tail of a point of Δᵏ⁺¹

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.coneTailFun {k : ℕ} (x : ↑(Delta (k + 1))) : Fin (k + 1) → ℝ

Normalize the non-apex barycentric coordinates by their total mass.

Equations

• SphereOddDegree.AffineBarycentricSubdivision.coneTailFun x i = x i.succ / (1 - x 0)

theorem SphereOddDegree.AffineBarycentricSubdivision.coneTailFun_mem {k : ℕ} (x : ↑(Delta (k + 1))) (hx : x 0 ≠ 1) : coneTailFun x ∈ finiteSimplex ℝ (Fin (k + 1))

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.coneTail {k : ℕ} (x : ↑(Delta (k + 1))) : ↑(Delta k)

The normalized base point of a cone simplex, choosing the first vertex at the apex.

Equations

• SphereOddDegree.AffineBarycentricSubdivision.coneTail x = if h : x 0 = 1 then SphereOddDegree.FiniteSimplex.vertex 0 else ⟨SphereOddDegree.AffineBarycentricSubdivision.coneTailFun x, ⋯⟩

theorem SphereOddDegree.AffineBarycentricSubdivision.coneTail_apply {k : ℕ} (x : ↑(Delta (k + 1))) (hx : x 0 ≠ 1) (i : Fin (k + 1)) : (coneTail x) i = x i.succ / (1 - x 0)

2. The affine cone map

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.affineConeMapFun {n k : ℕ} (v : ↑(Delta n)) (τ : ↑(Delta k) → ↑(Delta n)) (x : ↑(Delta (k + 1))) : Fin (n + 1) → ℝ

Barycentric coordinates of the cone from a vertex over a simplex map.

Equations

• SphereOddDegree.AffineBarycentricSubdivision.affineConeMapFun v τ x j = x 0 * v j + (1 - x 0) * (τ (SphereOddDegree.AffineBarycentricSubdivision.coneTail x)) j

theorem SphereOddDegree.AffineBarycentricSubdivision.affineConeMapFun_mem {n k : ℕ} (v : ↑(Delta n)) (τ : ↑(Delta k) → ↑(Delta n)) (x : ↑(Delta (k + 1))) : affineConeMapFun v τ x ∈ finiteSimplex ℝ (Fin (n + 1))

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.affineConeMap {n k : ℕ} (v : ↑(Delta n)) (τ : ↑(Delta k) → ↑(Delta n)) : ↑(Delta (k + 1)) → ↑(Delta n)

The simplex map obtained by coning a given map to the chosen vertex.

Equations

• SphereOddDegree.AffineBarycentricSubdivision.affineConeMap v τ x = ⟨SphereOddDegree.AffineBarycentricSubdivision.affineConeMapFun v τ x, ⋯⟩

@[simp]

theorem SphereOddDegree.AffineBarycentricSubdivision.affineConeMap_coord {n k : ℕ} (v : ↑(Delta n)) (τ : ↑(Delta k) → ↑(Delta n)) (x : ↑(Delta (k + 1))) (j : Fin (n + 1)) : (affineConeMap v τ x) j = x 0 * v j + (1 - x 0) * (τ (coneTail x)) j

3. Vertex formulas

theorem SphereOddDegree.AffineBarycentricSubdivision.affineConeMap_vertex_zero {n k : ℕ} (v : ↑(Delta n)) (τ : ↑(Delta k) → ↑(Delta n)) : affineConeMap v τ (FiniteSimplex.vertex 0) = v

theorem SphereOddDegree.AffineBarycentricSubdivision.affineConeMap_vertex_succ {n k : ℕ} (v : ↑(Delta n)) (τ : ↑(Delta k) → ↑(Delta n)) (i : Fin (k + 1)) : affineConeMap v τ (FiniteSimplex.vertex i.succ) = τ (FiniteSimplex.vertex i)

4. Continuity and bundled continuous cone map

theorem SphereOddDegree.AffineBarycentricSubdivision.continuousOn_coneTail {k : ℕ} : ContinuousOn coneTail {x : ↑(Delta (k + 1)) | x 0 ≠ 1}

theorem SphereOddDegree.AffineBarycentricSubdivision.continuous_affineConeMap {n k : ℕ} (v : ↑(Delta n)) (τ : C(↑(Delta k), ↑(Delta n))) : Continuous (affineConeMap v ⇑τ)

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.affineConeContinuousMap {n k : ℕ} (v : ↑(Delta n)) (τ : C(↑(Delta k), ↑(Delta n))) : C(↑(Delta (k + 1)), ↑(Delta n))

The affine cone construction bundled as a continuous map.

Equations

• SphereOddDegree.AffineBarycentricSubdivision.affineConeContinuousMap v τ = { toFun := SphereOddDegree.AffineBarycentricSubdivision.affineConeMap v ⇑τ, continuous_toFun := ⋯ }

@[simp]

theorem SphereOddDegree.AffineBarycentricSubdivision.affineConeContinuousMap_apply {n k : ℕ} (v : ↑(Delta n)) (τ : C(↑(Delta k), ↑(Delta n))) (x : ↑(Delta (k + 1))) : (affineConeContinuousMap v τ) x = affineConeMap v (⇑τ) x

5. Face formulas

theorem SphereOddDegree.AffineBarycentricSubdivision.cone_face_zero {n k : ℕ} (v : ↑(Delta n)) (τ : ↑(Delta k) → ↑(Delta n)) : (fun (y : ↑(Delta k)) => affineConeMap v τ ((cofaceTop k 0) y)) = τ

theorem SphereOddDegree.AffineBarycentricSubdivision.coneTail_cofaceTop_succ {k : ℕ} (j : Fin (k + 1 + 1)) (y : ↑(Delta (k + 1))) (hy : y 0 ≠ 1) : coneTail ((cofaceTop (k + 1) j.succ) y) = (cofaceTop k j) (coneTail y)

theorem SphereOddDegree.AffineBarycentricSubdivision.cone_face_succ {n k : ℕ} (v : ↑(Delta n)) (τ : ↑(Delta (k + 1)) → ↑(Delta n)) (j : Fin (k + 1 + 1)) : (fun (y : ↑(Delta (k + 1))) => affineConeMap v τ ((cofaceTop (k + 1) j.succ) y)) = fun (y : ↑(Delta (k + 1))) => affineConeMap v (fun (z : ↑(Delta k)) => τ ((cofaceTop k j) z)) y

6. The cone on singular simplices and chains of Δⁿ

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.coneSimplex (n k : ℕ) (v : ↑(Delta n)) (σ : singularSimplices (↧↑(Delta n)) k) : singularSimplices (↧↑(Delta n)) (k + 1)

The singular simplex obtained by coning to a point of the standard simplex.

Equations

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

theorem SphereOddDegree.AffineBarycentricSubdivision.coneSimplex_continuousMap (n k : ℕ) (v : ↑(Delta n)) (σ : singularSimplices (↧↑(Delta n)) k) : singularSimplexAsContinuousMap (↧↑(Delta n)) (k + 1) (coneSimplex n k v σ) = affineConeContinuousMap v (singularSimplexAsContinuousMap (↧↑(Delta n)) k σ)

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.constSimplex0 (n : ℕ) (v : ↑(Delta n)) : singularSimplices (↧↑(Delta n)) 0

The constant singular zero-simplex at the chosen point.

Equations

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

@[simp]

theorem SphereOddDegree.AffineBarycentricSubdivision.constSimplex0_continuousMap (n : ℕ) (v : ↑(Delta n)) : singularSimplexAsContinuousMap (↧↑(Delta n)) 0 (constSimplex0 n v) = ContinuousMap.const (↑(Delta 0)) v

theorem SphereOddDegree.AffineBarycentricSubdivision.coneSimplex_face_zero (n k : ℕ) (v : ↑(Delta n)) (σ : singularSimplices (↧↑(Delta n)) k) : AlexanderWhitney.faceSimplex (↧↑(Delta n)) k 0 (coneSimplex n k v σ) = σ

theorem SphereOddDegree.AffineBarycentricSubdivision.coneSimplex_face_succ (n k : ℕ) (v : ↑(Delta n)) (σ : singularSimplices (↧↑(Delta n)) (k + 1)) (j : Fin (k + 1 + 1)) : AlexanderWhitney.faceSimplex (↧↑(Delta n)) (k + 1) j.succ (coneSimplex n (k + 1) v σ) = coneSimplex n k v (AlexanderWhitney.faceSimplex (↧↑(Delta n)) k j σ)

theorem SphereOddDegree.AffineBarycentricSubdivision.coneSimplex_face_one_zero (n : ℕ) (v : ↑(Delta n)) (σ : singularSimplices (↧↑(Delta n)) 0) : AlexanderWhitney.faceSimplex (↧↑(Delta n)) 0 1 (coneSimplex n 0 v σ) = constSimplex0 n v

7. The cone on chains

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.coneGenerator (R : Type) [CommRing R] (n k : ℕ) (v : ↑(Delta n)) (σ : singularSimplices (↧↑(Delta n)) k) : ↑(singularChainGroup R (↧↑(Delta n)) (k + 1))

The chain generator associated with the cone over a singular simplex.

Equations

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

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.coneGeneratorHom (R : Type) [CommRing R] (n k : ℕ) (v : ↑(Delta n)) (σ : singularSimplices (↧↑(Delta n)) k) : ↧R ⟶ singularChainGroup R (↧↑(Delta n)) (k + 1)

Send a coefficient to its scalar multiple of the coned simplex generator.

Equations

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

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.coneLinearMap (R : Type) [CommRing R] (n k : ℕ) (v : ↑(Delta n)) : singularChainGroup R (↧↑(Delta n)) k ⟶ singularChainGroup R (↧↑(Delta n)) (k + 1)

Extend coning on singular generators linearly to all chains.

Equations

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

theorem SphereOddDegree.AffineBarycentricSubdivision.coneLinearMap_generator (R : Type) [CommRing R] (n k : ℕ) (v : ↑(Delta n)) (σ : singularSimplices (↧↑(Delta n)) k) : (ModuleCat.Hom.hom (coneLinearMap R n k v)) (chainGenerator R (↧↑(Delta n)) k σ) = coneGenerator R n k v σ

8. The boundary formula

theorem SphereOddDegree.AffineBarycentricSubdivision.singularBoundary_coneGenerator_zero (R : Type) [CommRing R] (n : ℕ) (v : ↑(Delta n)) (σ : singularSimplices (↧↑(Delta n)) 0) : (ModuleCat.Hom.hom (singularBoundary R (↧↑(Delta n)) 0)) (coneGenerator R n 0 v σ) = chainGenerator R (↧↑(Delta n)) 0 σ - chainGenerator R (↧↑(Delta n)) 0 (constSimplex0 n v)

theorem SphereOddDegree.AffineBarycentricSubdivision.singularBoundary_coneGenerator_succ (R : Type) [CommRing R] (n m : ℕ) (v : ↑(Delta n)) (σ : singularSimplices (↧↑(Delta n)) (m + 1)) : (ModuleCat.Hom.hom (singularBoundary R (↧↑(Delta n)) (m + 1))) (coneGenerator R n (m + 1) v σ) = chainGenerator R (↧↑(Delta n)) (m + 1) σ - (ModuleCat.Hom.hom (coneLinearMap R n m v)) ((ModuleCat.Hom.hom (singularBoundary R (↧↑(Delta n)) m)) (chainGenerator R (↧↑(Delta n)) (m + 1) σ))

theorem SphereOddDegree.AffineBarycentricSubdivision.singularBoundary_coneLinearMap (R : Type) [CommRing R] (n m : ℕ) (v : ↑(Delta n)) : CategoryTheory.CategoryStruct.comp (coneLinearMap R n (m + 1) v) (singularBoundary R (↧↑(Delta n)) (m + 1)) + CategoryTheory.CategoryStruct.comp (singularBoundary R (↧↑(Delta n)) m) (coneLinearMap R n m v) = CategoryTheory.CategoryStruct.id (singularChainGroup R (↧↑(Delta n)) (m + 1))