Normalized free-Yoneda bicomplex augmentation and its total complex

For every scheme X and integer-indexed cochain complex of X.Modules, the free-Yoneda left resolution gives a bicomplex whose natural augmentation normalizes to a flipped single-zero bicomplex and is a quasi-isomorphism in each resolution-direction row. Its integer-extended direct-sum total complex has terms flat over the identity, and the signed total of the normalized target is naturally the input complex. The final augmentation is a quasi-isomorphism for arbitrary inputs. AlgebraicGeometry.Scheme.Modules.isKFlat_freeYonedaSheafCoproductTotalComplexFunctor_obj proves K-flatness of this total downstream in the derived-tensor owner. For every strictly bounded-above input, termwise support and the nonpositive resolution degree make its total augmentation a quasi-isomorphism. This includes every canonical good truncation.

Main definitions

• AlgebraicGeometry.Scheme.Modules.normalizedBicomplexAugmentation is the natural map to the flipped single-zero bicomplex.
• AlgebraicGeometry.Scheme.Modules.freeYonedaSheafCoproductTotalTargetIso identifies the total of the original target with the input.
• AlgebraicGeometry.Scheme.Modules.freeYonedaSheafCoproductTotalAugmentation composes the normalized total map with the signed target comparison.

Main results

All unqualified names in this list are in AlgebraicGeometry.Scheme.Modules.

• AlgebraicGeometry.Scheme.Modules.normalizedBicomplexAugmentation_row_quasiIso proves each resolution-direction row is a quasi-isomorphism.
• freeYonedaSheafCoproductTotalAugmentation_eq_toSingleZero_comp_targetIso identifies the normalized total map with the earlier total-to-single-zero map followed by the target isomorphism.
• quasiIso_freeYonedaSheafCoproductTotalAugmentation_of_isStrictlyLE proves the augmentation is a quasi-isomorphism for strictly bounded-above inputs.
• quasiIso_freeYonedaSheafCoproductTotalAugmentation_truncLE specializes this result to each canonical good truncation.
• AlgebraicGeometry.Scheme.Modules.quasiIso_freeYonedaSheafCoproductTotalAugmentation passes the stagewise quasi-isomorphisms through the good-truncation colimit for arbitrary inputs.
• AlgebraicGeometry.Scheme.Modules.isStrictlyLE_freeYonedaSheafCoproductTotalComplexFunctor_obj retains a strict upper term bound through the nonpositive resolution total.

Implementation notes

The normalized map composes the existing row augmentation with HomologicalComplex₂.singleExtendMapFlipIso at the image degree zero. Its row maps stay quasi-isomorphisms because the second map is an isomorphism. HomologicalComplex₂.singleZeroFlipTotalNatIso supplies the signed total comparison. The original target type is retained for downstream consumers. For an input strictly supported at c, both bicomplexes vanish in outer degrees above c and inner degrees above zero. Reduced left resolution preserves zero terms, so the four-bound total-map criterion applies on each diagonal. The same support bounds give a strict upper bound on the source total. The source and target good-truncation cocones are colimiting. Exact filtered colimits preserve stagewise quasi-isomorphisms, and naturality transports the result from the chosen colimit to the original input.

References

The construction uses Mathlib's ComplexShape.Embedding.extendFunctor, HomologicalComplex₂.totalFunctor, and the repository's natural single-extension, mapped-single/flip, and signed single-zero comparisons.

Tags

free-Yoneda resolution, module sheaf, bicomplex, total complex, quasi-isomorphism

noncomputable def AlgebraicGeometry.Scheme.Modules.freeYonedaSheafCoproductResolutionBicomplexUpInt (X : Scheme) : CategoryTheory.Functor (CochainComplex X.Modules ℤ) (HomologicalComplex₂ X.Modules (ComplexShape.up ℤ) (ComplexShape.up ℤ))

Extend the resolution degree of the free-Yoneda bicomplex from nonnegative chain degrees to nonpositive integer cochain degrees, then include the flat terms into all module sheaves.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.Modules.freeYonedaSheafCoproductTotalComplexFunctor (X : Scheme) : CategoryTheory.Functor (CochainComplex X.Modules ℤ) (CochainComplex X.Modules ℤ)

The direct-sum total complex of the functorial free-Yoneda flat-resolution bicomplex. The augmentation to the input and its quasi-isomorphism are proved below. K-flatness is proved downstream by AlgebraicGeometry.Scheme.Modules.isKFlat_freeYonedaSheafCoproductTotalComplexFunctor_obj.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.Modules.isColimitFreeYonedaSheafCoproductTotalTruncLETowerCocone (X : Scheme) (K : CochainComplex X.Modules ℤ) : CategoryTheory.Limits.IsColimit ((freeYonedaSheafCoproductTotalComplexFunctor X).mapCocone K.truncLETowerCocone)

The literal total free-Yoneda resolution of the canonical good-truncation tower has a colimiting cocone. The mapped bicomplex cocone is colimiting degreewise, and direct-sum totalization preserves its colimit. This does not assert that the total augmentation is a quasi-isomorphism.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.Modules.freeYonedaSheafCoproductResolutionBicomplexAugmentation (X : Scheme) : freeYonedaSheafCoproductResolutionBicomplexUpInt X ⟶ ((ChainComplex.single₀ X.Modules).comp (ComplexShape.embeddingDownNat.extendFunctor X.Modules)).mapHomologicalComplex (ComplexShape.up ℤ)

Apply the natural augmentation of each free-Yoneda left resolution in the resolution direction. The target retains the input complex in resolution degree zero after extending that direction to integer degrees. Its totalization and comparison with the input are constructed below.

Equations

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

theorem AlgebraicGeometry.Scheme.Modules.freeYonedaSheafCoproductResolutionBicomplexAugmentation_row_quasiIso (X : Scheme) (K : CochainComplex X.Modules ℤ) (p : ℤ) : QuasiIso (((freeYonedaSheafCoproductResolutionBicomplexAugmentation X).app K).f p)

In each input degree, the bicomplex augmentation is a quasi-isomorphism in the resolution direction. Mathlib's embedding extension preserves the generic left-resolution quasi-isomorphism; this does not imply that its unbounded direct-sum totalization is a quasi-isomorphism.

noncomputable def AlgebraicGeometry.Scheme.Modules.normalizedBicomplexAugmentation (X : Scheme) : freeYonedaSheafCoproductResolutionBicomplexUpInt X ⟶ (HomologicalComplex.single (CochainComplex X.Modules ℤ) (ComplexShape.up ℤ) 0).comp (HomologicalComplex₂.flipFunctor X.Modules (ComplexShape.up ℤ) (ComplexShape.up ℤ))

Normalize the free-Yoneda augmentation before totalization: the embedding of the resolution degree sends source degree zero to integer degree zero, and HomologicalComplex₂.singleExtendMapFlipIso identifies its target with the flipped single-zero bicomplex.

Equations

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

theorem AlgebraicGeometry.Scheme.Modules.normalizedBicomplexAugmentation_row_quasiIso (X : Scheme) (K : CochainComplex X.Modules ℤ) (p : ℤ) : QuasiIso (((normalizedBicomplexAugmentation X).app K).f p)

Each row of the normalized augmentation remains a quasi-isomorphism: the original row theorem is followed by a component of a bicomplex isomorphism. This rowwise fact does not assert anything about unbounded direct-sum totalization.

noncomputable def AlgebraicGeometry.Scheme.Modules.freeYonedaSheafCoproductTotalAugmentationToSingleZero (X : Scheme) : freeYonedaSheafCoproductTotalComplexFunctor X ⟶ (((ChainComplex.single₀ X.Modules).comp (ComplexShape.embeddingDownNat.extendFunctor X.Modules)).mapHomologicalComplex (ComplexShape.up ℤ)).comp (HomologicalComplex₂.totalFunctor X.Modules (ComplexShape.up ℤ) (ComplexShape.up ℤ) (ComplexShape.up ℤ))

Totalize the natural bicomplex augmentation. The target is the total complex of a bicomplex concentrated in resolution degree zero. A natural identification with the input is constructed below and compared with this map.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.Modules.freeYonedaSheafCoproductTotalTargetIso (X : Scheme) : (((ChainComplex.single₀ X.Modules).comp (ComplexShape.embeddingDownNat.extendFunctor X.Modules)).mapHomologicalComplex (ComplexShape.up ℤ)).comp (HomologicalComplex₂.totalFunctor X.Modules (ComplexShape.up ℤ) (ComplexShape.up ℤ) (ComplexShape.up ℤ)) ≅ CategoryTheory.Functor.id (CochainComplex X.Modules ℤ)

The original resolution-degree-zero total target is naturally the input, by specializing the generic extended-single total isomorphism at the resolution-degree embedding and degree zero.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.Modules.freeYonedaSheafCoproductTotalAugmentation (X : Scheme) : freeYonedaSheafCoproductTotalComplexFunctor X ⟶ CategoryTheory.Functor.id (CochainComplex X.Modules ℤ)

The natural augmentation of the total free-Yoneda resolution into the input complex. It totalizes the normalized bicomplex map and follows it by the signed single-zero comparison. No total quasi-isomorphism is inferred from the rowwise theorem.

Equations

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

theorem AlgebraicGeometry.Scheme.Modules.freeYonedaSheafCoproductTotalAugmentation_eq_toSingleZero_comp_targetIso (X : Scheme) : freeYonedaSheafCoproductTotalAugmentation X = CategoryTheory.CategoryStruct.comp (freeYonedaSheafCoproductTotalAugmentationToSingleZero X) (freeYonedaSheafCoproductTotalTargetIso X).hom

The earlier and normalized augmentations identify the single-zero target at different stages. After unfolding the generic comparison and distributing right whiskering over composition, the two maps are definitionally equal; downstream proofs can switch presentations by rewriting.

theorem AlgebraicGeometry.Scheme.Modules.freeYonedaSheafCoproductTotalComplexFunctor_obj_X_isFlatOverId (X : Scheme) (K : CochainComplex X.Modules ℤ) (n : ℤ) : IsFlatOver (CategoryTheory.CategoryStruct.id X) (((freeYonedaSheafCoproductTotalComplexFunctor X).obj K).X n)

Every term of the direct-sum total complex of the free-Yoneda resolution is flat over the identity of the scheme. This termwise statement supplies no K-flatness claim.

theorem AlgebraicGeometry.Scheme.Modules.isStrictlyLE_freeYonedaSheafCoproductTotalComplexFunctor_obj (X : Scheme) (M : CochainComplex X.Modules ℤ) (c : ℤ) [M.IsStrictlyLE c] : ((freeYonedaSheafCoproductTotalComplexFunctor X).obj M).IsStrictlyLE c

The free-Yoneda resolution total of a strictly bounded-above input remains strictly bounded above at the same term degree. The resolution contributes only nonpositive inner degrees; this is a term-support claim, not K-flatness.

theorem AlgebraicGeometry.Scheme.Modules.quasiIso_freeYonedaSheafCoproductTotalAugmentation_of_isStrictlyLE (X : Scheme) (M : CochainComplex X.Modules ℤ) (c : ℤ) [M.IsStrictlyLE c] : QuasiIso ((freeYonedaSheafCoproductTotalAugmentation X).app M)

The free-Yoneda total augmentation is a quasi-isomorphism for inputs whose terms vanish strictly above c. The cutoff and nonpositive resolution degree give finite support on each total diagonal.

theorem AlgebraicGeometry.Scheme.Modules.quasiIso_freeYonedaSheafCoproductTotalAugmentation_truncLE (X : Scheme) (M : CochainComplex X.Modules ℤ) (c : ℤ) : QuasiIso ((freeYonedaSheafCoproductTotalAugmentation X).app (M.truncLE c))

Good truncations are strictly bounded above, so the bounded augmentation theorem applies at each stage of the tower used for the unbounded result below.

theorem AlgebraicGeometry.Scheme.Modules.quasiIso_freeYonedaSheafCoproductTotalAugmentation (X : Scheme) (M : CochainComplex X.Modules ℤ) : QuasiIso ((freeYonedaSheafCoproductTotalAugmentation X).app M)

The free-Yoneda total augmentation is a quasi-isomorphism for every input complex. Both good-truncation cocones are colimiting, so exact filtered colimits preserve the stagewise quasi-isomorphisms and naturality identifies the resulting map with the original augmentation.