Module

PushforwardCoefficients.lean

Nyll.SchemeTheory.Modules.PushforwardCoefficients

4 declarations indexed from sourceView source ↗

Module documentation

Coefficients of pushforward section modules

Constructs the prescribed coefficient maps to global and local sections and compares them.

Imports2

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

Imported by3

def

pushforwardGlobalCoefficient

L25 ↗

AlgebraicGeometry.Scheme.Hom.pushforwardGlobalCoefficient

Documentation

The actual base-ring map to global sections of the source.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Hom

Lean source · statement

def pushforwardGlobalCoefficient {R : CommRingCat.{u}} {X : Scheme.{u}}
    (j : X ⟶ Spec R) : R →+* Γ(X, ⊤)

def

pushforwardSectionCoefficient

L30 ↗

AlgebraicGeometry.Scheme.Hom.pushforwardSectionCoefficient

Documentation

The actual base-ring map to sections over the preimage of an open.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Hom

Lean source · statement

def pushforwardSectionCoefficient {R : CommRingCat.{u}} {X : Scheme.{u}}
    (j : X ⟶ Spec R) (V : (Spec R).Opens) : R →+* Γ(X, j ⁻¹ᵁ V)

theorem

pushforwardSectionCoefficient_eq_restrict

L36 ↗

AlgebraicGeometry.Scheme.Hom.pushforwardSectionCoefficient_eq_restrict

Documentation

The two coefficient routes agree by the scheme morphism's actual naturality.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Hom

Lean source · statement

theorem pushforwardSectionCoefficient_eq_restrict {R : CommRingCat.{u}} {X : Scheme.{u}}
    (j : X ⟶ Spec R) (V : (Spec R).Opens) :
    j.pushforwardSectionCoefficient V =
      (X.presheaf.map (j ⁻¹ᵁ V).leTop.op).hom.comp j.pushforwardGlobalCoefficient

theorem

preimage_basicOpen_pushforwardGlobalCoefficient

L48 ↗

AlgebraicGeometry.Scheme.Hom.preimage_basicOpen_pushforwardGlobalCoefficient

Documentation

The localization open is the literal preimage of the affine basic open.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory TopologicalSpace Opposite
namespace AlgebraicGeometry.Scheme.Hom

Lean source · statement

theorem preimage_basicOpen_pushforwardGlobalCoefficient {R : CommRingCat.{u}} {X : Scheme.{u}}
    (j : X ⟶ Spec R) (r : R) :
    j ⁻¹ᵁ PrimeSpectrum.basicOpen r = X.basicOpen (j.pushforwardGlobalCoefficient r)

Module documentation

Coefficients of pushforward section modules

Declarations

pushforwardGlobalCoefficient

pushforwardSectionCoefficient

pushforwardSectionCoefficient_eq_restrict

preimage_basicOpen_pushforwardGlobalCoefficient