The derived effect of the non-flat affine witness

This file computes one concrete effect of extension of scalars along the non-flat map ℤ → ZMod 2. It gives an explicit two-term free resolution of ZMod 2, proves that its degreewise scalar extension has nonzero homology in degree -1, and identifies that calculation with the existing supported affine K-projective pullback on this representative.

Main definitions

• ZModTwoNonflatDerived.twoTermResolution is the explicit two-term free cochain resolution of ZMod 2 over ℤ.
• ZModTwoNonflatDerived.baseChangedResolution is its degreewise scalar extension along ℤ → ZMod 2.
• ZModTwoNonflatDerived.affineKProjectivePullbackObject is the existing supported affine K-projective pullback applied to this representative.

Main results

• twoTermAugmentation_quasiIso certifies the displayed resolution.
• baseChangedResolution_homology_negOne_not_isZero proves the explicit degree-minus-one effect after scalar extension.
• torOneIsoRestrictScalarsBaseChangedResolutionHomologyNegOne identifies the restricted degree-minus-one homology with Mathlib's fixed-left, derived-second-argument Tor for the displayed modules.
• affineKProjectivePullbackObject_homology_negOne_not_isZero transports the effect to the supported pullback object.
• affineKProjectiveSchemeModulePullbackObject_homology_negOne_not_isZero transports the effect through the affine K-projective scheme-module comparison.

Implementation notes

The calculation is deliberately affine and representative-level. It does not assert a general scheme-level left-derived pullback, preservation of a full Dqc locus, a relative-perfect preservation theorem, or a comparison with an unformalized classical invariant.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.ZModTwoNonflatDerived.twoTermResolution : CochainComplex (ModuleCat ℤ) ℤ

The explicit two-term free cochain resolution of ZMod 2 over ℤ.

Equations

• AlgebraicGeometry.DerivedCategory.Dqc.ZModTwoNonflatDerived.twoTermResolution = CochainComplex.mappingCone AlgebraicGeometry.DerivedCategory.Dqc.ZModTwoNonflatDerived.shortExactAtZero✝.f

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.ZModTwoNonflatDerived.twoTermAugmentation : twoTermResolution ⟶ AlgebraicGeometry.DerivedCategory.Dqc.ZModTwoNonflatDerived.singleAtZero✝.obj AlgebraicGeometry.DerivedCategory.Dqc.ZModTwoNonflatDerived.zmodTwoModule✝

The augmentation from the two-term free resolution to ZMod 2[0].

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Dqc.ZModTwoNonflatDerived.twoTermAugmentation_quasiIso : QuasiIso twoTermAugmentation

The explicit two-term augmentation is a quasi-isomorphism.

instance AlgebraicGeometry.DerivedCategory.Dqc.ZModTwoNonflatDerived.twoTermResolution_isStrictlyLE_zero : twoTermResolution.IsStrictlyLE 0

The resolution is strictly supported in degrees at most zero.

instance AlgebraicGeometry.DerivedCategory.Dqc.ZModTwoNonflatDerived.twoTermResolution_projective_X (n : ℤ) : CategoryTheory.Projective (twoTermResolution.X n)

Every term of the explicit resolution is projective.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.ZModTwoNonflatDerived.kProjectiveRepresentative : CategoryTheory.KProjectiveHomotopyCategory (ModuleCat ℤ)

The resolution as a K-projective representative.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.ZModTwoNonflatDerived.boundedAboveProjectiveRepresentative : CategoryTheory.BoundedAboveProjectiveHomotopyCategory (ModuleCat ℤ)

The same concrete complex in the supported bounded-above-projective lane.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.ZModTwoNonflatDerived.supportedAffineBoundedAboveProjectiveRepresentative : CategoryTheory.BoundedAboveProjectiveHomotopyCategory (ModuleCat (ZMod 2))

The supported affine bounded-above-projective representative after base change.

Equations

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

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.DerivedCategory.Dqc.ZModTwoNonflatDerived.baseChangedResolution : CochainComplex (ModuleCat (ZMod 2)) ℤ

The degreewise scalar extension of the explicit two-term resolution.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.ZModTwoNonflatDerived.affineKProjectivePullbackObject : DerivedCategory (ModuleCat (ZMod 2))

The supported affine K-projective pullback of the explicit representative.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.ZModTwoNonflatDerived.affineKProjectivePullbackObjectIso : affineKProjectivePullbackObject ≅ DerivedCategory.Q.obj baseChangedResolution

The supported K-projective pullback is computed by degreewise scalar extension here.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Dqc.ZModTwoNonflatDerived.baseChangedResolution_homology_negOne_not_isZero : ¬CategoryTheory.Limits.IsZero (HomologicalComplex.homology baseChangedResolution (-1))

Degreewise scalar extension of the explicit resolution has nonzero H^{-1}.

theorem AlgebraicGeometry.DerivedCategory.Dqc.ZModTwoNonflatDerived.affineKProjectivePullbackObject_homology_negOne_not_isZero : ¬CategoryTheory.Limits.IsZero ((DerivedCategory.homologyFunctor (ModuleCat (ZMod 2)) (-1)).obj affineKProjectivePullbackObject)

The supported affine K-projective pullback object of this resolution has nonzero H^{-1}.

theorem AlgebraicGeometry.DerivedCategory.Dqc.ZModTwoNonflatDerived.supportedAffineBoundedAboveProjectiveRepresentative_homology_negOne_not_isZero : ¬CategoryTheory.Limits.IsZero (supportedAffineBoundedAboveProjectiveRepresentative.obj.as.homology (-1))

The bounded-above-projective representative after affine base change has nonzero H^{-1}.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.ZModTwoNonflatDerived.schemeModulePulledBackResolution : CochainComplex (Spec zmodTwoRing).Modules ℤ

The actual degreewise scheme-module pullback of the sheafified two-term resolution along zmodTwoSchemeMap. This is an ordinary complex, before passing to the derived category.

Equations

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

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.ZModTwoNonflatDerived.schemeModulePulledBackResolutionIso : schemeModulePulledBackResolution ≅ ((tilde.functor zmodTwoRing).mapHomologicalComplex (ComplexShape.up ℤ)).obj baseChangedResolution

The actual scheme-module pullback complex is isomorphic to the tilde of the already computed scalar extension of the resolution.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Dqc.ZModTwoNonflatDerived.schemeModulePulledBackResolution_homology_negOne_not_isZero : ¬CategoryTheory.Limits.IsZero ((DerivedCategory.homologyFunctor (Spec zmodTwoRing).Modules (-1)).obj (DerivedCategory.Q.obj schemeModulePulledBackResolution))

The derived object represented by the degreewise, underived scheme-module pullback of the displayed resolution has nonzero H⁻¹.

theorem AlgebraicGeometry.DerivedCategory.Dqc.ZModTwoNonflatDerived.affineKProjectiveSchemeModulePullbackObject_homology_negOne_not_isZero : ¬CategoryTheory.Limits.IsZero ((DerivedCategory.homologyFunctor (Spec zmodTwoRing).Modules (-1)).obj ((tilde.functor zmodTwoRing).mapDerivedCategory.obj ((affineKProjectiveDerivedPullback zmodTwoRingMap).obj ((CategoryTheory.kProjectiveQhEquivalence (ModuleCat ℤ)).functor.obj kProjectiveRepresentative))))

The generic affine comparison carries the existing ℤ → ZMod 2 example's nonzero degree-minus-one cohomology to its derived target in all scheme-module sheaves.

noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.ZModTwoNonflatDerived.torOneIsoRestrictScalarsBaseChangedResolutionHomologyNegOne : (ModuleCat.restrictScalars (Int.castRingHom (ZMod 2))).obj (HomologicalComplex.homology baseChangedResolution (-1)) ≅ ((CategoryTheory.Tor (ModuleCat ℤ) 1).obj ((ModuleCat.restrictScalars (Int.castRingHom (ZMod 2))).obj (ModuleCat.of (ZMod 2) (ZMod 2)))).obj (ModuleCat.of ℤ (ZMod 2))

The affine degree-minus-one effect, after restriction of scalars, is Mathlib's fixed-left and derived-second-factor Tor for the displayed ℤ-modules.

Equations

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

theorem AlgebraicGeometry.DerivedCategory.Dqc.ZModTwoNonflatDerived.torOne_not_isZero : ¬CategoryTheory.Limits.IsZero (((CategoryTheory.Tor (ModuleCat ℤ) 1).obj ((ModuleCat.restrictScalars (Int.castRingHom (ZMod 2))).obj (ModuleCat.of (ZMod 2) (ZMod 2)))).obj (ModuleCat.of ℤ (ZMod 2)))

The concrete affine Tor₁ value is nonzero.