Coordinate Projection #
noncomputable def
SphereOddDegree.keepHom
(R : Type)
[CommRing R]
(X : TopCat)
{n : ℕ}
(P : singularSimplices X n → Prop)
[DecidablePred P]
:
The chain projection that retains exactly the singular generators satisfying a predicate.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
SphereOddDegree.keepHom_generator
{R : Type}
[CommRing R]
{X : TopCat}
{n : ℕ}
(P : singularSimplices X n → Prop)
[DecidablePred P]
(σ : singularSimplices X n)
:
(ModuleCat.Hom.hom (keepHom R X P)) (AffineBarycentricSubdivision.chainGenerator R X n σ) = if P σ then AffineBarycentricSubdivision.chainGenerator R X n σ else 0
theorem
SphereOddDegree.keepHom_mem_subChainSubmodule
{R : Type}
[CommRing R]
{X : TopCat}
{n : ℕ}
{S T : Set ↑X}
[DecidablePred (IsSubordinate S)]
{c : ↑(AffineBarycentricSubdivision.singularChainGroup R X n)}
(hc : c ∈ subChainSubmodule R X T n)
:
theorem
SphereOddDegree.keepHom_eq_self_of_mem
{R : Type}
[CommRing R]
{X : TopCat}
{n : ℕ}
{S : Set ↑X}
[DecidablePred (IsSubordinate S)]
{c : ↑(AffineBarycentricSubdivision.singularChainGroup R X n)}
(hc : c ∈ subChainSubmodule R X S n)
: