NYLL
Module

GeneratedAlgebraPresheaf.lean

Nyll.SchemeTheory.Modules.GeneratedAlgebraPresheaf
10 declarations indexed from sourceView source ↗

Module documentation

The algebra presheaf generated by an actual submodule

Given an actual sheaf of commutative algebras and a submodule of its underlying module presheaf, generate the section subring from the structure coefficients and the given submodule sections. Restriction is the literal ambient ring restriction. Its stability and functor laws are proved, not provided as compatibility fields.

On the affine site this is the ring diagram for relative gluing. This file does not yet prove its coequifibered property or extend local submodules.

Imports4
Imported by2

Declarations

def

sectionSubmodule

L39 ↗
AlgebraicGeometry.Scheme.GeneratedAlgebra.sectionSubmodule
Documentation

The actual submodule of the algebra section ring. The coefficient action is the same restriction of scalars used by underlyingModule.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.GeneratedAlgebra
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
variable (α : X.sheaf ⟶ A)
variable (N : (RelativeSpec.underlyingModule α).val.Submodule)
Lean source · full declaration
def sectionSubmodule (U : X.Opensᵒᵖ) :
    let : Algebra (X.presheaf.obj U) (A.obj.obj U) := (α.hom.app U).hom.toAlgebra
    Submodule (X.presheaf.obj U) (A.obj.obj U) := by
  intro algebra
  change Submodule (X.ringCatSheaf.obj.obj U) ((RelativeSpec.underlyingModule α).val.obj U)
  exact N.obj U
def

sectionSubring

L47 ↗
AlgebraicGeometry.Scheme.GeneratedAlgebra.sectionSubring
Documentation

The actual generated section subring, inside the original section ring.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.GeneratedAlgebra
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
variable (α : X.sheaf ⟶ A)
variable (N : (RelativeSpec.underlyingModule α).val.Submodule)
Lean source · statement
def sectionSubring (U : X.Opensᵒᵖ) : Subring (A.obj.obj U)
theorem

restriction_mem

L54 ↗
AlgebraicGeometry.Scheme.GeneratedAlgebra.restriction_mem
Documentation

Restriction preserves the generated subrings by naturality of the structure map and stability of the given submodule.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.GeneratedAlgebra
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
variable (α : X.sheaf ⟶ A)
variable (N : (RelativeSpec.underlyingModule α).val.Submodule)
Lean source · statement
theorem restriction_mem {U V : X.Opensᵒᵖ} (i : U ⟶ V) :
    ∀ x ∈ sectionSubring α N U, A.obj.map i x ∈ sectionSubring α N V
def

presheaf

L69 ↗
AlgebraicGeometry.Scheme.GeneratedAlgebra.presheaf
Documentation

The ring presheaf whose sections are generated by the actual submodule.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.GeneratedAlgebra
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
variable (α : X.sheaf ⟶ A)
variable (N : (RelativeSpec.underlyingModule α).val.Submodule)
Lean source · full declaration
def presheaf : X.Opensᵒᵖ ⥤ CommRingCat.{u} where
  obj U := CommRingCat.of (sectionSubring α N U)
  map {U V} i := CommRingCat.ofHom
    ((A.obj.map i).hom.restrict (sectionSubring α N U) (sectionSubring α N V)
      (restriction_mem α N i))
  map_id U := by
    apply CommRingCat.hom_ext
    apply RingHom.ext
    intro x
    apply Subtype.ext
    exact congrArg (fun k : A.obj.obj U ⟶ A.obj.obj U => k x.val) (A.obj.map_id U)
  map_comp i j := by
    apply CommRingCat.hom_ext
    apply RingHom.ext
    intro x
    apply Subtype.ext
    exact congrArg (fun k => k x.val) (A.obj.map_comp i j)
def

inclusion

L88 ↗
AlgebraicGeometry.Scheme.GeneratedAlgebra.inclusion
Documentation

Inclusion of the generated ring presheaf into the original algebra.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.GeneratedAlgebra
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
variable (α : X.sheaf ⟶ A)
variable (N : (RelativeSpec.underlyingModule α).val.Submodule)
Lean source · full declaration
def inclusion : presheaf α N ⟶ A.obj where
  app U := CommRingCat.ofHom (sectionSubring α N U).subtype
  naturality {U V} i := by
    apply CommRingCat.hom_ext
    apply RingHom.ext
    intro x
    rfl
def

structureMap

L97 ↗
AlgebraicGeometry.Scheme.GeneratedAlgebra.structureMap
Documentation

The original structure map lands in the generated rings.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.GeneratedAlgebra
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
variable (α : X.sheaf ⟶ A)
variable (N : (RelativeSpec.underlyingModule α).val.Submodule)
Lean source · full declaration
def structureMap : X.presheaf ⟶ presheaf α N where
  app U := CommRingCat.ofHom
    ((α.hom.app U).hom.codRestrict (sectionSubring α N U)
      (fun r => Subring.subset_closure (Or.inl ⟨r, rfl⟩)))
  naturality {U V} i := by
    apply CommRingCat.hom_ext
    apply RingHom.ext
    intro r
    apply Subtype.ext
    exact congrArg (fun k : X.presheaf.obj U ⟶ A.obj.obj V => k r)
      (α.hom.naturality i)
theorem

structureMap_inclusion

L110 ↗
AlgebraicGeometry.Scheme.GeneratedAlgebra.structureMap_inclusion
Documentation

Inclusion recovers the given structure map exactly.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.GeneratedAlgebra
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
variable (α : X.sheaf ⟶ A)
variable (N : (RelativeSpec.underlyingModule α).val.Submodule)
Lean source · statement
theorem structureMap_inclusion : structureMap α N ≫ inclusion α N = α.hom
def

affinePresheaf

L119 ↗
AlgebraicGeometry.Scheme.GeneratedAlgebra.affinePresheaf
Documentation

The generated ring diagram on the actual affine Zariski site.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.GeneratedAlgebra
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
variable (α : X.sheaf ⟶ A)
variable (N : (RelativeSpec.underlyingModule α).val.Submodule)
Lean source · statement
def affinePresheaf : X.AffineZariskiSiteᵒᵖ ⥤ CommRingCat.{u}
def

affineStructureMap

L123 ↗
AlgebraicGeometry.Scheme.GeneratedAlgebra.affineStructureMap
Documentation

The actual affine structure map used by native relative gluing.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.GeneratedAlgebra
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
variable (α : X.sheaf ⟶ A)
variable (N : (RelativeSpec.underlyingModule α).val.Submodule)
Lean source · statement
def affineStructureMap :
    (AffineZariskiSite.toOpensFunctor X).op ⋙ X.presheaf ⟶ affinePresheaf α N
theorem

sectionSubring_eq_adjoin

L129 ↗
AlgebraicGeometry.Scheme.GeneratedAlgebra.sectionSubring_eq_adjoin
Documentation

Under the original coefficient action, the generated section subring is exactly the ring underlying the usual algebra generated by N(U).

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.GeneratedAlgebra
variable {X : Scheme.{u}} {A : TopCat.Sheaf CommRingCat.{u} X}
variable (α : X.sheaf ⟶ A)
variable (N : (RelativeSpec.underlyingModule α).val.Submodule)
Lean source · full declaration
theorem sectionSubring_eq_adjoin (U : X.Opensᵒᵖ) :
    let : Algebra (X.presheaf.obj U) (A.obj.obj U) := (α.hom.app U).hom.toAlgebra
    sectionSubring α N U =
      (Algebra.adjoin (X.presheaf.obj U)
        (sectionSubmodule α N U : Set (A.obj.obj U))).toSubring := by
  intro algebra
  exact (Algebra.adjoin_eq_ring_closure
    (R := X.presheaf.obj U) (sectionSubmodule α N U : Set (A.obj.obj U))).symm

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