Subdivision and its homotopy on small singular chains #
Barycentric subdivision and its prism operator preserve chains subordinate to any family of subsets: every simplex they produce factors through the original singular simplex. This file restricts both operators to the small-chain complex and proves the homotopy formula there. Thus subdivision induces the identity on small-chain homology as well as ordinary homology. This is needed when replacing a bounding chain by a sufficiently fine subdivision while keeping the correction to its already-small boundary inside the small-chain complex.
The restricted operators commute with the inclusion and with maps of covered spaces. No openness or covering hypothesis is needed for these preservation statements.
References #
- A. Hatcher, Algebraic Topology, Section 2.1, proof of Proposition 2.21, steps (2) and (4).
theorem
TauCeti.instMonoFNatChainComplexMapιSmallSingularSubcomplex
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasCoproducts C]
(R : C)
{X : TopCat}
{ι : Type u_1}
(U : ι → Set ↑X)
(n : ℕ)
:
CategoryTheory.Mono ((SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R).f n)
noncomputable def
TauCeti.smallSingularSubdivisionX
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasCoproducts C]
(R : C)
{X : TopCat}
{ι : Type u_1}
(U : ι → Set ↑X)
(n : ℕ)
:
((X.smallSingularSubcomplex U).toSSet.chainComplex R).X n ⟶ ((X.smallSingularSubcomplex U).toSSet.chainComplex R).X n
Barycentric subdivision restricted to small singular chains in degree n.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TauCeti.ιChainComplex_smallSingularSubdivisionX
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasCoproducts C]
(R : C)
{X : TopCat}
{ι : Type u_1}
(U : ι → Set ↑X)
{n : ℕ}
(σ : (X.smallSingularSubcomplex U).toSSet.obj (Opposite.op { len := n }))
:
CategoryTheory.CategoryStruct.comp ((X.smallSingularSubcomplex U).toSSet.ιChainComplex σ)
(smallSingularSubdivisionX R U n) = (AffineChain.smallSingularChain R U σ n)
((AffineChain.subdivision (Convexity.StdSimplex ℝ (Fin (n + 1))) n) (AffineChain.simplex n))
@[simp]
theorem
TauCeti.ιChainComplex_smallSingularSubdivisionX_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasCoproducts C]
(R : C)
{X : TopCat}
{ι : Type u_1}
(U : ι → Set ↑X)
{n : ℕ}
(σ : (X.smallSingularSubcomplex U).toSSet.obj (Opposite.op { len := n }))
{Z : C}
(h : ((X.smallSingularSubcomplex U).toSSet.chainComplex R).X n ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((X.smallSingularSubcomplex U).toSSet.ιChainComplex σ)
(CategoryTheory.CategoryStruct.comp (smallSingularSubdivisionX R U n) h) = CategoryTheory.CategoryStruct.comp
((AffineChain.smallSingularChain R U σ n)
((AffineChain.subdivision (Convexity.StdSimplex ℝ (Fin (n + 1))) n) (AffineChain.simplex n)))
h
@[simp]
theorem
TauCeti.smallSingularSubdivisionX_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasCoproducts C]
(R : C)
{X : TopCat}
{ι : Type u_1}
(U : ι → Set ↑X)
(n : ℕ)
:
CategoryTheory.CategoryStruct.comp (smallSingularSubdivisionX R U n)
((SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R).f n) = CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R).f n)
(singularSubdivisionX R X n)
Inclusion intertwines the restricted and ordinary subdivision operators.
@[simp]
theorem
TauCeti.smallSingularSubdivisionX_ι_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasCoproducts C]
(R : C)
{X : TopCat}
{ι : Type u_1}
(U : ι → Set ↑X)
(n : ℕ)
{Z : C}
(h : ((TopCat.toSSet.obj X).chainComplex R).X n ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (smallSingularSubdivisionX R U n)
(CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R).f n) h) = CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R).f n)
(CategoryTheory.CategoryStruct.comp (singularSubdivisionX R X n) h)
Inclusion intertwines the restricted and ordinary subdivision operators.
noncomputable def
TauCeti.smallSingularSubdivisionChainMap
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasCoproducts C]
(R : C)
{X : TopCat}
{ι : Type u_1}
(U : ι → Set ↑X)
:
(X.smallSingularSubcomplex U).toSSet.chainComplex R ⟶ (X.smallSingularSubcomplex U).toSSet.chainComplex R
Barycentric subdivision as an endomorphism of the small-chain complex.
Equations
- TauCeti.smallSingularSubdivisionChainMap R U = { f := fun (n : ℕ) => TauCeti.smallSingularSubdivisionX R U n, comm' := ⋯ }
Instances For
@[simp]
theorem
TauCeti.smallSingularSubdivisionChainMap_f
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasCoproducts C]
(R : C)
{X : TopCat}
{ι : Type u_1}
(U : ι → Set ↑X)
(n : ℕ)
:
@[simp]
theorem
TauCeti.smallSingularSubdivisionChainMap_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasCoproducts C]
(R : C)
{X : TopCat}
{ι : Type u_1}
(U : ι → Set ↑X)
:
The restricted chain map commutes with the inclusion of small chains.
@[simp]
theorem
TauCeti.smallSingularSubdivisionChainMap_ι_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasCoproducts C]
(R : C)
{X : TopCat}
{ι : Type u_1}
(U : ι → Set ↑X)
{Z : ChainComplex C ℕ}
(h : (TopCat.toSSet.obj X).chainComplex R ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (smallSingularSubdivisionChainMap R U)
(CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R) h) = CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R)
(CategoryTheory.CategoryStruct.comp (singularSubdivisionChainMap R X) h)
The restricted chain map commutes with the inclusion of small chains.
noncomputable def
TauCeti.smallSingularPrismX
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasCoproducts C]
(R : C)
{X : TopCat}
{ι : Type u_1}
(U : ι → Set ↑X)
(n : ℕ)
:
((X.smallSingularSubcomplex U).toSSet.chainComplex R).X n ⟶ ((X.smallSingularSubcomplex U).toSSet.chainComplex R).X (n + 1)
The prism operator of subdivision restricted to small singular chains.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TauCeti.ιChainComplex_smallSingularPrismX
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasCoproducts C]
(R : C)
{X : TopCat}
{ι : Type u_1}
(U : ι → Set ↑X)
{n : ℕ}
(σ : (X.smallSingularSubcomplex U).toSSet.obj (Opposite.op { len := n }))
:
CategoryTheory.CategoryStruct.comp ((X.smallSingularSubcomplex U).toSSet.ιChainComplex σ) (smallSingularPrismX R U n) = (AffineChain.smallSingularChain R U σ (n + 1)) (AffineChain.prismModel n)
@[simp]
theorem
TauCeti.ιChainComplex_smallSingularPrismX_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasCoproducts C]
(R : C)
{X : TopCat}
{ι : Type u_1}
(U : ι → Set ↑X)
{n : ℕ}
(σ : (X.smallSingularSubcomplex U).toSSet.obj (Opposite.op { len := n }))
{Z : C}
(h : ((X.smallSingularSubcomplex U).toSSet.chainComplex R).X (n + 1) ⟶ Z)
:
@[simp]
theorem
TauCeti.smallSingularPrismX_ι
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasCoproducts C]
(R : C)
{X : TopCat}
{ι : Type u_1}
(U : ι → Set ↑X)
(n : ℕ)
:
CategoryTheory.CategoryStruct.comp (smallSingularPrismX R U n)
((SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R).f (n + 1)) = CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R).f n)
(singularPrismX R X n)
Inclusion intertwines the restricted and ordinary prism operators.
@[simp]
theorem
TauCeti.smallSingularPrismX_ι_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasCoproducts C]
(R : C)
{X : TopCat}
{ι : Type u_1}
(U : ι → Set ↑X)
(n : ℕ)
{Z : C}
(h : ((TopCat.toSSet.obj X).chainComplex R).X (n + 1) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (smallSingularPrismX R U n)
(CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R).f (n + 1)) h) = CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap (X.smallSingularSubcomplex U).ι R).f n)
(CategoryTheory.CategoryStruct.comp (singularPrismX R X n) h)
Inclusion intertwines the restricted and ordinary prism operators.
@[simp]
theorem
TauCeti.smallSingularPrismX_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasCoproducts C]
(R : C)
{X : TopCat}
{ι : Type u_1}
(U : ι → Set ↑X)
:
@[simp]
theorem
TauCeti.smallSingularSubdivisionX_zero
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasCoproducts C]
(R : C)
{X : TopCat}
{ι : Type u_1}
(U : ι → Set ↑X)
:
smallSingularSubdivisionX R U 0 = CategoryTheory.CategoryStruct.id (((X.smallSingularSubcomplex U).toSSet.chainComplex R).X 0)
theorem
TauCeti.smallSingularPrismX_boundary_add_boundary_smallSingularPrismX
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasCoproducts C]
(R : C)
{X : TopCat}
{ι : Type u_1}
(U : ι → Set ↑X)
(n : ℕ)
:
CategoryTheory.CategoryStruct.comp (((X.smallSingularSubcomplex U).toSSet.chainComplex R).d (n + 1) n)
(smallSingularPrismX R U n) + CategoryTheory.CategoryStruct.comp (smallSingularPrismX R U (n + 1))
(((X.smallSingularSubcomplex U).toSSet.chainComplex R).d (n + 2) (n + 1)) = CategoryTheory.CategoryStruct.id (((X.smallSingularSubcomplex U).toSSet.chainComplex R).X (n + 1)) - smallSingularSubdivisionX R U (n + 1)
The prism homotopy formula holds inside the small-chain complex.
noncomputable def
TauCeti.smallSingularSubdivisionHomotopy
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasCoproducts C]
(R : C)
{X : TopCat}
{ι : Type u_1}
(U : ι → Set ↑X)
:
Subdivision of small singular chains is chain homotopic to their identity map.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
TauCeti.smallSingularSubdivisionHomotopy_hom
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasCoproducts C]
(R : C)
{X : TopCat}
{ι : Type u_1}
(U : ι → Set ↑X)
(n : ℕ)
:
theorem
TauCeti.smallSingularSubdivisionChainMap_naturality
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasCoproducts C]
(R : C)
{X : TopCat}
{ι : Type u_1}
(U : ι → Set ↑X)
{κ : Type u_2}
{Y : TopCat}
(V : κ → Set ↑Y)
(f : X ⟶ Y)
(r : ι → κ)
(hf : ∀ (i : ι), Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) (U i) (V (r i)))
:
The restricted subdivision commutes with maps carrying cover members into cover members.
theorem
TauCeti.smallSingularSubdivisionChainMap_naturality_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasCoproducts C]
(R : C)
{X : TopCat}
{ι : Type u_1}
(U : ι → Set ↑X)
{κ : Type u_2}
{Y : TopCat}
(V : κ → Set ↑Y)
(f : X ⟶ Y)
(r : ι → κ)
(hf : ∀ (i : ι), Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) (U i) (V (r i)))
{Z : ChainComplex C ℕ}
(h : (Y.smallSingularSubcomplex V).toSSet.chainComplex R ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (TopCat.smallSingularSubcomplexMap U V f r hf) R)
(CategoryTheory.CategoryStruct.comp (smallSingularSubdivisionChainMap R V) h) = CategoryTheory.CategoryStruct.comp (smallSingularSubdivisionChainMap R U)
(CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (TopCat.smallSingularSubcomplexMap U V f r hf) R) h)
The restricted subdivision commutes with maps carrying cover members into cover members.
theorem
TauCeti.smallSingularPrismX_naturality
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasCoproducts C]
(R : C)
{X : TopCat}
{ι : Type u_1}
(U : ι → Set ↑X)
{κ : Type u_2}
{Y : TopCat}
(V : κ → Set ↑Y)
(f : X ⟶ Y)
(r : ι → κ)
(hf : ∀ (i : ι), Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) (U i) (V (r i)))
(n : ℕ)
:
CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap (TopCat.smallSingularSubcomplexMap U V f r hf) R).f n)
(smallSingularPrismX R V n) = CategoryTheory.CategoryStruct.comp (smallSingularPrismX R U n)
((SSet.chainComplexMap (TopCat.smallSingularSubcomplexMap U V f r hf) R).f (n + 1))
The restricted prism commutes with maps carrying cover members into cover members.
theorem
TauCeti.smallSingularPrismX_naturality_assoc
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasCoproducts C]
(R : C)
{X : TopCat}
{ι : Type u_1}
(U : ι → Set ↑X)
{κ : Type u_2}
{Y : TopCat}
(V : κ → Set ↑Y)
(f : X ⟶ Y)
(r : ι → κ)
(hf : ∀ (i : ι), Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom f)) (U i) (V (r i)))
(n : ℕ)
{Z : C}
(h : ((Y.smallSingularSubcomplex V).toSSet.chainComplex R).X (n + 1) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp ((SSet.chainComplexMap (TopCat.smallSingularSubcomplexMap U V f r hf) R).f n)
(CategoryTheory.CategoryStruct.comp (smallSingularPrismX R V n) h) = CategoryTheory.CategoryStruct.comp (smallSingularPrismX R U n)
(CategoryTheory.CategoryStruct.comp
((SSet.chainComplexMap (TopCat.smallSingularSubcomplexMap U V f r hf) R).f (n + 1)) h)
The restricted prism commutes with maps carrying cover members into cover members.
@[simp]
theorem
TauCeti.homologyMap_smallSingularSubdivisionChainMap
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Preadditive C]
[CategoryTheory.Limits.HasCoproducts C]
(R : C)
{X : TopCat}
{ι : Type u_1}
(U : ι → Set ↑X)
[CategoryTheory.CategoryWithHomology C]
(n : ℕ)
:
Subdivision acts as the identity on small-chain homology.