Module

DirectImageAlgebraQuasicoherent.lean

Nyll.SchemeTheory.Modules.DirectImageAlgebraQuasicoherent

2 declarations indexed from sourceView source ↗

Module documentation

Quasicoherence of the actual affine direct-image algebra

The unit sheaf is the one-generator free sheaf. Affine pushforward preserves its quasicoherence, and the actual direct-image algebra/module comparison identifies the resulting module with the algebra's underlying module.

Imports4

Nyll.SchemeTheory.Modules.DirectImageAlgebra
Nyll.SchemeTheory.Modules.QuasicoherentPushforward
Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree
Mathlib.CategoryTheory.Limits.Shapes.Products

Imported by2

theorem

isQuasicoherent_unit

L30 ↗

AlgebraicGeometry.Scheme.Modules.isQuasicoherent_unit

Documentation

The actual structure-sheaf unit module is quasicoherent, by its isomorphism with the one-generator free sheaf.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme

Lean source · full declaration

theorem Modules.isQuasicoherent_unit (T : Scheme.{u}) :
    (show T.Modules from SheafOfModules.unit T.ringCatSheaf).IsQuasicoherent := by
  let M : T.Modules := SheafOfModules.free (R := T.ringCatSheaf) PUnit.{u + 1}
  have hM : M.IsQuasicoherent := inferInstance
  let e : M ≅ SheafOfModules.unit T.ringCatSheaf :=
    coproductUniqueIso (fun _ : PUnit.{u + 1} => SheafOfModules.unit T.ringCatSheaf)
  exact (SheafOfModules.isQuasicoherent T.ringCatSheaf).prop_of_iso e hM

theorem

isQuasicoherent_underlyingModule

L42 ↗

AlgebraicGeometry.Scheme.DirectImageAlgebra.isQuasicoherent_underlyingModule

Documentation

An affine morphism's actual direct-image ring algebra has a quasicoherent underlying module. No direct-image QC premise is required.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
universe u
open CategoryTheory Limits
namespace AlgebraicGeometry.Scheme
namespace DirectImageAlgebra

Lean source · statement

theorem isQuasicoherent_underlyingModule {T X : Scheme.{u}}
    (g : T ⟶ X) [IsAffineHom g] :
    (RelativeSpec.underlyingModule (structureMap g)).IsQuasicoherent

Module documentation

Quasicoherence of the actual affine direct-image algebra

Declarations

isQuasicoherent_unit

isQuasicoherent_underlyingModule