Stalkwise-flat generators for scheme module sheaves

The free-Yoneda module sheaf attached to an open U has stalk zero away from U. The inside-support stalk calculation identifies the module stalk with the local ring; together these results prove stalkwise flatness. The generic natural element-indexed epimorphism is specialized to X.Modules below without introducing another generator construction.

This gives a functorial left resolution of individual sheaves by stalkwise-flat objects. It does not assert projectivity or construct K-flat replacements of unbounded complexes.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Scheme.Modules.freeYonedaModuleSheaf (X : Scheme) (U : X.Opens) : X.Modules

The canonical free-Yoneda 𝒪_X-module sheaf associated to an open subset.

Equations

• AlgebraicGeometry.Scheme.Modules.freeYonedaModuleSheaf X U = SheafOfModules.freeYonedaSheaf X.ringCatSheaf U

noncomputable def AlgebraicGeometry.Scheme.Modules.freeYonedaModuleSheafStalkIsoRegularOfMem (X : Scheme) (U : X.Opens) (x : ↥X) (hx : x ∈ U) : (moduleStalkFunctor X x).obj (freeYonedaModuleSheaf X U) ≅ ModuleCat.of ↑(X.presheaf.stalk x) ↑(X.presheaf.stalk x)

On an open containing x, the stalk of the free-Yoneda module sheaf is the regular module over the local ring.

Equations

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

theorem AlgebraicGeometry.Scheme.Modules.freeYonedaModuleSheaf_stalk_flat_of_mem (X : Scheme) (U : X.Opens) (x : ↥X) (hx : x ∈ U) : Module.Flat ↑(X.presheaf.stalk x) ↑((moduleStalkFunctor X x).obj (freeYonedaModuleSheaf X U))

On an open containing x, the free-Yoneda module sheaf is flat at the stalk.

theorem AlgebraicGeometry.Scheme.Modules.freeYonedaModuleSheaf_stalk_isZero_of_not_mem (X : Scheme) (U : X.Opens) (x : ↥X) (hx : x ∉ U) : CategoryTheory.Limits.IsZero ((moduleStalkFunctor X x).obj (freeYonedaModuleSheaf X U))

The stalk at x of the free-Yoneda sheaf on an open not containing x is zero.

theorem AlgebraicGeometry.Scheme.Modules.freeYonedaModuleSheaf_stalk_flat_of_not_mem (X : Scheme) (U : X.Opens) (x : ↥X) (hx : x ∉ U) : Module.Flat ↑(X.presheaf.stalk x) ↑((moduleStalkFunctor X x).obj (freeYonedaModuleSheaf X U))

Away from its representing open, the free-Yoneda module sheaf is flat at the stalk.

theorem AlgebraicGeometry.Scheme.Modules.freeYonedaModuleSheaf_stalk_flat (X : Scheme) (U : X.Opens) (x : ↥X) : Module.Flat ↑(X.presheaf.stalk x) ↑((moduleStalkFunctor X x).obj (freeYonedaModuleSheaf X U))

Every stalk of a free-Yoneda module sheaf on an open is flat over the local ring.

theorem AlgebraicGeometry.Scheme.Modules.freeYonedaModuleSheaf_isFlatOver_id (X : Scheme) (U : X.Opens) : IsFlatOver (CategoryTheory.CategoryStruct.id X) (freeYonedaModuleSheaf X U)

The canonical free-Yoneda module sheaf on an open is flat over the identity map.

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Scheme.Modules.freeYonedaSheafCoproduct (X : Scheme) (M : X.Modules) : X.Modules

The generic element-indexed coproduct, specialized to X.Modules.

Its indexing type is M.val.Elements : Type u; the coproduct is the one defined at the small-ringed-site owner, not a second geometric presentation.

Equations

• AlgebraicGeometry.Scheme.Modules.freeYonedaSheafCoproduct X M = SheafOfModules.freeYonedaSheafCoproduct X.ringCatSheaf (have this := M; this)

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Scheme.Modules.fromFreeYonedaSheafCoproduct (X : Scheme) (M : X.Modules) : freeYonedaSheafCoproduct X M ⟶ M

The generic epimorphism from the element-indexed free-Yoneda coproduct, specialized to X.Modules.

Equations

• AlgebraicGeometry.Scheme.Modules.fromFreeYonedaSheafCoproduct X M = SheafOfModules.fromFreeYonedaSheafCoproduct X.ringCatSheaf (have this := M; this)

noncomputable def AlgebraicGeometry.Scheme.Modules.freeYonedaSheafCoproductMap (X : Scheme) {M N : X.Modules} (f : M ⟶ N) : freeYonedaSheafCoproduct X M ⟶ freeYonedaSheafCoproduct X N

The map on specialized coproducts induced by a morphism, inherited from the generic root.

Equations

• AlgebraicGeometry.Scheme.Modules.freeYonedaSheafCoproductMap X f = SheafOfModules.freeYonedaSheafCoproductMap X.ringCatSheaf (have this := f; this)

theorem AlgebraicGeometry.Scheme.Modules.fromFreeYonedaSheafCoproduct_epi (X : Scheme) (M : X.Modules) : CategoryTheory.Epi (fromFreeYonedaSheafCoproduct X M)

The element-indexed free-Yoneda coproduct epimorphism in X.Modules.

theorem AlgebraicGeometry.Scheme.Modules.freeYonedaSheafCoproduct_summand_stalk_flat (X : Scheme) (M : X.Modules) (m : M.val.Elements) (x : ↥X) : Module.Flat ↑(X.presheaf.stalk x) ↑((moduleStalkFunctor X x).obj (SheafOfModules.Elements.freeYonedaSheaf X.ringCatSheaf m))

Every element-indexed summand of the canonical presentation has flat stalks.

theorem AlgebraicGeometry.Scheme.Modules.freeYonedaSheafCoproduct_stalk_flat (X : Scheme) (M : X.Modules) (x : ↥X) : Module.Flat ↑(X.presheaf.stalk x) ↑((moduleStalkFunctor X x).obj (freeYonedaSheafCoproduct X M))

The stalks of the element-indexed free-Yoneda coproduct are flat because its summands are flat over the identity and that property is closed under coproducts.

noncomputable def AlgebraicGeometry.Scheme.Modules.freeYonedaSheafCoproductLeftResolution (X : Scheme) : CategoryTheory.Abelian.LeftResolution (CategoryTheory.ObjectProperty.ι fun (M : X.Modules) => IsFlatOver (CategoryTheory.CategoryStruct.id X) M)

The element-indexed free-Yoneda coproduct defines a Mathlib left resolution of every module sheaf by sheaves flat over the identity of X.

Applying CategoryTheory.Abelian.LeftResolution.chainComplexFunctor yields the functorial nonnegative resolution in the full subcategory cut out by AlgebraicGeometry.Scheme.Modules.IsFlatOver (𝟙 X). This is an objectwise resolution; it is not a K-flat replacement functor on unbounded complexes.

Equations

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

noncomputable def AlgebraicGeometry.Scheme.Modules.freeYonedaSheafCoproductReducedLeftResolution (X : Scheme) : CategoryTheory.Abelian.LeftResolution (CategoryTheory.ObjectProperty.ι fun (M : X.Modules) => IsFlatOver (CategoryTheory.CategoryStruct.id X) M)

The free-Yoneda resolution refined by Mathlib's CategoryTheory.Abelian.LeftResolution.reduced; its reduced functor preserves zero morphisms. This still gives an objectwise resolution, not a K-flat replacement on unbounded complexes.

Equations

• AlgebraicGeometry.Scheme.Modules.freeYonedaSheafCoproductReducedLeftResolution X = (AlgebraicGeometry.Scheme.Modules.freeYonedaSheafCoproductLeftResolution X).reduced

instance AlgebraicGeometry.Scheme.Modules.freeYonedaSheafCoproductReducedLeftResolution_preservesZeroMorphisms (X : Scheme) : (freeYonedaSheafCoproductReducedLeftResolution X).F.PreservesZeroMorphisms

The zero-preserving refinement is the additive input needed to apply this objectwise resolution functor term-by-term to homological complexes.

theorem AlgebraicGeometry.Scheme.Modules.freeYonedaSheafCoproductReducedLeftResolution_chainComplexMap_zero (X : Scheme) {M N : X.Modules} : (freeYonedaSheafCoproductReducedLeftResolution X).chainComplexMap 0 = 0

This zero-map lemma supplies the preservation instance required by CategoryTheory.Functor.mapHomologicalComplex for the induced resolution functor.

noncomputable def AlgebraicGeometry.Scheme.Modules.freeYonedaSheafCoproductResolutionBicomplex (X : Scheme) : CategoryTheory.Functor (CochainComplex X.Modules ℤ) (HomologicalComplex (ChainComplex (CategoryTheory.ObjectProperty.FullSubcategory fun (M : X.Modules) => IsFlatOver (CategoryTheory.CategoryStruct.id X) M) ℕ) (ComplexShape.up ℤ))

Applying the reduced free-Yoneda resolution to each term of an unbounded cochain complex gives a functorial complex of nonnegative flat resolutions. This records the bicomplex before totalization; it does not assert that the total complex is K-flat or that pullback preserves quasi-isomorphisms.

Equations

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

theorem AlgebraicGeometry.Scheme.Modules.freeYonedaSheafCoproductResolutionBicomplex_exactAt_succ (X : Scheme) (K : CochainComplex X.Modules ℤ) (i : ℤ) (n : ℕ) : (((CategoryTheory.ObjectProperty.ι fun (M : X.Modules) => IsFlatOver (CategoryTheory.CategoryStruct.id X) M).mapHomologicalComplex (ComplexShape.down ℕ)).obj (((freeYonedaSheafCoproductResolutionBicomplex X).obj K).X i)).ExactAt (n + 1)

Every row of the resolution bicomplex is exact in positive resolution degrees after inclusion into all module sheaves. Degree zero is only the one-step free cover, so this result does not identify the total complex with the original complex.

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

Resolve each term of an unbounded cochain complex by the zero-preserving free-Yoneda flat cover. This is the degree-zero column of the resolution bicomplex; its natural map to the input is proved epi, but this does not establish a quasi-isomorphism.

Equations

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

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

The natural augmentation of the termwise flat cover, induced by the epimorphisms in the objectwise CategoryTheory.Abelian.LeftResolution.

Equations

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

theorem AlgebraicGeometry.Scheme.Modules.freeYonedaSheafCoproductDegreewiseEpiCoverMap_epi (X : Scheme) (K : CochainComplex X.Modules ℤ) : CategoryTheory.Epi ((freeYonedaSheafCoproductDegreewiseEpiCoverMap X).app K)

The termwise augmentation is epi in every complex degree. It does not identify the termwise cover as a quasi-isomorphic replacement.

theorem AlgebraicGeometry.Scheme.Modules.freeYonedaSheafCoproductReducedLeftResolution_augmentedExact (X : Scheme) (M : X.Modules) : (CategoryTheory.Abelian.LeftResolution.augmentedShortComplex (CategoryTheory.ObjectProperty.ι fun (M : X.Modules) => IsFlatOver (CategoryTheory.CategoryStruct.id X) M) (freeYonedaSheafCoproductReducedLeftResolution X) M).Exact

The augmented first segment of the free-Yoneda flat resolution is exact after inclusion into all module sheaves. This objectwise fact does not identify the total complex of the resolution bicomplex with its input.

noncomputable def AlgebraicGeometry.Scheme.Modules.freeYonedaSheafCoproductReducedLeftResolutionHomologyZeroIso (X : Scheme) (M : X.Modules) : (((CategoryTheory.ObjectProperty.ι fun (M : X.Modules) => IsFlatOver (CategoryTheory.CategoryStruct.id X) M).mapHomologicalComplex (ComplexShape.down ℕ)).obj ((freeYonedaSheafCoproductReducedLeftResolution X).chainComplex M)).homology 0 ≅ M

The objectwise free-Yoneda left resolution has degree-zero homology M after inclusion into all module sheaves. This does not identify the totalized resolution of a complex with that complex.

Equations

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

theorem AlgebraicGeometry.Scheme.Modules.fromFreeYonedaSheafCoproduct_natural (X : Scheme) {M N : X.Modules} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (freeYonedaSheafCoproductMap X f) (fromFreeYonedaSheafCoproduct X N) = CategoryTheory.CategoryStruct.comp (fromFreeYonedaSheafCoproduct X M) f

Naturality of the specialized coproduct map follows from the generic naturality theorem.