Degree-wise barycentric subdivision operator on singular chains

This file builds on AffineBarycentricSubdivision.lean.

For a singular n-simplex σ : Δⁿ → X, barycentric subdivision is defined in chain degree n by the classical signed finite sum

sd(σ) = Σ_{π ∈ Sym(n+1)} sign(π) · (σ ∘ a_π),

where a_π : Δⁿ → Δⁿ is the affine simplex defined in AffineBarycentricSubdivision.lean, sending the k-th vertex of the domain to barycenter(π 0, ..., π k).

The output here is deliberately degree-wise:

• barycentricSubdivSimplex composes a singular simplex with one affine subdivision simplex;
• barycentricSubdivisionGenerator is the signed subdivision of one basis simplex as an element of the singular chain group;
• barycentricSubdivisionLinearMap extends this assignment linearly to all singular chains in a fixed degree.

This file does not assert that this degree-wise operator commutes with the boundary. The required boundary theorem is the face/sign calculation

∂ (sd c) = sd (∂ c).

Only after that theorem is proved should one package sd as a genuine chain map.

1. Continuous affine subdivision maps

theorem SphereOddDegree.AffineBarycentricSubdivision.continuous_affineSubdivMapFun_coord (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (j : Fin (n + 1)) : Continuous fun (x : ↑(Delta n)) => affineSubdivMapFun n π x j

Coordinate continuity for the affine subdivision map.

theorem SphereOddDegree.AffineBarycentricSubdivision.continuous_affineSubdivMap (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : Continuous (affineSubdivMap n π)

The affine subdivision map is continuous.

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.affineSubdivContinuousMap (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : C(↑(Delta n), ↑(Delta n))

The affine subdivision simplex as a bundled continuous self-map of Δⁿ.

Equations

• SphereOddDegree.AffineBarycentricSubdivision.affineSubdivContinuousMap n π = { toFun := SphereOddDegree.AffineBarycentricSubdivision.affineSubdivMap n π, continuous_toFun := ⋯ }

@[simp]

theorem SphereOddDegree.AffineBarycentricSubdivision.affineSubdivContinuousMap_apply (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (x : ↑(Delta n)) : (affineSubdivContinuousMap n π) x = affineSubdivMap n π x

2. Singular-simplex summands

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.intrinsicSimplexCoordinates (n : ℕ) : Convexity.StdSimplex ℝ (Fin (n + 1)) ≃ₜ ↑(Delta n)

Coordinate realization of Mathlib's intrinsic simplex.

Equations

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

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.singularSimplexAsContinuousMap (X : TopCat) (n : ℕ) (σ : singularSimplices X n) : C(↑(Delta n), ↑X)

Convert a singular simplex, represented as a simplex of TopCat.toSSet.obj X, to the corresponding bundled continuous map out of the topological standard simplex.

Equations

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

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.continuousMapAsSingularSimplex (X : TopCat) (n : ℕ) (σ : C(↑(Delta n), ↑X)) : singularSimplices X n

Convert a bundled continuous map out of the standard simplex into the corresponding simplex of the singular simplicial set.

Equations

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

@[simp]

theorem SphereOddDegree.AffineBarycentricSubdivision.singularSimplexAsContinuousMap_continuousMapAsSingularSimplex (X : TopCat) (n : ℕ) (σ : C(↑(Delta n), ↑X)) : singularSimplexAsContinuousMap X n (continuousMapAsSingularSimplex X n σ) = σ

@[simp]

theorem SphereOddDegree.AffineBarycentricSubdivision.continuousMapAsSingularSimplex_singularSimplexAsContinuousMap (X : TopCat) (n : ℕ) (σ : singularSimplices X n) : continuousMapAsSingularSimplex X n (singularSimplexAsContinuousMap X n σ) = σ

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivSimplex (X : TopCat) (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (σ : singularSimplices X n) : singularSimplices X n

The π-summand of barycentric subdivision of a singular simplex: precompose σ : Δⁿ → X with the affine subdivision simplex a_π : Δⁿ → Δⁿ.

Equations

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

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivSimplex_def (X : TopCat) (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (σ : singularSimplices X n) : barycentricSubdivSimplex X n π σ = continuousMapAsSingularSimplex X n ((singularSimplexAsContinuousMap X n σ).comp (affineSubdivContinuousMap n π))

The identity permutation summand is the singular simplex obtained by precomposition with the identity-order affine subdivision simplex. This is not simplified to σ; the identity-order affine summand is only one subsimplex of barycentric subdivision, not the identity map.

3. Degree-wise chain groups and generators

@[reducible, inline]

noncomputable abbrev SphereOddDegree.AffineBarycentricSubdivision.singularChainGroup (R : Type) [CommRing R] (X : TopCat) (n : ℕ) : ModuleCat R

The singular chain group C_n(X; R) with coefficients in R, specialized to coefficients R as a module over itself.

Equations

• SphereOddDegree.AffineBarycentricSubdivision.singularChainGroup R X n = (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj ↧R).obj X).X n

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.chainGenerator (R : Type) [CommRing R] (X : TopCat) (n : ℕ) (σ : singularSimplices X n) : ↑(singularChainGroup R X n)

The basis chain associated to a singular simplex.

Equations

• SphereOddDegree.AffineBarycentricSubdivision.chainGenerator R X n σ = (ModuleCat.Hom.hom (CategoryTheory.Limits.Sigma.ι (fun (x : SphereOddDegree.singularSimplices X n) => ↧R) σ)) 1

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.permSignCoeff (R : Type) [CommRing R] {n : ℕ} (π : Equiv.Perm (Fin (n + 1))) : R

The sign of a finite permutation, interpreted in a coefficient ring. For R = ℤ this is ±1; for R = ZMod 2 both signs become 1.

Equations

• SphereOddDegree.AffineBarycentricSubdivision.permSignCoeff R π = ↑↑(Equiv.Perm.sign π)

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionGenerator (R : Type) [CommRing R] (X : TopCat) (n : ℕ) (σ : singularSimplices X n) : ↑(singularChainGroup R X n)

The barycentric subdivision of a basis singular simplex as a chain in the same degree.

Equations

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

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionGeneratorHom (R : Type) [CommRing R] (X : TopCat) (n : ℕ) (σ : singularSimplices X n) : ↧R ⟶ singularChainGroup R X n

The R-linear map R → C_n(X; R) sending 1 to the barycentric subdivision of a fixed basis simplex.

Equations

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

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionLinearMap (R : Type) [CommRing R] (X : TopCat) (n : ℕ) : singularChainGroup R X n ⟶ singularChainGroup R X n

The degree-n barycentric subdivision operator on singular chains. It is obtained from the coproduct universal property by prescribing its value on each basis simplex.

Equations

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

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionLinearMap_generator (R : Type) [CommRing R] (X : TopCat) (n : ℕ) (σ : singularSimplices X n) : (ModuleCat.Hom.hom (barycentricSubdivisionLinearMap R X n)) (chainGenerator R X n σ) = barycentricSubdivisionGenerator R X n σ

The degree-wise subdivision operator has the prescribed value on basis simplices.

@[reducible, inline]

noncomputable abbrev SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionLinearMapℤ (X : TopCat) (n : ℕ) : singularChainGroup ℤ X n ⟶ singularChainGroup ℤ X n

Integral degree-wise barycentric subdivision.

Equations

• SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionLinearMapℤ X n = SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionLinearMap ℤ X n

@[reducible, inline]

noncomputable abbrev SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionLinearMapZMod2 (X : TopCat) (n : ℕ) : singularChainGroup (ZMod 2) X n ⟶ singularChainGroup (ZMod 2) X n

Mod-2 degree-wise barycentric subdivision. The same signed definition is used; the sign coefficients reduce to 1 in ZMod 2.

Equations

• SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionLinearMapZMod2 X n = SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionLinearMap (ZMod 2) X n

4. Explicit formulas useful for later boundary computations

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionLinearMap_generator_sum (R : Type) [CommRing R] (X : TopCat) (n : ℕ) (σ : singularSimplices X n) : (ModuleCat.Hom.hom (barycentricSubdivisionLinearMap R X n)) (chainGenerator R X n σ) = ∑ π : Equiv.Perm (Fin (n + 1)), permSignCoeff R π • chainGenerator R X n (barycentricSubdivSimplex X n π σ)

Expanding the value of the degree-wise operator on a basis simplex.

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionLinearMap_add (R : Type) [CommRing R] (X : TopCat) (n : ℕ) (c d : ↑(singularChainGroup R X n)) : (ModuleCat.Hom.hom (barycentricSubdivisionLinearMap R X n)) (c + d) = (ModuleCat.Hom.hom (barycentricSubdivisionLinearMap R X n)) c + (ModuleCat.Hom.hom (barycentricSubdivisionLinearMap R X n)) d

Linearity of the degree-wise subdivision operator, as a concrete formula on vectors in the degree-n singular chain group.

theorem SphereOddDegree.AffineBarycentricSubdivision.barycentricSubdivisionLinearMap_smul (R : Type) [CommRing R] (X : TopCat) (n : ℕ) (a : R) (c : ↑(singularChainGroup R X n)) : (ModuleCat.Hom.hom (barycentricSubdivisionLinearMap R X n)) (a • c) = a • (ModuleCat.Hom.hom (barycentricSubdivisionLinearMap R X n)) c

Scalar compatibility of the degree-wise subdivision operator.

5. The singular boundary on generators

noncomputable def SphereOddDegree.AffineBarycentricSubdivision.singularBoundary (R : Type) [CommRing R] (X : TopCat) (n : ℕ) : singularChainGroup R X (n + 1) ⟶ singularChainGroup R X n

The singular boundary map ∂ : C_{n+1}(X; R) → C_n(X; R), i.e. the differential of the singular chain complex with coefficients in R.

Equations

• SphereOddDegree.AffineBarycentricSubdivision.singularBoundary R X n = (((AlgebraicTopology.singularChainComplexFunctor (ModuleCat R)).obj ↧R).obj X).d (n + 1) n

theorem SphereOddDegree.AffineBarycentricSubdivision.singularBoundary_sigma_ι_formula (R : Type) [CommRing R] (X : TopCat) (n : ℕ) (σ : singularSimplices X (n + 1)) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun (x : singularSimplices X (n + 1)) => ↧R) σ) (singularBoundary R X n) = ∑ i : Fin (n + 2), (-1) ^ ↑i • CategoryTheory.Limits.Sigma.ι (fun (x : singularSimplices X n) => ↧R) (AlexanderWhitney.faceSimplex X n i σ)

Coproduct-injection boundary formula. Pre-composing the coproduct injection of a basis simplex σ with the singular differential yields the alternating sum of the coproduct injections of the boundary faces of σ: Sigma.ι σ ≫ ∂ = ∑ i (-1)^i • Sigma.ι (faceSimplex … i σ).

theorem SphereOddDegree.AffineBarycentricSubdivision.singularBoundary_chainGenerator_formula (R : Type) [CommRing R] (X : TopCat) (n : ℕ) (σ : singularSimplices X (n + 1)) : (ModuleCat.Hom.hom (singularBoundary R X n)) (chainGenerator R X (n + 1) σ) = ∑ i : Fin (n + 2), (-1) ^ ↑i • chainGenerator R X n (AlexanderWhitney.faceSimplex X n i σ)

Singular boundary on a generator. The differential ∂ of the singular chain complex acts on a basis chain [σ] by the classical alternating sum over boundary faces:

∂[σ] = ∑_i (-1)^i [σ ∘ δ_i].

This is the concrete face/sign formula in the library's actual singular-chain API; it is AlternatingFaceMapComplex.obj_d_eq specialised to the singular simplicial module, with the integer signs (-1)^i interpreted in R.