Module

CoherentBaseChange.lean

Nyll.SchemeTheory.Cohomology.Sheaves.CoherentBaseChange

7 declarations indexed from sourceView source ↗

Module documentation

Finite free two-term complexes, their fibre dimensions and the canonical kernel base-change map.

Imports7

Mathlib.LinearAlgebra.TensorProduct.Tower
Mathlib.LinearAlgebra.Dimension.Finrank
Mathlib.LinearAlgebra.FreeModule.Basic
Mathlib.LinearAlgebra.Quotient.Defs
Mathlib.RingTheory.Finiteness.Defs
Mathlib.RingTheory.Spectrum.Prime.Defs
Mathlib.RingTheory.LocalRing.ResidueField.Ideal

Imported by15

structure

TwoTermComplex

L34 ↗

CoherentBaseChange.TwoTermComplex

Documentation

A two-term complex of finite free R-modules in degrees zero and one.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace CoherentBaseChange

Lean source · full declaration

structure TwoTermComplex (R : Type u) [CommRing R] where
  /-- The underlying type of the degree-zero module. -/
  C0 : Type v
  /-- The additive commutative group structure on the degree-zero module. -/
  [C0_addCommGroup : AddCommGroup C0]
  /-- The R-module structure on the degree-zero module. -/
  [C0_module : Module R C0]
  /-- The degree-zero module is finitely generated over R. -/
  [C0_finite : Module.Finite R C0]
  /-- The degree-zero module is free over R. -/
  [C0_free : Module.Free R C0]
  /-- The underlying type of the degree-one module. -/
  C1 : Type v
  /-- The additive commutative group structure on the degree-one module. -/
  [C1_addCommGroup : AddCommGroup C1]
  /-- The R-module structure on the degree-one module. -/
  [C1_module : Module R C1]
  /-- The degree-one module is finitely generated over R. -/
  [C1_finite : Module.Finite R C1]
  /-- The degree-one module is free over R. -/
  [C1_free : Module.Free R C1]
  /-- The differential from degree zero to degree one. -/
  d : C0 →ₗ[R] C1

def

fibreH0

L67 ↗

CoherentBaseChange.TwoTermComplex.fibreH0

Documentation

The dimension of the kernel after base change to the residue field at the given prime.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace CoherentBaseChange
attribute [instance] TwoTermComplex.C0_addCommGroup TwoTermComplex.C0_module
  TwoTermComplex.C0_finite TwoTermComplex.C0_free TwoTermComplex.C1_addCommGroup
  TwoTermComplex.C1_module TwoTermComplex.C1_finite TwoTermComplex.C1_free
namespace TwoTermComplex
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)

Lean source · statement

def fibreH0 (𝔭 : PrimeSpectrum R) : ℕ

def

fibreH1

L72 ↗

CoherentBaseChange.TwoTermComplex.fibreH1

Documentation

The dimension of the cokernel after base change to the residue field at the given prime.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace CoherentBaseChange
attribute [instance] TwoTermComplex.C0_addCommGroup TwoTermComplex.C0_module
  TwoTermComplex.C0_finite TwoTermComplex.C0_free TwoTermComplex.C1_addCommGroup
  TwoTermComplex.C1_module TwoTermComplex.C1_finite TwoTermComplex.C1_free
namespace TwoTermComplex
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)

Lean source · statement

def fibreH1 (𝔭 : PrimeSpectrum R) : ℕ

def

chi

L77 ↗

CoherentBaseChange.TwoTermComplex.chi

Documentation

The Euler characteristic given by the degree-zero rank minus the degree-one rank.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace CoherentBaseChange
attribute [instance] TwoTermComplex.C0_addCommGroup TwoTermComplex.C0_module
  TwoTermComplex.C0_finite TwoTermComplex.C0_free TwoTermComplex.C1_addCommGroup
  TwoTermComplex.C1_module TwoTermComplex.C1_finite TwoTermComplex.C1_free
namespace TwoTermComplex
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)

Lean source · statement

def chi : ℤ

abbrev

H0

L81 ↗

CoherentBaseChange.TwoTermComplex.H0

Documentation

The kernel of the differential after base change to A.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace CoherentBaseChange
attribute [instance] TwoTermComplex.C0_addCommGroup TwoTermComplex.C0_module
  TwoTermComplex.C0_finite TwoTermComplex.C0_free TwoTermComplex.C1_addCommGroup
  TwoTermComplex.C1_module TwoTermComplex.C1_finite TwoTermComplex.C1_free
namespace TwoTermComplex
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)

Lean source · statement

abbrev H0 (A : Type w) [CommRing A] [Algebra R A] : Submodule A (A ⊗[R] G.C0)

def

kerBaseChangeHom

L86 ↗

CoherentBaseChange.TwoTermComplex.kerBaseChangeHom

Documentation

The natural map from the base change of the original kernel to the kernel of the base-changed differential.

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace CoherentBaseChange
attribute [instance] TwoTermComplex.C0_addCommGroup TwoTermComplex.C0_module
  TwoTermComplex.C0_finite TwoTermComplex.C0_free TwoTermComplex.C1_addCommGroup
  TwoTermComplex.C1_module TwoTermComplex.C1_finite TwoTermComplex.C1_free
namespace TwoTermComplex
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)

Lean source · statement

def kerBaseChangeHom (A : Type w) [CommRing A] [Algebra R A] :
    A ⊗[R] (LinearMap.ker G.d) →ₗ[A] G.H0 A

theorem

kerBaseChangeHom_apply_coe

L96 ↗

CoherentBaseChange.TwoTermComplex.kerBaseChangeHom_apply_coe

Source context 7 commands

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

noncomputable section
open scoped TensorProduct
universe u v w
namespace CoherentBaseChange
attribute [instance] TwoTermComplex.C0_addCommGroup TwoTermComplex.C0_module
  TwoTermComplex.C0_finite TwoTermComplex.C0_free TwoTermComplex.C1_addCommGroup
  TwoTermComplex.C1_module TwoTermComplex.C1_finite TwoTermComplex.C1_free
namespace TwoTermComplex
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)

Lean source · statement

theorem kerBaseChangeHom_apply_coe (A : Type w) [CommRing A] [Algebra R A]
    (x : A ⊗[R] (LinearMap.ker G.d)) :
    (G.kerBaseChangeHom A x : A ⊗[R] G.C0) = (LinearMap.ker G.d).subtype.baseChange A x

Module documentation

Declarations

TwoTermComplex

fibreH0

fibreH1

chi

H0

kerBaseChangeHom

kerBaseChangeHom_apply_coe