NYLL
Module

KaehlerModule.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.KaehlerModule
11 declarations indexed from sourceView source ↗

Module documentation

Kaehler Module

Imports5
Imported by4

Declarations

def

kaehlerPresheaf

L34 ↗
AlgebraicGeometry.Scheme.Hom.kaehlerPresheaf
Documentation

The presheaf of relative Kaehler differentials for f.

Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Hom
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
Lean source · statement
def kaehlerPresheaf : X.PresheafOfModules
instance

kaehlerPresheafModule

L37 ↗
AlgebraicGeometry.Scheme.Hom.kaehlerPresheafModule
Source context 5 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Hom
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
Lean source · statement
instance kaehlerPresheafModule (U : X.Opens) :
    Module Γ(X, U) (f.kaehlerPresheaf.obj (op U))
def

kaehler

L42 ↗
AlgebraicGeometry.Scheme.Hom.kaehler
Documentation

The module sheaf obtained by sheafifying the relative differential presheaf.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Hom
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
local instance kaehlerPresheafModule (U : X.Opens) :
    Module Γ(X, U) (f.kaehlerPresheaf.obj (op U)) :=
  (f.kaehlerPresheaf.obj (op U)).isModule
Lean source · statement
def kaehler : X.Modules
def

topDifferentials

L46 ↗
AlgebraicGeometry.Scheme.Hom.topDifferentials
Documentation

The specified determinant degree of the relative differential module sheaf.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Hom
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
local instance kaehlerPresheafModule (U : X.Opens) :
    Module Γ(X, U) (f.kaehlerPresheaf.obj (op U)) :=
  (f.kaehlerPresheaf.obj (op U)).isModule
Lean source · statement
def topDifferentials (d : ℕ) : X.Modules
abbrev

topPresheaf

L50 ↗
AlgebraicGeometry.Scheme.Hom.topPresheaf
Documentation

The specified exterior degree of the relative differential presheaf.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Hom
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
local instance kaehlerPresheafModule (U : X.Opens) :
    Module Γ(X, U) (f.kaehlerPresheaf.obj (op U)) :=
  (f.kaehlerPresheaf.obj (op U)).isModule
Lean source · statement
abbrev topPresheaf (d : ℕ) : X.PresheafOfModules
lemma

kaehlerPresheaf_obj

L53 ↗
AlgebraicGeometry.Scheme.Hom.kaehlerPresheaf_obj
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Hom
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
local instance kaehlerPresheafModule (U : X.Opens) :
    Module Γ(X, U) (f.kaehlerPresheaf.obj (op U)) :=
  (f.kaehlerPresheaf.obj (op U)).isModule
Lean source · statement
lemma kaehlerPresheaf_obj (U : (X.Opens)ᵒᵖ) :
    f.kaehlerPresheaf.obj U = CommRingCat.KaehlerDifferential (f.constToPresheaf.app U)
def

kaehlerToSections

L57 ↗
AlgebraicGeometry.Scheme.Hom.kaehlerToSections
Documentation

The map from presheaf differentials to sections of the sheafified differential module.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Hom
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
local instance kaehlerPresheafModule (U : X.Opens) :
    Module Γ(X, U) (f.kaehlerPresheaf.obj (op U)) :=
  (f.kaehlerPresheaf.obj (op U)).isModule
Lean source · statement
def kaehlerToSections (U : X.Opens) :
    (f.kaehlerPresheaf.obj (op U) : Type u) → (Γ(f.kaehler, U) : Type u)
def

kaehlerToSectionsₗ

L63 ↗
AlgebraicGeometry.Scheme.Hom.kaehlerToSectionsₗ
Documentation

The linear sheafification map on the differential module over the selected open.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Hom
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
local instance kaehlerPresheafModule (U : X.Opens) :
    Module Γ(X, U) (f.kaehlerPresheaf.obj (op U)) :=
  (f.kaehlerPresheaf.obj (op U)).isModule
Lean source · statement
def kaehlerToSectionsₗ (U : X.Opens) :
    (f.kaehlerPresheaf.obj (op U)) →ₗ[Γ(X, U)] (Γ(f.kaehler, U) : Type u)
def

topToSections

L70 ↗
AlgebraicGeometry.Scheme.Hom.topToSections
Documentation

The map from exterior presheaf differentials to sections of the corresponding determinant sheaf.

Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Hom
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
local instance kaehlerPresheafModule (U : X.Opens) :
    Module Γ(X, U) (f.kaehlerPresheaf.obj (op U)) :=
  (f.kaehlerPresheaf.obj (op U)).isModule
Lean source · statement
def topToSections (d : ℕ) (U : X.Opens) :
    (⋀[Γ(X, U)]^d (f.kaehlerPresheaf.obj (op U)) : Type u) → (Γ(f.topDifferentials d, U) : Type u)
theorem

kaehlerToSections_add

L77 ↗
AlgebraicGeometry.Scheme.Hom.kaehlerToSections_add
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Hom
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
local instance kaehlerPresheafModule (U : X.Opens) :
    Module Γ(X, U) (f.kaehlerPresheaf.obj (op U)) :=
  (f.kaehlerPresheaf.obj (op U)).isModule
Lean source · statement
theorem kaehlerToSections_add (U : X.Opens) (s t : f.kaehlerPresheaf.obj (op U)) :
    f.kaehlerToSections U (s + t) = f.kaehlerToSections U s + f.kaehlerToSections U t
theorem

kaehlerPresheaf_nontrivial_polynomial

L81 ↗
AlgebraicGeometry.Scheme.Hom.kaehlerPresheaf_nontrivial_polynomial
Source context 6 commands

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

noncomputable section
universe u
open CategoryTheory Opposite
namespace AlgebraicGeometry.Scheme.Hom
variable {A : Type u} [CommRing A] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of A))
local instance kaehlerPresheafModule (U : X.Opens) :
    Module Γ(X, U) (f.kaehlerPresheaf.obj (op U)) :=
  (f.kaehlerPresheaf.obj (op U)).isModule
Lean source · full declaration
theorem kaehlerPresheaf_nontrivial_polynomial (A : Type u) [CommRing A] [Nontrivial A] :
    letI f : Spec (CommRingCat.of (Polynomial A)) ⟶ Spec (CommRingCat.of A) :=
      Spec.map (CommRingCat.ofHom (algebraMap A (Polynomial A)))
    Nontrivial (f.kaehlerPresheaf.obj (op ⊤)) := by
  set f : Spec (CommRingCat.of (Polynomial A)) ⟶ Spec (CommRingCat.of A) :=
    Spec.map (CommRingCat.ofHom (algebraMap A (Polynomial A))) with hf
  let Γ' : Type u := Γ(Spec (CommRingCat.of (Polynomial A)), ⊤)
  let algA : Algebra A Γ' := f.sectionsAlgebra ⊤
  let e : Γ' ≃+* Polynomial A := (Scheme.ΓSpecIso (CommRingCat.of (Polynomial
    A))).commRingCatIsoToRingEquiv
  let : Algebra Γ' (Polynomial A) := e.toRingHom.toAlgebra
  have hcomp : (algebraMap Γ' (Polynomial A)).comp (algebraMap A Γ') = algebraMap A (Polynomial A)
    := by
    refine RingHom.ext fun a => ?_
    change (Scheme.ΓSpecIso (CommRingCat.of (Polynomial A))).hom.hom
      ((f.appLE ⊤ ⊤ le_top).hom ((Scheme.ΓSpecIso (CommRingCat.of A)).inv.hom a)) = algebraMap A
        (Polynomial A) a
    have h1 : f.appLE ⊤ ⊤ le_top = f.appTop := by
      unfold Scheme.Hom.appLE
      have ht : (show op (⊤ : (Spec (CommRingCat.of (Polynomial A))).Opens) ⟶ op ⊤ from
          (homOfLE (le_top : (⊤ : (Spec (CommRingCat.of (Polynomial A))).Opens) ≤ f ⁻¹ᵁ ⊤)).op) =
          𝟙 (op ⊤) := Subsingleton.elim _ _
      have hm : (Spec (CommRingCat.of (Polynomial A))).presheaf.map
          (show op (⊤ : (Spec (CommRingCat.of (Polynomial A))).Opens) ⟶ op ⊤ from
            (homOfLE (le_top : (⊤ : (Spec (CommRingCat.of (Polynomial A))).Opens) ≤ f ⁻¹ᵁ ⊤)).op) =
          𝟙 Γ(Spec (CommRingCat.of (Polynomial A)), ⊤) :=
        (congrArg (fun i : op (⊤ : (Spec (CommRingCat.of (Polynomial A))).Opens) ⟶ op ⊤ =>
          (Spec (CommRingCat.of (Polynomial A))).presheaf.map i) ht).trans
          (CategoryTheory.Functor.map_id _ _)
      exact (congrArg (fun k : Γ(Spec (CommRingCat.of (Polynomial A)), ⊤) ⟶
          Γ(Spec (CommRingCat.of (Polynomial A)), ⊤) => f.appTop ≫ k) hm).trans
        (Category.comp_id f.appTop)
    rw [h1]
    have h2 := Scheme.ΓSpecIso_naturality (CommRingCat.ofHom (algebraMap A (Polynomial A)))
    rw [← hf] at h2
    have h3 := congrArg (fun φ => φ.hom ((Scheme.ΓSpecIso (CommRingCat.of A)).inv.hom a)) h2
    simp only [CommRingCat.hom_comp, RingHom.coe_comp, Function.comp_apply] at h3
    rw [h3]
    change algebraMap A (Polynomial A) (((Scheme.ΓSpecIso (CommRingCat.of A)).inv ≫
      (Scheme.ΓSpecIso (CommRingCat.of A)).hom).hom a) = _
    rw [Iso.inv_hom_id]; rfl
  have : IsScalarTower A Γ' (Polynomial A) := IsScalarTower.of_algebraMap_eq' hcomp.symm
  have hsurj : Function.Surjective (KaehlerDifferential.map A A Γ' (Polynomial A)) :=
    KaehlerDifferential.map_surjective_of_surjective A A (h := e.surjective)
  have : Nontrivial (Ω[Polynomial A⁄A]) :=
    (KaehlerDifferential.polynomialEquiv A).toEquiv.nontrivial
  exact hsurj.nontrivial

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