Documentation

TauCeti.AlgebraicGeometry.VectorBundle.Affine.Basic

Finite locally free sheaves on an affine scheme #

For a commutative ring R, Mathlib's equivalence AlgebraicGeometry.tildeEquiv identifies R-modules with quasicoherent sheaves on Spec R by M ↦ M~, with inverse the global sections. It restricts to an equivalence between finitely generated projective R-modules and finite locally free sheaves on Spec R.

The sheaf M~ is finite locally free exactly when M is finitely generated and projective. One direction is TauCeti.AlgebraicGeometry.isFiniteLocallyFree_tilde. Conversely, a finite locally free sheaf is dualizable in the category of quasicoherent sheaves, and the dualizable quasicoherent sheaves on Spec R are those whose global sections are finitely generated and projective (TauCeti.AlgebraicGeometry.QuasicoherentSheaf.nonempty_hasLeftDual_iff_finite_projective).

Under this equivalence, the rank of a finite locally free sheaf at a prime p is the rank of the free R_p-module M_p (Mathlib's Module.rankAtStalk). Indeed, the pullback of M~ along Spec R_p ⟶ Spec R is the sheaf associated with R_p ⊗_R M ≅ M_p, hence free on a basis of M_p, and its rank at the closed point is the rank of M~ at p.

Main declarations #

References #

source
theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.finite_projective_moduleSpecΓ {R : CommRingCat} (E : FiniteLocallyFreeSheaf (AlgebraicGeometry.Spec R)) :
Module.Finite ↑R ↑(AlgebraicGeometry.moduleSpecΓFunctor.obj E.obj) ∧ Module.Projective ↑R ↑(AlgebraicGeometry.moduleSpecΓFunctor.obj E.obj)

The global sections of a finite locally free sheaf on Spec R form a finitely generated projective R-module.

source
theorem TauCeti.AlgebraicGeometry.isFiniteLocallyFree_tilde_iff {R : CommRingCat} (M : ModuleCat ↑R) :
AlgebraicGeometry.Scheme.Modules.isFiniteLocallyFree (AlgebraicGeometry.Spec R) (AlgebraicGeometry.tilde M) ↔ Module.Finite ↑R ↑M ∧ Module.Projective ↑R ↑M

The sheaf M~ on Spec R associated with an R-module M is finite locally free if and only if M is finitely generated and projective.

source
noncomputable def TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.finiteProjectiveEquiv (R : CommRingCat) :
(finiteProjectiveModules ↑R).FullSubcategory ≌ FiniteLocallyFreeSheaf (AlgebraicGeometry.Spec R)

Finitely generated projective R-modules are equivalent to finite locally free sheaves on Spec R, by M ↦ M~ with inverse the global sections. This is the restriction of Mathlib's AlgebraicGeometry.tildeEquiv to these full subcategories.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.finiteProjectiveEquiv_unitIso_hom_app_hom (R : CommRingCat) (X : (finiteProjectiveModules ↑R).FullSubcategory) :
    ((finiteProjectiveEquiv R).unitIso.hom.app X).hom = AlgebraicGeometry.tilde.toTildeΓNatIso.hom.app X.obj
    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.finiteProjectiveEquiv_functor_obj_obj (R : CommRingCat) (X : (finiteProjectiveModules ↑R).FullSubcategory) :
    ((finiteProjectiveEquiv R).functor.obj X).obj = AlgebraicGeometry.tilde X.obj
    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.finiteProjectiveEquiv_inverse_map_hom (R : CommRingCat) {X✝ Y✝ : FiniteLocallyFreeSheaf (AlgebraicGeometry.Spec R)} (f : X✝ ⟶ Y✝) :
    ((finiteProjectiveEquiv R).inverse.map f).hom = AlgebraicGeometry.moduleSpecΓFunctor.map f.hom
    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.finiteProjectiveEquiv_functor_map_hom (R : CommRingCat) {X✝ Y✝ : (finiteProjectiveModules ↑R).FullSubcategory} (f : X✝ ⟶ Y✝) :
    ((finiteProjectiveEquiv R).functor.map f).hom = AlgebraicGeometry.tilde.map f.hom
    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.finiteProjectiveEquiv_inverse_obj_obj (R : CommRingCat) (X : FiniteLocallyFreeSheaf (AlgebraicGeometry.Spec R)) :
    ((finiteProjectiveEquiv R).inverse.obj X).obj = AlgebraicGeometry.moduleSpecΓFunctor.obj X.obj
    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.finiteProjectiveEquiv_counitIso_hom_app_hom {R : CommRingCat} (E : FiniteLocallyFreeSheaf (AlgebraicGeometry.Spec R)) :
    ((finiteProjectiveEquiv R).counitIso.hom.app E).hom = E.obj.fromTildeΓ

    The counit of finiteProjectiveEquiv is the canonical isomorphism from the sheaf associated with the global sections of a finite locally free sheaf to the sheaf itself.

    source
    @[simp]
    theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.rank_finiteProjectiveEquiv_functor_obj_apply {R : CommRingCat} (M : (finiteProjectiveModules ↑R).FullSubcategory) (p : ↥(AlgebraicGeometry.Spec R)) :
    ((finiteProjectiveEquiv R).functor.obj M).rank p = Module.rankAtStalk (↑M.obj) p

    The rank of the sheaf M~ associated with a finitely generated projective R-module M at a prime p is the rank of the free R_p-module M_p.

    source
    theorem TauCeti.AlgebraicGeometry.FiniteLocallyFreeSheaf.rank_apply_eq_rankAtStalk {R : CommRingCat} (E : FiniteLocallyFreeSheaf (AlgebraicGeometry.Spec R)) (p : ↥(AlgebraicGeometry.Spec R)) :
    E.rank p = Module.rankAtStalk (↑(AlgebraicGeometry.moduleSpecΓFunctor.obj E.obj)) p

    The rank of a finite locally free sheaf E on Spec R at a prime p is the rank at p of its module of global sections.