Module

SpecSectionMap.lean

Nyll.SchemeTheory.Affine.SpecSectionMap

4 declarations indexed from sourceView source ↗

Module documentation

The actual section map of a morphism from a spectrum

The ΓSpec conversion is performed in this generic owner. The exported constructor and its equations keep that intermediate section ring out of callers that use the resulting morphism.

Imports2

Mathlib.Algebra.Category.Ring.Basic
Mathlib.AlgebraicGeometry.Scheme

Imported by4

def

specLiftSectionMap

L28 ↗

AlgebraicGeometry.specLiftSectionMap

Documentation

The actual global-section map of a morphism from an affine spectrum. Its intermediate sections of Spec S stay inside this generic constructor.

Source context 4 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u

Lean source · statement

def specLiftSectionMap {S : Type u} [CommRing S] {X : Scheme.{u}}
    (l : Spec (.of S) ⟶ X) : Γ(X, ⊤) ⟶ CommRingCat.of S

theorem

specLiftSectionMap_comp_endomorphism

L32 ↗

AlgebraicGeometry.specLiftSectionMap_comp_endomorphism

Source context 4 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u

Lean source · statement

theorem specLiftSectionMap_comp_endomorphism
    {S : Type u} [CommRing S] {X : Scheme.{u}}
    (l : Spec (.of S) ⟶ X) (τ : S →+* S)
    (hl : Spec.map (CommRingCat.ofHom τ) ≫ l = l) :
    specLiftSectionMap l ≫ CommRingCat.ofHom τ = specLiftSectionMap l

theorem

specLiftSectionMap_specMap

L56 ↗

AlgebraicGeometry.specLiftSectionMap_specMap

Documentation

The section-map constructor on an actual affine spectrum morphism is the native ΓSpec map of its ring homomorphism.

Source context 4 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u

Lean source · statement

theorem specLiftSectionMap_specMap
    {B S : Type u} [CommRing B] [CommRing S] (g : B →+* S) :
    specLiftSectionMap (Spec.map (CommRingCat.ofHom g)) =
      (Scheme.ΓSpecIso (CommRingCat.of B)).hom ≫ CommRingCat.ofHom g

theorem

specLiftSectionMap_affine

L64 ↗

AlgebraicGeometry.specLiftSectionMap_affine

Documentation

Evaluating the actual section map of an affine spectrum morphism returns exactly its original ring-category morphism.

Source context 4 commands

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

noncomputable section
open CategoryTheory
namespace AlgebraicGeometry
universe u

Lean source · statement

theorem specLiftSectionMap_affine {B S : CommRingCat.{u}} (g : B ⟶ S) :
    (Scheme.ΓSpecIso B).inv ≫ specLiftSectionMap (Spec.map g) = g

Module documentation

The actual section map of a morphism from a spectrum

Declarations

specLiftSectionMap

specLiftSectionMap_comp_endomorphism

specLiftSectionMap_specMap

specLiftSectionMap_affine