Module

SectionsAlgebra.lean

Nyll.SchemeTheory.Modules.SectionsAlgebra

2 declarations indexed from sourceView source ↗

Module documentation

The structure-presheaf map and section algebra induced by a morphism to an affine scheme.

Imports1

Mathlib.AlgebraicGeometry.Modules.Sheaf

Imported by3

def

constToPresheaf

L28 ↗

AlgebraicGeometry.Scheme.Hom.constToPresheaf

Documentation

The morphism from the constant base ring presheaf to the structure presheaf induced by f.

Source context 5 commands

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

universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Hom
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
noncomputable section

Lean source · full declaration

def constToPresheaf : (Functor.const (X.Opens)ᵒᵖ).obj (CommRingCat.of A) ⟶ X.presheaf where
  app U := (Scheme.ΓSpecIso (CommRingCat.of A)).inv ≫ f.appLE ⊤ U.unop le_top
  naturality U V i := by
    simp only [Functor.const_obj_obj, Functor.const_obj_map, Category.id_comp, Category.assoc]
    erw [Scheme.Hom.appLE_map]

def

sectionsAlgebra

L35 ↗

AlgebraicGeometry.Scheme.Hom.sectionsAlgebra

Documentation

The base ring algebra structure on local sections induced by f.

Source context 5 commands

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

universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Hom
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
noncomputable section

Lean source · statement

def sectionsAlgebra (U : X.Opens) : Algebra A Γ(X, U)

Module documentation

Declarations

constToPresheaf

sectionsAlgebra