Module

IdealSheafModuleMaps.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.IdealSheafModuleMaps

5 declarations indexed from sourceView source ↗

Module documentation

Maps between ideal modules under inverse image

The subscheme pullback map induces an ideal-module morphism and its adjoint pullback comparison.

Imports1

Nyll.AlgebraicCurves.Geometry.Sheaves.IdealSheafModule

Imported by39

abbrev

comapSubschemeHom

L35 ↗

AlgebraicGeometry.Scheme.IdealSheafData.comapSubschemeHom

Documentation

The canonical morphism from the inverse-image subscheme to the original subscheme.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits
noncomputable section
namespace AlgebraicGeometry.Scheme.IdealSheafData
variable {X X' : Scheme.{u}} (f : X' ⟶ X) (I : X.IdealSheafData)
open Opposite

Lean source · statement

abbrev comapSubschemeHom : (I.comap f).subscheme ⟶ I.subscheme

lemma

comapSubschemeHom_comp

L38 ↗

AlgebraicGeometry.Scheme.IdealSheafData.comapSubschemeHom_comp

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits
noncomputable section
namespace AlgebraicGeometry.Scheme.IdealSheafData
variable {X X' : Scheme.{u}} (f : X' ⟶ X) (I : X.IdealSheafData)
open Opposite

Lean source · statement

lemma comapSubschemeHom_comp :
    I.comapSubschemeHom f ≫ I.subschemeι = (I.comap f).subschemeι ≫ f

lemma

kernelι_unitToPushforwardUnit_map_eq_zero

L42 ↗

AlgebraicGeometry.Scheme.IdealSheafData.kernelι_unitToPushforwardUnit_map_eq_zero

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits
noncomputable section
namespace AlgebraicGeometry.Scheme.IdealSheafData
variable {X X' : Scheme.{u}} (f : X' ⟶ X) (I : X.IdealSheafData)
open Opposite

Lean source · statement

lemma kernelι_unitToPushforwardUnit_map_eq_zero :
    (kernel.ι I.subschemeι.unitToPushforwardUnit ≫ f.unitToPushforwardUnit) ≫
      (SheafOfModules.pushforward f.toRingCatSheafHom).map
        (I.comap f).subschemeι.unitToPushforwardUnit = 0

def

moduleToPushforwardComapModule

L67 ↗

AlgebraicGeometry.Scheme.IdealSheafData.moduleToPushforwardComapModule

Documentation

The ideal-module map induced by inverse image of the corresponding ideal sheaf.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits
noncomputable section
namespace AlgebraicGeometry.Scheme.IdealSheafData
variable {X X' : Scheme.{u}} (f : X' ⟶ X) (I : X.IdealSheafData)
open Opposite

Lean source · statement

def moduleToPushforwardComapModule :
    (I.module : SheafOfModules X.ringCatSheaf) ⟶
      (SheafOfModules.pushforward f.toRingCatSheafHom).obj (I.comap f).module

def

pullbackModuleComparison

L81 ↗

AlgebraicGeometry.Scheme.IdealSheafData.pullbackModuleComparison

Documentation

The pullback ideal-module map obtained from the pushforward map by adjunction.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits
noncomputable section
namespace AlgebraicGeometry.Scheme.IdealSheafData
variable {X X' : Scheme.{u}} (f : X' ⟶ X) (I : X.IdealSheafData)
open Opposite

Lean source · statement

def pullbackModuleComparison :
    (Scheme.Modules.pullback f).obj I.module ⟶ (I.comap f).module

Module documentation

Maps between ideal modules under inverse image

Declarations

comapSubschemeHom

comapSubschemeHom_comp

kernelι_unitToPushforwardUnit_map_eq_zero

moduleToPushforwardComapModule

pullbackModuleComparison