The cutoff contraction of the cochains of a groupoid nerve

Let C be a groupoid, k a commutative ring and M a k-module. The cochain complex TauCeti.nerveCochainComplex C k M of the nerve of C with coefficients in M is, in degree n, the module of M-valued functions on strings x₀ ⟶ x₁ ⟶ ⋯ ⟶ xₙ of n composable arrows (TauCeti.cochainValuesEquiv), with the alternating sum of faces as differential.

A function c : C → k on the objects is a cutoff if for every object x its values at the sources of the arrows with target x sum to one, ∑ᶠ b : Quiver.Costar x, c b.1 = 1. Inverting arrows, this is the normalization ∑ᶠ a ∈ Quiver.Total.left ⁻¹' {x}, c a.right = 1 of the cutoff functions TauCeti.Quiver.IsCutoff of proper étale groupoids (Quiver.Total.finsum_costar_eq_finsum_mem_preimage_left_singleton). The groupoid need not be finite, and no topology enters here.

Prepending an arrow weighted by c defines operators lowering the degree, $$(h\varphi)(x_0 \to \cdots \to x_n) = \sum_{b : y \to x_0} c(y)\, \varphi(y \xrightarrow{b} x_0 \to \cdots \to x_n)$$ (TauCeti.nerveCochainComplex.cutoffPrepend). For each string only finitely many terms are nonzero (otherwise k is the zero ring). With P φ (x) = ∑_{b : y ⟶ x} c(y) φ(y) (TauCeti.nerveCochainComplex.cutoffAverage), they satisfy $$h \circ d + d \circ h = 1 \text{ in positive degrees}, \qquad h \circ d = 1 - P \text{ in degree } 0.$$ So the identity of the cochain complex is homotopic to the cochain map that is P in degree 0 and zero in positive degrees (TauCeti.nerveCochainComplex.cutoffHomotopy). In particular every positive-degree cocycle φ is the coboundary of h φ, the positive-degree cohomology vanishes, the values of P are constant along arrows, and every degree-0 cocycle, that is every function constant along arrows, is fixed by P. The homotopy and the primitives are assembled from the two identities by CochainComplex.homotopyOfDCompEq and CochainComplex.d_hom_apply_of_d_comp_eq. No sign is needed: prepending an arrow commutes with the faces deleting later vertices, and the face deleting the second vertex composes the prepended arrow with the first arrow of the string (CategoryTheory.nerve.δ_succ_precomp), which reindexes the sum since C is a groupoid. Every arrow is counted, including every isotropy arrow.

The operators are natural for functors Φ : D ⥤ C that are bijective on arrows with a given target, such as the restriction to a full subgroupoid on a saturated set of objects, with the cutoff pulled back along Φ (TauCeti.nerveCochainComplex.cochainComplexMap_f_comp_cutoffPrependHom).

This is the groupoid form of the contraction of the cochains of an action presentation TauCeti.groupCohomology.cutoffHomotopy, which inserts a last label instead of a first arrow.

Main declarations

• TauCeti.nerveCochainComplex: the cochain complex of the nerve with coefficients in M.
• TauCeti.nerveCochainComplex.cutoffPrependHom: the operator h lowering the degree.
• TauCeti.nerveCochainComplex.cutoffCochainMap: the cutoff average P, placed in degree 0.
• TauCeti.nerveCochainComplex.cutoffHomotopy: the homotopy from the identity to TauCeti.nerveCochainComplex.cutoffCochainMap.
• TauCeti.nerveCochainComplex.isZero_homology_succ: the positive-degree cohomology vanishes.

References

• M. Crainic, Differentiable and algebroid cohomology, van Est isomorphisms, and characteristic classes, Comment. Math. Helv. 78 (2003), Section 2, for cutoff functions and the vanishing of the cohomology of proper groupoids.
• I. Moerdijk, Orbifolds as groupoids: an introduction, Section 4.

@[reducible, inline]

noncomputable abbrev TauCeti.nerveCochainComplex (C : Type w) [CategoryTheory.Category.{w, w} C] (k : Type w) [CommRing k] (M : ModuleCat k) : CochainComplex (ModuleCat k) ℕ

The cochain complex of the nerve of C with coefficients in M: in degree n, the k-linear maps from the n-chains of the nerve to M. These are the M-valued functions on strings of n composable arrows (TauCeti.cochainValuesEquiv).

noncomputable def TauCeti.nerveCochainComplex.valuesEquiv {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {M : ModuleCat k} (n : ℕ) : ↑((nerveCochainComplex C k M).X n) ≃ₗ[k] CategoryTheory.ComposableArrows C n → ↑M

The value coordinates TauCeti.cochainValuesLinearEquiv on the cochains of degree n of the nerve: they identify these cochains k-linearly with the functions on strings of n composable arrows.

theorem TauCeti.nerveCochainComplex.valuesEquiv_apply {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {M : ModuleCat k} (n : ℕ) (φ : ↑((nerveCochainComplex C k M).X n)) : (valuesEquiv n) φ = (cochainValuesEquiv k M (CategoryTheory.nerve C) n) φ

The value coordinates of the nerve cochains are those of TauCeti.cochainValuesEquiv.

theorem TauCeti.nerveCochainComplex.valuesEquiv_d {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {M : ModuleCat k} (n : ℕ) (φ : ↑((nerveCochainComplex C k M).X n)) (σ : CategoryTheory.ComposableArrows C (n + 1)) : (valuesEquiv (n + 1)) ((CategoryTheory.ConcreteCategory.hom ((nerveCochainComplex C k M).d n (n + 1))) φ) σ = ∑ i : Fin (n + 2), (-1) ^ ↑i • (valuesEquiv n) φ ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (CategoryTheory.nerve C) i)) σ)

The values of a coboundary are alternating sums of values on faces.

noncomputable def TauCeti.nerveCochainComplex.cutoffPrepend {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {M : ModuleCat k} (c : C → k) (n : ℕ) (φ : CategoryTheory.ComposableArrows C (n + 1) → ↑M) (σ : CategoryTheory.ComposableArrows C n) : ↑M

Prepending an arrow weighted by c: the value at a string x₀ ⟶ ⋯ ⟶ xₙ is the sum, over the arrows b : y ⟶ x₀, of c y times the value at the string y ⟶ x₀ ⟶ ⋯ ⟶ xₙ.

noncomputable def TauCeti.nerveCochainComplex.cutoffAverage {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {M : ModuleCat k} (c : C → k) (φ : CategoryTheory.ComposableArrows C 0 → ↑M) : CategoryTheory.ComposableArrows C 0 → ↑M

The cutoff average of a function on objects, viewed as strings of no arrows: the value at x is the sum, over the arrows b : y ⟶ x, of c y times the value at y. It prepends an arrow weighted by c to the function on single arrows given by the value at their source.

theorem TauCeti.nerveCochainComplex.cutoffPrepend_apply {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {M : ModuleCat k} (c : C → k) (n : ℕ) (φ : CategoryTheory.ComposableArrows C (n + 1) → ↑M) (σ : CategoryTheory.ComposableArrows C n) : cutoffPrepend c n φ σ = ∑ᶠ (b : Quiver.Costar σ.left), c b.fst • φ (σ.precomp b.snd)

The value of TauCeti.nerveCochainComplex.cutoffPrepend at a string σ is the sum, over the arrows b into its first vertex, of c at the source of b times the value at σ with b prepended.

theorem TauCeti.nerveCochainComplex.cutoffAverage_apply {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {M : ModuleCat k} (c : C → k) (φ : CategoryTheory.ComposableArrows C 0 → ↑M) (σ : CategoryTheory.ComposableArrows C 0) : cutoffAverage c φ σ = ∑ᶠ (b : Quiver.Costar σ.left), c b.fst • φ (CategoryTheory.ComposableArrows.mk₀ b.fst)

The value of TauCeti.nerveCochainComplex.cutoffAverage at an object σ.left is the sum, over the arrows b into it, of c at the source of b times the value at that source.

theorem TauCeti.nerveCochainComplex.cutoffPrepend_add {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {M : ModuleCat k} {c : C → k} (hc : ∀ (x : C), ∑ᶠ (b : Quiver.Costar x), c b.fst = 1) (n : ℕ) (φ ψ : CategoryTheory.ComposableArrows C (n + 1) → ↑M) : cutoffPrepend c n (φ + ψ) = cutoffPrepend c n φ + cutoffPrepend c n ψ

Prepending arrows weighted by a cutoff is additive.

theorem TauCeti.nerveCochainComplex.cutoffPrepend_smul {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {M : ModuleCat k} {c : C → k} (hc : ∀ (x : C), ∑ᶠ (b : Quiver.Costar x), c b.fst = 1) (n : ℕ) (a : k) (φ : CategoryTheory.ComposableArrows C (n + 1) → ↑M) : cutoffPrepend c n (a • φ) = a • cutoffPrepend c n φ

Prepending arrows weighted by a cutoff commutes with scalar multiplication.

noncomputable def TauCeti.nerveCochainComplex.cutoffPrependHom {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] (M : ModuleCat k) {c : C → k} (hc : ∀ (x : C), ∑ᶠ (b : Quiver.Costar x), c b.fst = 1) (n : ℕ) : (nerveCochainComplex C k M).X (n + 1) ⟶ (nerveCochainComplex C k M).X n

The operator TauCeti.nerveCochainComplex.cutoffPrepend from cochains of degree n + 1 to cochains of degree n.

@[simp]

theorem TauCeti.nerveCochainComplex.valuesEquiv_cutoffPrependHom {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {M : ModuleCat k} {c : C → k} (hc : ∀ (x : C), ∑ᶠ (b : Quiver.Costar x), c b.fst = 1) (n : ℕ) (φ : ↑((nerveCochainComplex C k M).X (n + 1))) : (valuesEquiv n) ((CategoryTheory.ConcreteCategory.hom (cutoffPrependHom M hc n)) φ) = cutoffPrepend c n ((valuesEquiv (n + 1)) φ)

In values, TauCeti.nerveCochainComplex.cutoffPrependHom is TauCeti.nerveCochainComplex.cutoffPrepend.

noncomputable def TauCeti.nerveCochainComplex.cutoffAverageHom {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] (M : ModuleCat k) {c : C → k} (hc : ∀ (x : C), ∑ᶠ (b : Quiver.Costar x), c b.fst = 1) : (nerveCochainComplex C k M).X 0 ⟶ (nerveCochainComplex C k M).X 0

The cutoff average TauCeti.nerveCochainComplex.cutoffAverage on cochains of degree 0.

@[simp]

theorem TauCeti.nerveCochainComplex.valuesEquiv_cutoffAverageHom {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {M : ModuleCat k} {c : C → k} (hc : ∀ (x : C), ∑ᶠ (b : Quiver.Costar x), c b.fst = 1) (φ : ↑((nerveCochainComplex C k M).X 0)) : (valuesEquiv 0) ((CategoryTheory.ConcreteCategory.hom (cutoffAverageHom M hc)) φ) = cutoffAverage c ((valuesEquiv 0) φ)

In values, TauCeti.nerveCochainComplex.cutoffAverageHom is TauCeti.nerveCochainComplex.cutoffAverage.

theorem TauCeti.nerveCochainComplex.cutoffPrepend_d_zero {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {M : ModuleCat k} {c : C → k} (hc : ∀ (x : C), ∑ᶠ (b : Quiver.Costar x), c b.fst = 1) (φ : ↑((nerveCochainComplex C k M).X 0)) (σ : CategoryTheory.ComposableArrows C 0) : cutoffPrepend c 0 ((valuesEquiv 1) ((CategoryTheory.ConcreteCategory.hom ((nerveCochainComplex C k M).d 0 1)) φ)) σ = (valuesEquiv 0) φ σ - cutoffAverage c ((valuesEquiv 0) φ) σ

Contraction in degree 0. Prepending to the coboundary of a function on objects gives the function minus its cutoff average.

theorem TauCeti.nerveCochainComplex.cutoffPrepend_d_add_d_cutoffPrepend {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {M : ModuleCat k} {c : C → k} (hc : ∀ (x : C), ∑ᶠ (b : Quiver.Costar x), c b.fst = 1) [CategoryTheory.IsGroupoid C] (n : ℕ) (φ : ↑((nerveCochainComplex C k M).X (n + 1))) (σ : CategoryTheory.ComposableArrows C (n + 1)) : cutoffPrepend c (n + 1) ((valuesEquiv (n + 2)) ((CategoryTheory.ConcreteCategory.hom ((nerveCochainComplex C k M).d (n + 1) (n + 2))) φ)) σ + (valuesEquiv (n + 1)) ((CategoryTheory.ConcreteCategory.hom ((nerveCochainComplex C k M).d n (n + 1))) ((CategoryTheory.ConcreteCategory.hom (cutoffPrependHom M hc n)) φ)) σ = (valuesEquiv (n + 1)) φ σ

Contraction in positive degrees. For a cochain φ of degree n + 1, prepending to its coboundary plus the coboundary of the prepended cochain is φ.

theorem TauCeti.nerveCochainComplex.d_comp_cutoffPrependHom_add {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {M : ModuleCat k} {c : C → k} (hc : ∀ (x : C), ∑ᶠ (b : Quiver.Costar x), c b.fst = 1) [CategoryTheory.IsGroupoid C] (n : ℕ) : CategoryTheory.CategoryStruct.comp ((nerveCochainComplex C k M).d (n + 1) (n + 2)) (cutoffPrependHom M hc (n + 1)) + CategoryTheory.CategoryStruct.comp (cutoffPrependHom M hc n) ((nerveCochainComplex C k M).d n (n + 1)) = CategoryTheory.CategoryStruct.id ((nerveCochainComplex C k M).X (n + 1))

Contraction in positive degrees, as an identity of maps of cochains.

theorem TauCeti.nerveCochainComplex.d_comp_cutoffPrependHom_zero {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {M : ModuleCat k} {c : C → k} (hc : ∀ (x : C), ∑ᶠ (b : Quiver.Costar x), c b.fst = 1) : CategoryTheory.CategoryStruct.comp ((nerveCochainComplex C k M).d 0 1) (cutoffPrependHom M hc 0) = CategoryTheory.CategoryStruct.id ((nerveCochainComplex C k M).X 0) - cutoffAverageHom M hc

Contraction in degree 0, as an identity of maps of cochains.

theorem TauCeti.nerveCochainComplex.cutoffAverageHom_comp_d {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {M : ModuleCat k} {c : C → k} (hc : ∀ (x : C), ∑ᶠ (b : Quiver.Costar x), c b.fst = 1) [CategoryTheory.IsGroupoid C] : CategoryTheory.CategoryStruct.comp (cutoffAverageHom M hc) ((nerveCochainComplex C k M).d 0 1) = 0

The cutoff average of a function on objects is constant along arrows: its coboundary vanishes.

noncomputable def TauCeti.nerveCochainComplex.cutoffCochainMap {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {M : ModuleCat k} {c : C → k} (hc : ∀ (x : C), ∑ᶠ (b : Quiver.Costar x), c b.fst = 1) [CategoryTheory.IsGroupoid C] : nerveCochainComplex C k M ⟶ nerveCochainComplex C k M

The cutoff average, placed in degree 0, as an endomorphism of the cochain complex: it is TauCeti.nerveCochainComplex.cutoffAverageHom on cochains of degree 0 and zero in positive degrees.

@[simp]

theorem TauCeti.nerveCochainComplex.cutoffCochainMap_f_zero {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {M : ModuleCat k} {c : C → k} (hc : ∀ (x : C), ∑ᶠ (b : Quiver.Costar x), c b.fst = 1) [CategoryTheory.IsGroupoid C] : (cutoffCochainMap hc).f 0 = cutoffAverageHom M hc

In degree 0, TauCeti.nerveCochainComplex.cutoffCochainMap is the cutoff average.

@[simp]

theorem TauCeti.nerveCochainComplex.cutoffCochainMap_f_succ {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {M : ModuleCat k} {c : C → k} (hc : ∀ (x : C), ∑ᶠ (b : Quiver.Costar x), c b.fst = 1) [CategoryTheory.IsGroupoid C] (n : ℕ) : (cutoffCochainMap hc).f (n + 1) = 0

In positive degrees, TauCeti.nerveCochainComplex.cutoffCochainMap is zero.

noncomputable def TauCeti.nerveCochainComplex.cutoffHomotopy {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {M : ModuleCat k} {c : C → k} (hc : ∀ (x : C), ∑ᶠ (b : Quiver.Costar x), c b.fst = 1) [CategoryTheory.IsGroupoid C] : Homotopy (CategoryTheory.CategoryStruct.id (nerveCochainComplex C k M)) (cutoffCochainMap hc)

The cutoff contraction. The identity of the cochain complex of the nerve is homotopic to the cutoff average placed in degree 0, through the homotopy whose component from degree n + 1 to degree n prepends an arrow weighted by c (TauCeti.nerveCochainComplex.cutoffHomotopy_hom_succ).

@[simp]

theorem TauCeti.nerveCochainComplex.cutoffHomotopy_hom_succ {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {M : ModuleCat k} {c : C → k} (hc : ∀ (x : C), ∑ᶠ (b : Quiver.Costar x), c b.fst = 1) [CategoryTheory.IsGroupoid C] (n : ℕ) : (cutoffHomotopy hc).hom (n + 1) n = cutoffPrependHom M hc n

The component of TauCeti.nerveCochainComplex.cutoffHomotopy from degree n + 1 to degree n is TauCeti.nerveCochainComplex.cutoffPrependHom.

theorem TauCeti.nerveCochainComplex.d_cutoffPrependHom_of_d_eq_zero {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {M : ModuleCat k} {c : C → k} (hc : ∀ (x : C), ∑ᶠ (b : Quiver.Costar x), c b.fst = 1) [CategoryTheory.IsGroupoid C] {n : ℕ} {φ : ↑((nerveCochainComplex C k M).X (n + 1))} (hφ : (CategoryTheory.ConcreteCategory.hom ((nerveCochainComplex C k M).d (n + 1) (n + 2))) φ = 0) : (CategoryTheory.ConcreteCategory.hom ((nerveCochainComplex C k M).d n (n + 1))) ((CategoryTheory.ConcreteCategory.hom (cutoffPrependHom M hc n)) φ) = φ

The explicit primitive of a positive-degree cocycle: prepending an arrow weighted by c to a cocycle of degree n + 1 gives a cochain whose coboundary is the cocycle.

theorem TauCeti.nerveCochainComplex.exactAt_succ {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {M : ModuleCat k} {c : C → k} (hc : ∀ (x : C), ∑ᶠ (b : Quiver.Costar x), c b.fst = 1) [CategoryTheory.IsGroupoid C] (n : ℕ) : HomologicalComplex.ExactAt (nerveCochainComplex C k M) (n + 1)

The cochain complex of the nerve is exact in positive degrees.

theorem TauCeti.nerveCochainComplex.isZero_homology_succ {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {M : ModuleCat k} {c : C → k} (hc : ∀ (x : C), ∑ᶠ (b : Quiver.Costar x), c b.fst = 1) [CategoryTheory.IsGroupoid C] (n : ℕ) : CategoryTheory.Limits.IsZero (HomologicalComplex.homology (nerveCochainComplex C k M) (n + 1))

The positive-degree cohomology of the nerve with coefficients in M vanishes.

theorem TauCeti.nerveCochainComplex.cutoffAverageHom_apply_of_d_eq_zero {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {M : ModuleCat k} {c : C → k} (hc : ∀ (x : C), ∑ᶠ (b : Quiver.Costar x), c b.fst = 1) {φ : ↑((nerveCochainComplex C k M).X 0)} (hφ : (CategoryTheory.ConcreteCategory.hom ((nerveCochainComplex C k M).d 0 1)) φ = 0) : (CategoryTheory.ConcreteCategory.hom (cutoffAverageHom M hc)) φ = φ

A function on objects constant along arrows, that is a cocycle of degree 0, is its own cutoff average.

Naturality for functors bijective on arrows with a given target

theorem TauCeti.nerveCochainComplex.finsum_costar_comp_eq_one {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {c : C → k} (hc : ∀ (x : C), ∑ᶠ (b : Quiver.Costar x), c b.fst = 1) {D : Type w} [CategoryTheory.Category.{w, w} D] {Φ : CategoryTheory.Functor D C} (hΦ : ∀ (y : D), Function.Bijective (Φ.toPrefunctor.costar y)) (y : D) : ∑ᶠ (b : Quiver.Costar y), (c ∘ Φ.obj) b.fst = 1

A cutoff pulls back to a cutoff along a functor bijective on the arrows with a given target.

theorem TauCeti.nerveCochainComplex.valuesEquiv_cochainComplexMap {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {M : ModuleCat k} {D : Type w} [CategoryTheory.Category.{w, w} D] {Φ : CategoryTheory.Functor D C} (n : ℕ) (φ : ↑((nerveCochainComplex C k M).X n)) (σ : CategoryTheory.ComposableArrows D n) : (valuesEquiv n) ((CategoryTheory.ConcreteCategory.hom ((SSet.cochainComplexMap (CategoryTheory.nerveMap Φ)).f n)) φ) σ = (valuesEquiv n) φ ((Φ.mapComposableArrows n).obj σ)

Pulling back cochains along the functor Φ evaluates them on the images of strings.

theorem TauCeti.nerveCochainComplex.cutoffPrepend_comp_mapComposableArrows {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {M : ModuleCat k} {c : C → k} {D : Type w} [CategoryTheory.Category.{w, w} D] {Φ : CategoryTheory.Functor D C} (hΦ : ∀ (y : D), Function.Bijective (Φ.toPrefunctor.costar y)) (n : ℕ) (φ : CategoryTheory.ComposableArrows C (n + 1) → ↑M) (σ : CategoryTheory.ComposableArrows D n) : cutoffPrepend (c ∘ Φ.obj) n (φ ∘ (Φ.mapComposableArrows (n + 1)).obj) σ = cutoffPrepend c n φ ((Φ.mapComposableArrows n).obj σ)

Prepending arrows weighted by the pulled-back cutoff commutes with evaluating on images of strings under Φ.

theorem TauCeti.nerveCochainComplex.cochainComplexMap_f_comp_cutoffPrependHom {C : Type w} [CategoryTheory.Category.{w, w} C] {k : Type w} [CommRing k] {M : ModuleCat k} {c : C → k} (hc : ∀ (x : C), ∑ᶠ (b : Quiver.Costar x), c b.fst = 1) {D : Type w} [CategoryTheory.Category.{w, w} D] {Φ : CategoryTheory.Functor D C} (hΦ : ∀ (y : D), Function.Bijective (Φ.toPrefunctor.costar y)) (n : ℕ) : CategoryTheory.CategoryStruct.comp ((SSet.cochainComplexMap (CategoryTheory.nerveMap Φ)).f (n + 1)) (cutoffPrependHom M ⋯ n) = CategoryTheory.CategoryStruct.comp (cutoffPrependHom M hc n) ((SSet.cochainComplexMap (CategoryTheory.nerveMap Φ)).f n)

Restriction law. Pulling back cochains along a functor bijective on the arrows with a given target commutes with prepending arrows, weighted by the cutoff and by its pullback.