NYLL
Module

PushforwardSectionComparison.lean

Nyll.SchemeTheory.Modules.PushforwardSectionComparison
22 declarations indexed from sourceView source ↗

Module documentation

Comparison of pushforward sections

Compares the existing section modules through the prescribed coefficient and restriction maps.

Imports12
Imported by2

Declarations

def

targetSectionCoefficient

L35 ↗
AlgebraicGeometry.Scheme.Hom.targetSectionCoefficient
Documentation

The actual target coefficient route at the already computed native section ring.

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 targetSectionCoefficient {R : CommRingCat.{u}} {X : Scheme.{u}}
    (j : X ⟶ Spec R) (V : (Spec R).Opens) : R →+* j.sectionComparisonRing V
def

sourceSectionCoefficient

L40 ↗
AlgebraicGeometry.Scheme.Hom.sourceSectionCoefficient
Documentation

The actual source coefficient route at the same native section ring.

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 sourceSectionCoefficient {R : CommRingCat.{u}} {X : Scheme.{u}}
    (j : X ⟶ Spec R) (V : (Spec R).Opens) : R →+* j.sectionComparisonRing V
theorem

sectionCoefficient_eq

L46 ↗
AlgebraicGeometry.Scheme.Hom.sectionCoefficient_eq
Documentation

The existing coefficient naturality at these computed native values.

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 sectionCoefficient_eq {R : CommRingCat.{u}} {X : Scheme.{u}}
    (j : X ⟶ Spec R) (V : (Spec R).Opens) :
    j.targetSectionCoefficient V = j.sourceSectionCoefficient V
def

pushforwardModulePresheaf

L56 ↗
AlgebraicGeometry.Scheme.Modules.pushforwardModulePresheaf
Documentation

The actual underlying base-module presheaf of the existing module pushforward.

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.Modules
Lean source · statement
def pushforwardModulePresheaf {R : CommRingCat.{u}} {X : Scheme.{u}}
    (j : X ⟶ Spec R) (M : X.Modules) : (Spec R).Opensᵒᵖ ⥤ ModuleCat.{u} R
def

sourceModulePresheaf

L61 ↗
AlgebraicGeometry.Scheme.Modules.sourceModulePresheaf
Documentation

The existing source global-module presheaf with its prescribed base coefficients.

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.Modules
Lean source · statement
def sourceModulePresheaf {R : CommRingCat.{u}} {X : Scheme.{u}}
    (j : X ⟶ Spec R) (M : X.Modules) : X.Opensᵒᵖ ⥤ ModuleCat.{u} R
def

restrictedModule

L68 ↗
AlgebraicGeometry.Scheme.Modules.restrictedModule
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.Modules
Lean source · statement
def restrictedModule {R A : CommRingCat.{u}} (σ : R →+* A)
    (N : ModuleCat.{u} A) : ModuleCat.{u} R
def

coefficientCongr

L72 ↗
AlgebraicGeometry.Scheme.Modules.coefficientCongr
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.Modules
Lean source · statement
def coefficientCongr {R A : CommRingCat.{u}} (σ τ : R →+* A)
    (h : σ = τ) (N : ModuleCat.{u} A) :
    restrictedModule σ N ≅ restrictedModule τ N
lemma

coefficientCongr_hom_apply

L77 ↗
AlgebraicGeometry.Scheme.Modules.coefficientCongr_hom_apply
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.Modules
Lean source · statement
lemma coefficientCongr_hom_apply {R A : CommRingCat.{u}} (σ τ : R →+* A)
    (h : σ = τ) (N : ModuleCat.{u} A) (x : N) :
    (coefficientCongr σ τ h N).hom x = x
def

targetSectionComponent

L83 ↗
AlgebraicGeometry.Scheme.Modules.targetSectionComponent
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.Modules
Lean source · statement
def targetSectionComponent {R : CommRingCat.{u}} {X : Scheme.{u}}
    (j : X ⟶ Spec R) (M : X.Modules) (V : (Spec R).Opens) :
    (pushforwardModulePresheaf j M).obj (op V) ≅
      restrictedModule (j.targetSectionCoefficient V) (j.sectionComparisonModule M V)
def

sourceSectionComponent

L90 ↗
AlgebraicGeometry.Scheme.Modules.sourceSectionComponent
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.Modules
Lean source · statement
def sourceSectionComponent {R : CommRingCat.{u}} {X : Scheme.{u}}
    (j : X ⟶ Spec R) (M : X.Modules) (V : (Spec R).Opens) :
    (sourceModulePresheaf j M).obj (op (j.sectionComparisonOpen V)) ≅
      restrictedModule (j.sourceSectionCoefficient V) (j.sectionComparisonModule M V)
def

pushforwardSectionIso

L98 ↗
AlgebraicGeometry.Scheme.Modules.pushforwardSectionIso
Documentation

Actual section comparison, using native values and the proved coefficient equality.

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.Modules
Lean source · statement
def pushforwardSectionIso {R : CommRingCat.{u}} {X : Scheme.{u}}
    (j : X ⟶ Spec R) (M : X.Modules) (V : (Spec R).Opens) :
    (pushforwardModulePresheaf j M).obj (op V) ≅
      (sourceModulePresheaf j M).obj (op (j.sectionComparisonOpen V))
def

sourceModuleOnTarget

L108 ↗
AlgebraicGeometry.Scheme.Modules.sourceModuleOnTarget
Documentation

The actual source module presheaf precomposed with the native preimage functor.

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.Modules
Lean source · statement
def sourceModuleOnTarget {R : CommRingCat.{u}} {X : Scheme.{u}}
    (j : X ⟶ Spec R) (M : X.Modules) : (Spec R).Opensᵒᵖ ⥤ ModuleCat.{u} R
def

sectionIsoOnTarget

L112 ↗
AlgebraicGeometry.Scheme.Modules.sectionIsoOnTarget
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.Modules
Lean source · statement
def sectionIsoOnTarget {R : CommRingCat.{u}} {X : Scheme.{u}}
    (j : X ⟶ Spec R) (M : X.Modules) (V : (Spec R).Opens) :
    (pushforwardModulePresheaf j M).obj (op V) ≅ (sourceModuleOnTarget j M).obj (op V)
lemma

coefficientCongr_hom_toAddMonoidHom

L117 ↗
AlgebraicGeometry.Scheme.Modules.coefficientCongr_hom_toAddMonoidHom
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.Modules
Lean source · statement
lemma coefficientCongr_hom_toAddMonoidHom {R A : CommRingCat.{u}}
    (σ τ : R →+* A) (h : σ = τ) (N : ModuleCat.{u} A) :
    (coefficientCongr σ τ h N).hom.hom.toAddMonoidHom = AddMonoidHom.id N
def

componentAddHom

L123 ↗
AlgebraicGeometry.Scheme.Modules.componentAddHom
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.Modules
Lean source · statement
def componentAddHom {R : CommRingCat.{u}} {X : Scheme.{u}}
    (j : X ⟶ Spec R) (M : X.Modules) (V : (Spec R).Opens) :
    j.sectionComparisonGroup M V →+ j.sectionComparisonGroup M V
lemma

componentAddHom_eq_id

L128 ↗
AlgebraicGeometry.Scheme.Modules.componentAddHom_eq_id
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.Modules
Lean source · statement
lemma componentAddHom_eq_id {R : CommRingCat.{u}} {X : Scheme.{u}}
    (j : X ⟶ Spec R) (M : X.Modules) (V : (Spec R).Opens) :
    componentAddHom j M V = AddMonoidHom.id (j.sectionComparisonGroup M V)
def

targetRestrictionAddHom

L134 ↗
AlgebraicGeometry.Scheme.Modules.targetRestrictionAddHom
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.Modules
Lean source · statement
def targetRestrictionAddHom {R : CommRingCat.{u}} {X : Scheme.{u}}
    (j : X ⟶ Spec R) (M : X.Modules) {U V : (Spec R).Opens} (i : U ⟶ V) :
    j.sectionComparisonGroup M V →+ j.sectionComparisonGroup M U
def

sourceRestrictionAddHom

L139 ↗
AlgebraicGeometry.Scheme.Modules.sourceRestrictionAddHom
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.Modules
Lean source · statement
def sourceRestrictionAddHom {R : CommRingCat.{u}} {X : Scheme.{u}}
    (j : X ⟶ Spec R) (M : X.Modules) {U V : (Spec R).Opens} (i : U ⟶ V) :
    j.sectionComparisonGroup M V →+ j.sectionComparisonGroup M U
lemma

restrictionAddHom_eq

L144 ↗
AlgebraicGeometry.Scheme.Modules.restrictionAddHom_eq
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.Modules
Lean source · statement
lemma restrictionAddHom_eq {R : CommRingCat.{u}} {X : Scheme.{u}}
    (j : X ⟶ Spec R) (M : X.Modules) {U V : (Spec R).Opens} (i : U ⟶ V) :
    targetRestrictionAddHom j M i = sourceRestrictionAddHom j M i
lemma

additive_naturality

L148 ↗
AlgebraicGeometry.Scheme.Modules.additive_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.Modules
Lean source · statement
lemma additive_naturality {R : CommRingCat.{u}} {X : Scheme.{u}}
    (j : X ⟶ Spec R) (M : X.Modules) {U V : (Spec R).Opens} (i : U ⟶ V) :
    (componentAddHom j M U).comp (targetRestrictionAddHom j M i) =
      (sourceRestrictionAddHom j M i).comp (componentAddHom j M V)
lemma

sectionIsoOnTarget_naturality

L156 ↗
AlgebraicGeometry.Scheme.Modules.sectionIsoOnTarget_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.Modules
Lean source · statement
lemma sectionIsoOnTarget_naturality {R : CommRingCat.{u}} {X : Scheme.{u}}
    (j : X ⟶ Spec R) (M : X.Modules) {U V : (Spec R).Opens} (i : U ⟶ V) :
    (pushforwardModulePresheaf j M).map i.op ≫ (sectionIsoOnTarget j M U).hom =
      (sectionIsoOnTarget j M V).hom ≫ (sourceModuleOnTarget j M).map i.op
def

pushforwardModulePresheafIso

L165 ↗
AlgebraicGeometry.Scheme.Modules.pushforwardModulePresheafIso
Documentation

The actual underlying module presheaves agree naturally over the target-open site.

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.Modules
Lean source · statement
def pushforwardModulePresheafIso {R : CommRingCat.{u}} {X : Scheme.{u}}
    (j : X ⟶ Spec R) (M : X.Modules) :
    pushforwardModulePresheaf j M ≅ sourceModuleOnTarget j M

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