NYLL
Module

OModulePresheafHom.lean

Nyll.SchemeTheory.Cohomology.Sheaves.OModulePresheafHom
32 declarations indexed from sourceView source ↗

Module documentation

Morphisms of module presheaves, their affine sections and short exact sequences.

Imports2
Imported by28

Declarations

theorem

isAffineOpen_inf_of_isSeparated

L34 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.isAffineOpen_inf_of_isSeparated
Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace Scheme.OrderedAffineCover
variable (π : V ⟶ Spec (.of R)) (K : V.OrderedAffineCover)
Lean source · statement
theorem isAffineOpen_inf_of_isSeparated [IsSeparated π] {U W : V.Opens} (hU : IsAffineOpen U)
    (hW : IsAffineOpen W) : IsAffineOpen (U ⊓ W)
theorem

isAffineOpen_inter

L39 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.isAffineOpen_inter
Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace Scheme.OrderedAffineCover
variable (π : V ⟶ Spec (.of R)) (K : V.OrderedAffineCover)
Lean source · statement
theorem isAffineOpen_inter [IsSeparated π] {i : ℕ} (s : K.Idx i) : IsAffineOpen (K.inter s)
abbrev

affineInter

L58 ↗
AlgebraicGeometry.Scheme.OrderedAffineCover.affineInter
Documentation

The affine open given by an intersection indexed by the ordered affine cover.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace Scheme.OrderedAffineCover
variable (π : V ⟶ Spec (.of R)) (K : V.OrderedAffineCover)
Lean source · statement
abbrev affineInter [IsSeparated π] {i : ℕ} (s : K.Idx i) : V.affineOpens
structure

Hom

L71 ↗
AlgebraicGeometry.OModulePresheaf.Hom
Documentation

A morphism of O-module presheaves, linear over local section rings and compatible with restriction.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
Lean source · full declaration
structure Hom (F G : OModulePresheaf π) where
  /-- The base-ring linear map on sections of each open subset. -/
  app : ∀ U : V.Opens, F.obj U →ₗ[R] G.obj U
  /-- Each section map respects scalar multiplication by local regular functions. -/
  app_smul : ∀ (U : V.Opens) (a : Γ(V, U)) (x : F.obj U), app U (a • x) = a • app U x
  /-- The section maps commute with restriction to smaller open subsets. -/
  naturality : ∀ {U U' : V.Opens} (h : U ≤ U'), app U ∘ₗ F.res h = G.res h ∘ₗ app U'
structure

SES

L80 ↗
AlgebraicGeometry.OModulePresheaf.SES
Documentation

A sequence of O-module presheaves that is short exact on every open subset.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
Lean source · full declaration
structure SES (F₁ F₂ F₃ : OModulePresheaf π) where
  /-- The inclusion morphism of the short exact sequence. -/
  inc : Hom F₁ F₂
  /-- The projection morphism of the short exact sequence. -/
  proj : Hom F₂ F₃
  /-- The inclusion is injective on sections of every open subset. -/
  injective : ∀ U : V.Opens, Function.Injective (inc.app U)
  /-- The projection is surjective on sections of every open subset. -/
  surjective : ∀ U : V.Opens, Function.Surjective (proj.app U)
  /-- The image of the inclusion equals the kernel of the projection on each open subset. -/
  exact : ∀ U : V.Opens, LinearMap.range (inc.app U) = LinearMap.ker (proj.app U)
structure

AffHom

L96 ↗
AlgebraicGeometry.OModulePresheaf.AffHom
Documentation

A morphism on affine-open sections, linear over local section rings and compatible with restriction.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
Lean source · full declaration
structure AffHom (F G : OModulePresheaf π) where
  /-- The base-ring linear map on sections of each affine open subset. -/
  app : ∀ U : V.affineOpens, F.obj U.1 →ₗ[R] G.obj U.1
  /-- Each affine-open section map respects scalar multiplication by local regular functions. -/
  app_smul : ∀ (U : V.affineOpens) (a : Γ(V, U.1)) (x : F.obj U.1), app U (a • x) = a • app U x
  /-- The section maps commute with restriction between affine open subsets. -/
  naturality : ∀ {U U' : V.affineOpens} (h : U.1 ≤ U'.1), app U ∘ₗ F.res h = G.res h ∘ₗ app U'
structure

AffSES

L105 ↗
AlgebraicGeometry.OModulePresheaf.AffSES
Documentation

A sequence of O-module presheaves that is short exact on every affine open subset.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
Lean source · full declaration
structure AffSES (F₁ F₂ F₃ : OModulePresheaf π) where
  /-- The inclusion morphism on affine-open sections. -/
  inc : AffHom F₁ F₂
  /-- The projection morphism on affine-open sections. -/
  proj : AffHom F₂ F₃
  /-- The inclusion is injective on sections of every affine open subset. -/
  injective : ∀ U : V.affineOpens, Function.Injective (inc.app U)
  /-- The projection is surjective on sections of every affine open subset. -/
  surjective : ∀ U : V.affineOpens, Function.Surjective (proj.app U)
  /-- The image of the inclusion equals the kernel of the projection on each affine open subset. -/
  exact : ∀ U : V.affineOpens, LinearMap.range (inc.app U) = LinearMap.ker (proj.app U)
def

appSections

L122 ↗
AlgebraicGeometry.OModulePresheaf.Hom.appSections
Documentation

The section map viewed as a linear map over the ring of regular functions on the open subset.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
namespace Hom
variable {F G H : OModulePresheaf π}
Lean source · statement
def appSections (φ : Hom F G) (U : V.Opens) : F.obj U →ₗ[Γ(V, U)] G.obj U
theorem

appSections_apply

L125 ↗
AlgebraicGeometry.OModulePresheaf.Hom.appSections_apply
Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
namespace Hom
variable {F G H : OModulePresheaf π}
Lean source · statement
theorem appSections_apply (φ : Hom F G) (U : V.Opens) (x : F.obj U) :
    φ.appSections U x = φ.app U x
theorem

naturality_apply

L128 ↗
AlgebraicGeometry.OModulePresheaf.Hom.naturality_apply
Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
namespace Hom
variable {F G H : OModulePresheaf π}
Lean source · statement
theorem naturality_apply (φ : Hom F G) {U U' : V.Opens} (h : U ≤ U') (x : F.obj U') :
    φ.app U (F.res h x) = G.res h (φ.app U' x)
def

id

L134 ↗
AlgebraicGeometry.OModulePresheaf.Hom.id
Documentation

The identity morphism of an O-module presheaf.

Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
namespace Hom
variable {F G H : OModulePresheaf π}
variable (F) in
Lean source · full declaration
def id : Hom F F where
  app _ := LinearMap.id
  app_smul _ _ _ := rfl
  naturality _ := rfl
def

comp

L140 ↗
AlgebraicGeometry.OModulePresheaf.Hom.comp
Documentation

The composite morphism obtained by composing the section maps.

Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
namespace Hom
variable {F G H : OModulePresheaf π}
variable (F) in
Lean source · full declaration
def comp (ψ : Hom G H) (φ : Hom F G) : Hom F H where
  app U := ψ.app U ∘ₗ φ.app U
  app_smul U a x := by
    change ψ.app U (φ.app U (a • x)) = a • ψ.app U (φ.app U x)
    rw [φ.app_smul, ψ.app_smul]
  naturality h := by
    rw [LinearMap.comp_assoc, φ.naturality, ← LinearMap.comp_assoc, ψ.naturality,
      LinearMap.comp_assoc]
theorem

id_app

L149 ↗
AlgebraicGeometry.OModulePresheaf.Hom.id_app
Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
namespace Hom
variable {F G H : OModulePresheaf π}
variable (F) in
Lean source · statement
theorem id_app (U : V.Opens) (x : F.obj U) : (Hom.id F).app U x = x
theorem

comp_app

L150 ↗
AlgebraicGeometry.OModulePresheaf.Hom.comp_app
Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
namespace Hom
variable {F G H : OModulePresheaf π}
variable (F) in
Lean source · statement
theorem comp_app (ψ : Hom G H) (φ : Hom F G) (U : V.Opens) (x : F.obj U) :
    (ψ.comp φ).app U x = ψ.app U (φ.app U x)
def

toAffHom

L154 ↗
AlgebraicGeometry.OModulePresheaf.Hom.toAffHom
Documentation

The restriction of a presheaf morphism to affine-open sections.

Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
namespace Hom
variable {F G H : OModulePresheaf π}
variable (F) in
Lean source · full declaration
def toAffHom (φ : Hom F G) : AffHom F G where
  app U := φ.app U.1
  app_smul U := φ.app_smul U.1
  naturality h := φ.naturality h
theorem

toAffHom_app

L159 ↗
AlgebraicGeometry.OModulePresheaf.Hom.toAffHom_app
Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
namespace Hom
variable {F G H : OModulePresheaf π}
variable (F) in
Lean source · statement
theorem toAffHom_app (φ : Hom F G) (U : V.affineOpens) : φ.toAffHom.app U = φ.app U.1
def

appSections

L168 ↗
AlgebraicGeometry.OModulePresheaf.AffHom.appSections
Documentation

The affine-open section map viewed as linear over its ring of regular functions.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
namespace AffHom
variable {F G H : OModulePresheaf π}
Lean source · statement
def appSections (φ : AffHom F G) (U : V.affineOpens) : F.obj U.1 →ₗ[Γ(V, U.1)] G.obj U.1
theorem

appSections_apply

L171 ↗
AlgebraicGeometry.OModulePresheaf.AffHom.appSections_apply
Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
namespace AffHom
variable {F G H : OModulePresheaf π}
Lean source · statement
theorem appSections_apply (φ : AffHom F G) (U : V.affineOpens) (x : F.obj U.1) :
    φ.appSections U x = φ.app U x
theorem

naturality_apply

L174 ↗
AlgebraicGeometry.OModulePresheaf.AffHom.naturality_apply
Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
namespace AffHom
variable {F G H : OModulePresheaf π}
Lean source · statement
theorem naturality_apply (φ : AffHom F G) {U U' : V.affineOpens} (h : U.1 ≤ U'.1) (x : F.obj U'.1) :
    φ.app U (F.res h x) = G.res h (φ.app U' x)
def

id

L180 ↗
AlgebraicGeometry.OModulePresheaf.AffHom.id
Documentation

The identity morphism on affine-open sections.

Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
namespace AffHom
variable {F G H : OModulePresheaf π}
variable (F) in
Lean source · full declaration
def id : AffHom F F where
  app _ := LinearMap.id
  app_smul _ _ _ := rfl
  naturality _ := rfl
def

comp

L186 ↗
AlgebraicGeometry.OModulePresheaf.AffHom.comp
Documentation

The composite morphism on affine-open sections.

Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
namespace AffHom
variable {F G H : OModulePresheaf π}
variable (F) in
Lean source · full declaration
def comp (ψ : AffHom G H) (φ : AffHom F G) : AffHom F H where
  app U := ψ.app U ∘ₗ φ.app U
  app_smul U a x := by
    change ψ.app U (φ.app U (a • x)) = a • ψ.app U (φ.app U x)
    rw [φ.app_smul, ψ.app_smul]
  naturality h := by
    rw [LinearMap.comp_assoc, φ.naturality, ← LinearMap.comp_assoc, ψ.naturality,
      LinearMap.comp_assoc]
theorem

id_app

L195 ↗
AlgebraicGeometry.OModulePresheaf.AffHom.id_app
Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
namespace AffHom
variable {F G H : OModulePresheaf π}
variable (F) in
Lean source · statement
theorem id_app (U : V.affineOpens) (x : F.obj U.1) : (AffHom.id F).app U x = x
theorem

comp_app

L196 ↗
AlgebraicGeometry.OModulePresheaf.AffHom.comp_app
Source context 10 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
namespace AffHom
variable {F G H : OModulePresheaf π}
variable (F) in
Lean source · statement
theorem comp_app (ψ : AffHom G H) (φ : AffHom F G) (U : V.affineOpens) (x : F.obj U.1) :
    (ψ.comp φ).app U x = ψ.app U (φ.app U x)
def

toAffSES

L204 ↗
AlgebraicGeometry.OModulePresheaf.SES.toAffSES
Documentation

The short exact sequence on affine-open sections obtained from a sectionwise short exact sequence.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
Lean source · full declaration
def SES.toAffSES {F₁ F₂ F₃ : OModulePresheaf π} (S : SES F₁ F₂ F₃) : AffSES F₁ F₂ F₃ where
  inc := S.inc.toAffHom
  proj := S.proj.toAffHom
  injective U := S.injective U.1
  surjective U := S.surjective U.1
  exact U := S.exact U.1
def

cochainMap

L216 ↗
AlgebraicGeometry.OModulePresheaf.AffHom.cochainMap
Documentation

The map of Cech cochains induced by the affine-open section maps.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
section Cochains
variable [IsSeparated π] (K : V.OrderedAffineCover) {F G : OModulePresheaf π}
Lean source · statement
def AffHom.cochainMap (φ : AffHom F G) (i : ℕ) : F.cochain K i →ₗ[R] G.cochain K i
theorem

cochainMap_apply

L219 ↗
AlgebraicGeometry.OModulePresheaf.AffHom.cochainMap_apply
Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
section Cochains
variable [IsSeparated π] (K : V.OrderedAffineCover) {F G : OModulePresheaf π}
Lean source · statement
theorem AffHom.cochainMap_apply (φ : AffHom F G) (i : ℕ) (f : F.cochain K i) (s : K.Idx i) :
    φ.cochainMap K i f s = φ.app (K.affineInter π s) (f s)
theorem

cochainMap_comp_d

L222 ↗
AlgebraicGeometry.OModulePresheaf.AffHom.cochainMap_comp_d
Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
section Cochains
variable [IsSeparated π] (K : V.OrderedAffineCover) {F G : OModulePresheaf π}
Lean source · statement
theorem AffHom.cochainMap_comp_d (φ : AffHom F G) (i : ℕ) :
    φ.cochainMap K (i + 1) ∘ₗ F.d K i = G.d K i ∘ₗ φ.cochainMap K i
def

kerMap

L232 ↗
AlgebraicGeometry.OModulePresheaf.AffHom.kerMap
Documentation

The induced map on the kernels of the Cech differentials.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
section Cochains
variable [IsSeparated π] (K : V.OrderedAffineCover) {F G : OModulePresheaf π}
Lean source · statement
def AffHom.kerMap (φ : AffHom F G) (i : ℕ) :
    LinearMap.ker (F.d K i) →ₗ[R] LinearMap.ker (G.d K i)
theorem

kerMap_coe

L238 ↗
AlgebraicGeometry.OModulePresheaf.AffHom.kerMap_coe
Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
section Cochains
variable [IsSeparated π] (K : V.OrderedAffineCover) {F G : OModulePresheaf π}
Lean source · statement
theorem AffHom.kerMap_coe (φ : AffHom F G) (i : ℕ) (x : LinearMap.ker (F.d K i)) :
    (φ.kerMap K i x : G.cochain K i) = φ.cochainMap K i x
abbrev

H0Map

L242 ↗
AlgebraicGeometry.OModulePresheaf.AffHom.H0Map
Documentation

The induced map on zeroth Cech cohomology.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
section Cochains
variable [IsSeparated π] (K : V.OrderedAffineCover) {F G : OModulePresheaf π}
Lean source · statement
abbrev AffHom.H0Map (φ : AffHom F G) : F.H0 K →ₗ[R] G.H0 K
def

HSuccMap

L245 ↗
AlgebraicGeometry.OModulePresheaf.AffHom.HSuccMap
Documentation

The induced map on Cech cohomology in degree i + 1.

Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
section Cochains
variable [IsSeparated π] (K : V.OrderedAffineCover) {F G : OModulePresheaf π}
Lean source · statement
def AffHom.HSuccMap (φ : AffHom F G) (i : ℕ) : F.HSucc K i →ₗ[R] G.HSucc K i
theorem

HSuccMap_mk

L253 ↗
AlgebraicGeometry.OModulePresheaf.AffHom.HSuccMap_mk
Source context 9 commands

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

noncomputable section
universe u
namespace AlgebraicGeometry
open CategoryTheory Opposite Limits
variable {R : Type u} [CommRing R] {V : Scheme.{u}}
namespace OModulePresheaf
variable {π : V ⟶ Spec (.of R)}
section Cochains
variable [IsSeparated π] (K : V.OrderedAffineCover) {F G : OModulePresheaf π}
Lean source · statement
theorem AffHom.HSuccMap_mk (φ : AffHom F G) (i : ℕ) (x : LinearMap.ker (F.d K (i + 1))) :
    φ.HSuccMap K i (Submodule.Quotient.mk x) = Submodule.Quotient.mk (φ.kerMap K (i + 1) x)

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