Documentation

DerivedAlgGeo.AlgebraicGeometry.DerivedCategory.Dqc.AffineNonflatExample

A supported non-flat affine derived pullback #

This file supplies the concrete example required by SF8.5 item 9. The ring map ℤ → ZMod 2 is a non-isomorphism and is not flat, while the existing geometric affine bounded-above-projective core pseudofunctor constructs its pullback without a flatness hypothesis.

This is deliberately an example, not an existence theorem for arbitrary scheme-module resolutions. It consumes the supported affine K-projective-derived lane already constructed in AffineGeometricCorePseudofunctor.lean; it does not identify that lane with the full relative-perfect locus or prove the general-scheme preservation theorems still listed in #554.

AffineNonflatDerivedObject.lean separately computes the degree-minus-one effect of this particular map on an explicit two-term free representative. That calculation remains in the same affine bounded-projective lane and does not enlarge this example into a scheme-level assertion.

source
@[reducible, inline]
abbrev AlgebraicGeometry.DerivedCategory.Dqc.zmodTwoRing :
CommRingCat

The target ring in the standard closed-immersion example.

Equations
Instances For
    source
    def AlgebraicGeometry.DerivedCategory.Dqc.zmodTwoRingMap :
    CommRingCat.of ℤ ⟶ zmodTwoRing

    The nonidentity ring morphism ℤ → ZMod 2.

    Equations
    Instances For
      source
      noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.zmodTwoSchemeMap :
      Spec zmodTwoRing ⟶ Spec (CommRingCat.of ℤ)

      The corresponding morphism of affine schemes.

      Equations
      Instances For
        source
        theorem AlgebraicGeometry.DerivedCategory.Dqc.zmodTwoRingMap_not_flat :
        ¬(CommRingCat.Hom.hom zmodTwoRingMap).Flat

        The closed-immersion ring map is not flat.

        Flatness would make the ℤ-module ZMod 2 torsion-free, but 2 • 1 = 0 while both the scalar 2 and the element 1 are nonzero.

        source
        theorem AlgebraicGeometry.DerivedCategory.Dqc.zmodTwoSchemeMap_not_flat :
        ¬Flat zmodTwoSchemeMap

        The corresponding affine-scheme morphism is not flat.

        source
        theorem AlgebraicGeometry.DerivedCategory.Dqc.zmodTwoRingMap_not_iso :
        ¬CategoryTheory.IsIso zmodTwoRingMap

        The example is genuinely nonidentity: its ring map is not an isomorphism.

        source
        noncomputable def AlgebraicGeometry.DerivedCategory.Dqc.zmodTwoAffinePullback :
        CategoryTheory.Functor (AffineBoundedAboveProjectiveModuliFiber (CommRingCat.of ℤ)) (AffineBoundedAboveProjectiveModuliFiber zmodTwoRing)

        The actual supported affine derived pullback along the non-flat example.

        The source and target are the already-defined geometric affine moduli fibers; the construction therefore has no caller-supplied flatness or exactness hypothesis.

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