Module

LinearPencilSections.lean

Nyll.AlgebraicCurves.RelativeDivisors.LinearPencilSections

16 declarations indexed from sourceView source ↗

Module documentation

Actual sections in a linear pencil

The section (1-t)s₀ + ts₁ is formed on the actual product with the affine line. Its restrictions along the sections t = a are computed through the canonical composition and identity isomorphisms for pullback of modules.

Imports4

Nyll.SchemeTheory.Modules.PullbackLocalSection
Nyll.SchemeTheory.Modules.PullbackUnitComposition
Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.Algebra.Polynomial.Eval.Defs

Imported by4

def

lineMap

L33 ↗

AlgebraicGeometry.LinearPencil.lineMap

Documentation

The structure morphism of the affine parameter line.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.LinearPencil
open Scheme.Modules
variable {R : Type u} [CommRing R] {X : Scheme.{u}}

Lean source · statement

def lineMap : Spec (CommRingCat.of (Polynomial R)) ⟶ Spec (CommRingCat.of R)

def

evaluate

L37 ↗

AlgebraicGeometry.LinearPencil.evaluate

Documentation

Evaluation at a base-ring element, as a section of the affine line.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.LinearPencil
open Scheme.Modules
variable {R : Type u} [CommRing R] {X : Scheme.{u}}

Lean source · statement

def evaluate (a : R) : Spec (CommRingCat.of R) ⟶ Spec (CommRingCat.of (Polynomial R))

theorem

evaluate_comp_lineMap

L40 ↗

AlgebraicGeometry.LinearPencil.evaluate_comp_lineMap

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.LinearPencil
open Scheme.Modules
variable {R : Type u} [CommRing R] {X : Scheme.{u}}

Lean source · statement

theorem evaluate_comp_lineMap (a : R) : evaluate a ≫ lineMap = 𝟙 _

def

fibre

L51 ↗

AlgebraicGeometry.LinearPencil.fibre

Documentation

Inclusion of the fibre with parameter a into the actual product.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.LinearPencil
open Scheme.Modules
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (c : X ⟶ Spec (CommRingCat.of R))

Lean source · statement

def fibre (a : R) : X ⟶ pullback c lineMap

theorem

fibre_fst

L55 ↗

AlgebraicGeometry.LinearPencil.fibre_fst

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.LinearPencil
open Scheme.Modules
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (c : X ⟶ Spec (CommRingCat.of R))

Lean source · statement

theorem fibre_fst (a : R) : fibre c a ≫ pullback.fst c lineMap = 𝟙 X

theorem

fibre_snd

L58 ↗

AlgebraicGeometry.LinearPencil.fibre_snd

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.LinearPencil
open Scheme.Modules
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (c : X ⟶ Spec (CommRingCat.of R))

Lean source · statement

theorem fibre_snd (a : R) : fibre c a ≫ pullback.snd c lineMap = c ≫ evaluate a

def

parameter

L62 ↗

AlgebraicGeometry.LinearPencil.parameter

Documentation

The actual parameter as a global function on the product.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.LinearPencil
open Scheme.Modules
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (c : X ⟶ Spec (CommRingCat.of R))

Lean source · statement

def parameter : Γ(pullback c lineMap, ⊤)

theorem

parameter_fibre

L66 ↗

AlgebraicGeometry.LinearPencil.parameter_fibre

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.LinearPencil
open Scheme.Modules
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (c : X ⟶ Spec (CommRingCat.of R))

Lean source · statement

theorem parameter_fibre (a : R) : (fibre c a).appTop (parameter c) =
    c.appTop ((Scheme.ΓSpecIso (CommRingCat.of R)).inv a)

theorem

pullbackComp_section

L82 ↗

AlgebraicGeometry.LinearPencil.pullbackComp_section

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.LinearPencil
open Scheme.Modules
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (c : X ⟶ Spec (CommRingCat.of R))

Lean source · statement

theorem pullbackComp_section {Y Z : Scheme.{u}} (f : Z ⟶ Y)
    (g : Y ⟶ X) (M : X.Modules) (s : Γ(M, ⊤)) :
    ((pullbackComp f g).hom.app M).app ⊤
      (pullbackLocalSection f (pullbackLocalSection g s)) =
      pullbackLocalSection (f ≫ g) s

theorem

pullbackId_section

L95 ↗

AlgebraicGeometry.LinearPencil.pullbackId_section

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.LinearPencil
open Scheme.Modules
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (c : X ⟶ Spec (CommRingCat.of R))

Lean source · statement

theorem pullbackId_section (M : X.Modules) (s : Γ(M, ⊤)) :
    ((pullbackId X).hom.app M).app ⊤ (pullbackLocalSection (𝟙 X) s) = s

theorem

pullbackCongr_section

L103 ↗

AlgebraicGeometry.LinearPencil.pullbackCongr_section

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.LinearPencil
open Scheme.Modules
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (c : X ⟶ Spec (CommRingCat.of R))

Lean source · statement

theorem pullbackCongr_section {Y : Scheme.{u}} {f g : Y ⟶ X}
    (h : f = g) (M : X.Modules) (s : Γ(M, ⊤)) :
    ((pullbackCongr h).hom.app M).app ⊤ (pullbackLocalSection f s) =
      pullbackLocalSection g s

def

fibreModuleIso

L112 ↗

AlgebraicGeometry.LinearPencil.fibreModuleIso

Documentation

Canonical comparison of a pulled-back module with its restriction to a fibre.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.LinearPencil
open Scheme.Modules
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (c : X ⟶ Spec (CommRingCat.of R))

Lean source · statement

def fibreModuleIso (a : R) (M : X.Modules) :
    (Scheme.Modules.pullback (fibre c a)).obj
      ((Scheme.Modules.pullback (pullback.fst c lineMap)).obj M) ≅ M

theorem

fibreModuleIso_section

L118 ↗

AlgebraicGeometry.LinearPencil.fibreModuleIso_section

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.LinearPencil
open Scheme.Modules
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (c : X ⟶ Spec (CommRingCat.of R))

Lean source · statement

theorem fibreModuleIso_section (a : R) (M : X.Modules) (s : Γ(M, ⊤)) :
    (fibreModuleIso c a M).hom.app ⊤
      (pullbackLocalSection (fibre c a)
        (pullbackLocalSection (pullback.fst c lineMap) s)) = s

def

pencilSection

L130 ↗

AlgebraicGeometry.LinearPencil.pencilSection

Documentation

Linear interpolation of two sections on the actual affine-line product.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.LinearPencil
open Scheme.Modules
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (c : X ⟶ Spec (CommRingCat.of R))

Lean source · statement

def pencilSection (M : X.Modules) (s₀ s₁ : Γ(M, ⊤)) :
    Γ((Scheme.Modules.pullback (pullback.fst c lineMap)).obj M, ⊤)

theorem

pencilSection_pullback

L142 ↗

AlgebraicGeometry.LinearPencil.pencilSection_pullback

Documentation

Pullback of the actual pencil along an arbitrary test-scheme morphism. This includes geometric fibres over extensions of the ground field.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.LinearPencil
open Scheme.Modules
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (c : X ⟶ Spec (CommRingCat.of R))

Lean source · full declaration

theorem pencilSection_pullback {Y : Scheme.{u}} (φ : Y ⟶ pullback c lineMap)
    (M : X.Modules) (s₀ s₁ : Γ(M, ⊤)) :
    let V : Y.Modules := (Scheme.Modules.pullback (φ ≫ pullback.fst c lineMap)).obj M
    let v₀ : Γ(V, ⊤) := pullbackLocalSection (φ ≫ pullback.fst c lineMap) s₀
    let v₁ : Γ(V, ⊤) := pullbackLocalSection (φ ≫ pullback.fst c lineMap) s₁
    ((pullbackComp φ (pullback.fst c lineMap)).hom.app M).app ⊤
      (pullbackLocalSection φ (pencilSection c M s₀ s₁)) =
      (1 - φ.appTop (parameter c)) • v₀ + φ.appTop (parameter c) • v₁ := by
  intro V v₀ v₁
  let N : (pullback c lineMap).Modules :=
    (Scheme.Modules.pullback (pullback.fst c lineMap)).obj M
  let z₀ : Γ(N, ⊤) := pullbackLocalSection (pullback.fst c lineMap) s₀
  let z₁ : Γ(N, ⊤) := pullbackLocalSection (pullback.fst c lineMap) s₁
  let W : Y.Modules := (Scheme.Modules.pullback φ).obj N
  let w₀ : Γ(W, ⊤) := pullbackLocalSection φ z₀
  let w₁ : Γ(W, ⊤) := pullbackLocalSection φ z₁
  have h₀ : ((pullbackComp φ (pullback.fst c lineMap)).hom.app M).app ⊤ w₀ = v₀ :=
    pullbackComp_section φ (pullback.fst c lineMap) M s₀
  have h₁ : ((pullbackComp φ (pullback.fst c lineMap)).hom.app M).app ⊤ w₁ = v₁ :=
    pullbackComp_section φ (pullback.fst c lineMap) M s₁
  change ((pullbackComp φ (pullback.fst c lineMap)).hom.app M).app ⊤
    (pullbackLocalSection φ ((1 - parameter c) • z₀ + parameter c • z₁)) = _
  rw [pullbackLocalSection_add, pullbackLocalSection_smul (L := N) (U := ⊤),
    pullbackLocalSection_smul (L := N) (U := ⊤)]
  change ((pullbackComp φ (pullback.fst c lineMap)).hom.app M).app ⊤
    ((φ.appTop (1 - parameter c)) • w₀ + φ.appTop (parameter c) • w₁) = _
  rw [map_sub, map_one, map_add, Scheme.Modules.Hom.app_smul,
    Scheme.Modules.Hom.app_smul, h₀, h₁]

theorem

section_fibre

L172 ↗

AlgebraicGeometry.LinearPencil.section_fibre

Documentation

Restricting the actual pencil to t=a gives the stated linear combination.

Source context 7 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite
namespace AlgebraicGeometry.LinearPencil
open Scheme.Modules
variable {R : Type u} [CommRing R] {X : Scheme.{u}}
variable (c : X ⟶ Spec (CommRingCat.of R))

Lean source · statement

theorem section_fibre (a : R) (M : X.Modules) (s₀ s₁ : Γ(M, ⊤)) :
    (fibreModuleIso c a M).hom.app ⊤
      (pullbackLocalSection (fibre c a) (pencilSection c M s₀ s₁)) =
      (1 - c.appTop ((Scheme.ΓSpecIso (CommRingCat.of R)).inv a)) • s₀ +
        c.appTop ((Scheme.ΓSpecIso (CommRingCat.of R)).inv a) • s₁

Module documentation

Actual sections in a linear pencil

Declarations