The alternating coface complex is the opposite of an alternating face complex

Mathlib develops extra degeneracies, and the homotopy equivalence they induce, on the simplicial side: SimplicialObject.Augmented.ExtraDegeneracy.homotopyEquiv is stated against alternatingFaceMapComplex and lands in ChainComplex. Čech cohomology, in Mathlib/CategoryTheory/Sites/SheafCohomology/Cech.lean, is built from alternatingCofaceMapComplex and is cosimplicial. Nothing upstream connects the two, so no Čech vanishing argument can reach the machinery that would prove it.

This file supplies the connection: for a cosimplicial object Y in a preadditive category,

((alternatingCofaceMapComplex A).obj Y).op ≅ (alternatingFaceMapComplex Aᵒᵖ).obj Y.op

Both sides are Y.obj ⦋n⦌ in degree n — that much is rfl — and both differentials are ∑ i, (-1) ^ i • δ i. What is not rfl is that HomologicalComplex.op distributes over the sum and the zsmul; that is the content, such as it is, and op_sum and op_zsmul supply it.

Why this is the useful direction

The alternative is to define an extra codegeneracy structure on augmented cosimplicial objects and redo the homotopy from scratch, roughly duplicating Mathlib/AlgebraicTopology/ExtraDegeneracy.lean. With this isomorphism that is unnecessary: a cosimplicial object in A is a simplicial object in Aᵒᵖ, the upstream extra-degeneracy theory applies there verbatim, and the isomorphism carries its conclusion back. In particular CategoryTheory.Limits.FormalCoproduct.extraDegeneracyCech — the Čech object of a family has an extra degeneracy once the terminal object maps into one of its members — is already upstream and can be used as it stands.

The payoff

exactAt_succ_of_extraDegeneracy is what #13 consumes: an extra degeneracy on an augmented simplicial object in Aᵒᵖ whose underlying object is Y.op forces the alternating coface complex of Y to be exact in every positive degree. The chain is ExtraDegeneracy.homotopyEquiv (upstream) → quasi-isomorphism → exactAt_iff_of_quasiIsoAt → ChainComplex.exactAt_succ_single_obj, carried across opIso.

exactAt_succ_of_extraDegeneracy_map adds the contravariant transport. ExtraDegeneracy.map takes a covariant functor, while Čech cohomology applies FormalCoproduct.evalOp of a presheaf, which is contravariant on the site; Functor.rightOp turns one into the other, and this lemma is the composite in the form the caller wants.

Not done here

An augmentation ε for alternatingCofaceMapComplex, dual to AlternatingFaceMapComplex.ε, was expected to be needed and is not. The augmentation is handled on the simplicial side by homotopyEquiv, and the coface complex only ever appears unaugmented, so adding one would be dead weight. Recorded because the issue asked for it.

DerivedAlgGeo/AlgebraicGeometry/Cohomology/Cech/Affine.lean now supplies the remaining affine argument: it identifies the restriction maps degreewise as localizations and descends exactness from a finite distinguished-open cover whose defining elements span the unit ideal.

The Abelian A hypothesis is stronger than the argument needs — Preadditive, a zero object and homology would do — but the two HasZeroMorphisms Aᵒᵖ instances (Preadditive's and Limits.hasZeroMorphismsOpposite) are only definitionally equal, and rw sees through neither. Assuming Abelian makes instance search pick one consistently. Every intended caller is abelian.

References

• Mathlib/AlgebraicTopology/ExtraDegeneracy.lean — the simplicial theory this reaches
• Mathlib/CategoryTheory/Limits/FormalCoproducts/ExtraDegeneracy.lean — the Čech object's extra degeneracy, already upstream

noncomputable def AlgebraicTopology.AlternatingCofaceMapComplex.opIso {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] (Y : CategoryTheory.CosimplicialObject A) : HomologicalComplex.op ((alternatingCofaceMapComplex A).obj Y) ≅ (alternatingFaceMapComplex Aᵒᵖ).obj (CategoryTheory.Functor.op Y)

The alternating coface map complex of a cosimplicial object Y in A, made opposite, is the alternating face map complex of Y viewed as a simplicial object in Aᵒᵖ.

Degreewise both sides are Y.obj ⦋n⦌, and both differentials are ∑ i, (-1) ^ i • δ i; the proof is that op distributes over that sum.

Equations

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

@[simp]

theorem AlgebraicTopology.AlternatingCofaceMapComplex.opIso_hom_f {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] (Y : CategoryTheory.CosimplicialObject A) (n : ℕ) : (opIso Y).hom.f n = CategoryTheory.CategoryStruct.id ((HomologicalComplex.op ((alternatingCofaceMapComplex A).obj Y)).X n)

@[simp]

theorem AlgebraicTopology.AlternatingCofaceMapComplex.opIso_inv_f {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Preadditive A] (Y : CategoryTheory.CosimplicialObject A) (n : ℕ) : (opIso Y).inv.f n = CategoryTheory.CategoryStruct.id (((alternatingFaceMapComplex Aᵒᵖ).obj (CategoryTheory.Functor.op Y)).X n)

theorem AlgebraicTopology.exactAt_succ_of_extraDegeneracy {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {Y : CategoryTheory.CosimplicialObject A} {X : CategoryTheory.SimplicialObject.Augmented Aᵒᵖ} (e : CategoryTheory.SimplicialObject.Augmented.drop.obj X ≅ CategoryTheory.Functor.op Y) (ed : X.ExtraDegeneracy) (n : ℕ) : HomologicalComplex.ExactAt ((alternatingCofaceMapComplex A).obj Y) (n + 1)

Positive-degree exactness from an extra degeneracy. If the opposite of a cosimplicial object Y in A underlies an augmented simplicial object in Aᵒᵖ carrying an extra degeneracy, then the alternating coface complex of Y is exact in every positive degree.

The augmentation is not visible in the conclusion, which is the point: it lives on the simplicial side, where ExtraDegeneracy.homotopyEquiv already handles it.

theorem AlgebraicTopology.exactAt_succ_of_extraDegeneracy_map {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Abelian A] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] {X : CategoryTheory.SimplicialObject.Augmented D} (ed : X.ExtraDegeneracy) (G : CategoryTheory.Functor Dᵒᵖ A) {Y : CategoryTheory.CosimplicialObject A} (e : CategoryTheory.SimplicialObject.Augmented.drop.obj (((CategoryTheory.SimplicialObject.Augmented.whiskering D Aᵒᵖ).obj G.rightOp).obj X) ≅ CategoryTheory.Functor.op Y) (n : ℕ) : HomologicalComplex.ExactAt ((alternatingCofaceMapComplex A).obj Y) (n + 1)

The same, with the contravariant transport folded in.

ExtraDegeneracy.map applies a covariant functor. Čech cohomology applies FormalCoproduct.evalOp of a presheaf, which is contravariant on the site; Functor.rightOp converts one to the other. This is the form a Čech vanishing argument calls.