NYLL
Module

GeneratedAlgebraSource.lean

Nyll.SchemeTheory.Modules.GeneratedAlgebraSource
8 declarations indexed from sourceView source ↗

Module documentation

The original source maps to its generated relative algebra model

The inclusion of the actual generated section rings induces a map of the literal spectrum diagrams. The previously proved colimit with vertex the original affine-morphism source gives the scheme morphism. Its composite with the generated model's structure morphism is the original morphism. Consequently source surjectivity supplies surjectivity of the model.

Imports6
Imported by2

Declarations

instance

generatedDiagram_isLocallyDirected

L37 ↗
AlgebraicGeometry.Scheme.DirectImageAlgebra.generatedDiagram_isLocallyDirected
Source context 8 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite
namespace AlgebraicGeometry.Scheme.DirectImageAlgebra
variable {T X : Scheme.{u}} (g : T ⟶ X) [IsAffineHom g]
variable [(RelativeSpec.underlyingModule (structureMap g)).IsQuasicoherent]
variable (N : SheafOfModules.Submodule (RelativeSpec.underlyingModule (structureMap g)))
variable [(show X.Modules from N.toSheafOfModules).IsQuasicoherent]
Lean source · statement
instance generatedDiagram_isLocallyDirected :
    ((GeneratedAlgebra.gluingData (structureMap g) N).functor ⋙
      Scheme.forget).IsLocallyDirected
def

generatedDiagramMap

L44 ↗
AlgebraicGeometry.Scheme.DirectImageAlgebra.generatedDiagramMap
Documentation

The actual generated-ring inclusion, mapped contravariantly by Spec.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite
namespace AlgebraicGeometry.Scheme.DirectImageAlgebra
variable {T X : Scheme.{u}} (g : T ⟶ X) [IsAffineHom g]
variable [(RelativeSpec.underlyingModule (structureMap g)).IsQuasicoherent]
variable (N : SheafOfModules.Submodule (RelativeSpec.underlyingModule (structureMap g)))
variable [(show X.Modules from N.toSheafOfModules).IsQuasicoherent]
local instance generatedDiagram_isLocallyDirected :
    ((GeneratedAlgebra.gluingData (structureMap g) N).functor ⋙
      Scheme.forget).IsLocallyDirected :=
  Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin
    (GeneratedAlgebra.gluingData (structureMap g) N)
Lean source · statement
def generatedDiagramMap :
    AffineSourceColimit.diagram g ⟶ (GeneratedAlgebra.gluingData (structureMap g) N).functor
def

generatedCocone

L50 ↗
AlgebraicGeometry.Scheme.DirectImageAlgebra.generatedCocone
Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite
namespace AlgebraicGeometry.Scheme.DirectImageAlgebra
variable {T X : Scheme.{u}} (g : T ⟶ X) [IsAffineHom g]
variable [(RelativeSpec.underlyingModule (structureMap g)).IsQuasicoherent]
variable (N : SheafOfModules.Submodule (RelativeSpec.underlyingModule (structureMap g)))
variable [(show X.Modules from N.toSheafOfModules).IsQuasicoherent]
local instance generatedDiagram_isLocallyDirected :
    ((GeneratedAlgebra.gluingData (structureMap g) N).functor ⋙
      Scheme.forget).IsLocallyDirected :=
  Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin
    (GeneratedAlgebra.gluingData (structureMap g) N)
Lean source · full declaration
def generatedCocone : Cocone (AffineSourceColimit.diagram g) where
  pt := GeneratedAlgebra.scheme (structureMap g) N
  ι := generatedDiagramMap g N ≫
    (colimit.cocone (GeneratedAlgebra.gluingData (structureMap g) N).functor).ι
def

toGenerated

L57 ↗
AlgebraicGeometry.Scheme.DirectImageAlgebra.toGenerated
Documentation

The map from the original scheme source to the actual generated relative model, using the original source's proved colimit.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite
namespace AlgebraicGeometry.Scheme.DirectImageAlgebra
variable {T X : Scheme.{u}} (g : T ⟶ X) [IsAffineHom g]
variable [(RelativeSpec.underlyingModule (structureMap g)).IsQuasicoherent]
variable (N : SheafOfModules.Submodule (RelativeSpec.underlyingModule (structureMap g)))
variable [(show X.Modules from N.toSheafOfModules).IsQuasicoherent]
local instance generatedDiagram_isLocallyDirected :
    ((GeneratedAlgebra.gluingData (structureMap g) N).functor ⋙
      Scheme.forget).IsLocallyDirected :=
  Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin
    (GeneratedAlgebra.gluingData (structureMap g) N)
Lean source · statement
def toGenerated : T ⟶ GeneratedAlgebra.scheme (structureMap g) N
theorem

fromSpec_toGenerated

L63 ↗
AlgebraicGeometry.Scheme.DirectImageAlgebra.fromSpec_toGenerated
Documentation

On a literal source affine chart, the new morphism is Spec of the actual inclusion of generated sections.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite
namespace AlgebraicGeometry.Scheme.DirectImageAlgebra
variable {T X : Scheme.{u}} (g : T ⟶ X) [IsAffineHom g]
variable [(RelativeSpec.underlyingModule (structureMap g)).IsQuasicoherent]
variable (N : SheafOfModules.Submodule (RelativeSpec.underlyingModule (structureMap g)))
variable [(show X.Modules from N.toSheafOfModules).IsQuasicoherent]
local instance generatedDiagram_isLocallyDirected :
    ((GeneratedAlgebra.gluingData (structureMap g) N).functor ⋙
      Scheme.forget).IsLocallyDirected :=
  Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin
    (GeneratedAlgebra.gluingData (structureMap g) N)
Lean source · statement
theorem fromSpec_toGenerated (U : X.AffineZariskiSite) :
    (U.2.preimage g).fromSpec ≫ toGenerated g N =
      Spec.map ((GeneratedAlgebra.inclusion (structureMap g) N.toSubmodule).app (op U.1)) ≫
        colimit.ι (GeneratedAlgebra.gluingData (structureMap g) N).functor U
theorem

generatedChart_toBase

L70 ↗
AlgebraicGeometry.Scheme.DirectImageAlgebra.generatedChart_toBase
Source context 10 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite
namespace AlgebraicGeometry.Scheme.DirectImageAlgebra
variable {T X : Scheme.{u}} (g : T ⟶ X) [IsAffineHom g]
variable [(RelativeSpec.underlyingModule (structureMap g)).IsQuasicoherent]
variable (N : SheafOfModules.Submodule (RelativeSpec.underlyingModule (structureMap g)))
variable [(show X.Modules from N.toSheafOfModules).IsQuasicoherent]
local instance generatedDiagram_isLocallyDirected :
    ((GeneratedAlgebra.gluingData (structureMap g) N).functor ⋙
      Scheme.forget).IsLocallyDirected :=
  Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin
    (GeneratedAlgebra.gluingData (structureMap g) N)
omit [IsAffineHom g] in
Lean source · statement
theorem generatedChart_toBase (U : X.AffineZariskiSite) :
    colimit.ι (GeneratedAlgebra.gluingData (structureMap g) N).functor U ≫
        GeneratedAlgebra.toBase (structureMap g) N =
      Spec.map ((GeneratedAlgebra.structureMap (structureMap g) N.toSubmodule).app (op U.1)) ≫
        U.2.fromSpec
theorem

toGenerated_toBase

L87 ↗
AlgebraicGeometry.Scheme.DirectImageAlgebra.toGenerated_toBase
Documentation

The actual original source morphism factors through the generated model.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite
namespace AlgebraicGeometry.Scheme.DirectImageAlgebra
variable {T X : Scheme.{u}} (g : T ⟶ X) [IsAffineHom g]
variable [(RelativeSpec.underlyingModule (structureMap g)).IsQuasicoherent]
variable (N : SheafOfModules.Submodule (RelativeSpec.underlyingModule (structureMap g)))
variable [(show X.Modules from N.toSheafOfModules).IsQuasicoherent]
local instance generatedDiagram_isLocallyDirected :
    ((GeneratedAlgebra.gluingData (structureMap g) N).functor ⋙
      Scheme.forget).IsLocallyDirected :=
  Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin
    (GeneratedAlgebra.gluingData (structureMap g) N)
Lean source · statement
theorem toGenerated_toBase :
    toGenerated g N ≫ GeneratedAlgebra.toBase (structureMap g) N = g
theorem

surjective_toBase

L128 ↗
AlgebraicGeometry.Scheme.DirectImageAlgebra.surjective_toBase
Documentation

Surjectivity of the original morphism gives surjectivity of the actual generated model's structure map.

Source context 9 commands

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

noncomputable section
universe u
open CategoryTheory Limits Opposite
namespace AlgebraicGeometry.Scheme.DirectImageAlgebra
variable {T X : Scheme.{u}} (g : T ⟶ X) [IsAffineHom g]
variable [(RelativeSpec.underlyingModule (structureMap g)).IsQuasicoherent]
variable (N : SheafOfModules.Submodule (RelativeSpec.underlyingModule (structureMap g)))
variable [(show X.Modules from N.toSheafOfModules).IsQuasicoherent]
local instance generatedDiagram_isLocallyDirected :
    ((GeneratedAlgebra.gluingData (structureMap g) N).functor ⋙
      Scheme.forget).IsLocallyDirected :=
  Cover.RelativeGluingData.instIsLocallyDirectedI₀CompFunctorForgetOfIsThin
    (GeneratedAlgebra.gluingData (structureMap g) N)
Lean source · statement
theorem surjective_toBase [Surjective g] :
    Surjective (GeneratedAlgebra.toBase (structureMap g) N)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.