Module

TwoChartCech_isLocallyConstant_fibreEulerChar.lean

Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_isLocallyConstant_fibreEulerChar

3 declarations indexed from sourceView source ↗

Module documentation

Local constancy of the fibre kernel-minus-cokernel dimension of a finite flat two-term model.

Imports12

Nyll.AlgebraicCurves.Geometry.Schemes.MumfordTruncation
Nyll.SchemeTheory.Cohomology.Cech.TwoChartCech
Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_Mumford_finite_K0
Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_Mumford_flat_K0
Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_Mumford_bijective_kerMapBaseChange
Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_Mumford_bijective_cokerMapBaseChange
Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Mathlib.RingTheory.Flat.Basic
Mathlib.RingTheory.Noetherian.Basic
Mathlib.Algebra.Module.FinitePresentation
Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Mathlib.RingTheory.TensorProduct.Finite

Imported by4

theorem

finrank_ker_sub_finrank_coker

L51 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_isLocallyConstant_fibreEulerChar.TwoChartCech.Mumford.finrank_ker_sub_finrank_coker

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_isLocallyConstant_fibreEulerChar
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]

Lean source · statement

theorem finrank_ker_sub_finrank_coker {K : Type u} [Field K] {V W : Type u} [AddCommGroup V]
    [Module K V]
    [AddCommGroup W] [Module K W] [Module.Finite K V] [Module.Finite K W] (f : V →ₗ[K] W) :
    (Module.finrank K (LinearMap.ker f) : ℤ) - Module.finrank K (W ⧸ LinearMap.range f)
      = (Module.finrank K V : ℤ) - Module.finrank K W

theorem

fibreEulerChar_eq_of_bijective

L60 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_isLocallyConstant_fibreEulerChar.TwoChartCech.Mumford.fibreEulerChar_eq_of_bijective

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_isLocallyConstant_fibreEulerChar
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace Mumford
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech.Mumford
open _root_.TwoChartCech
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]

Lean source · statement

theorem fibreEulerChar_eq_of_bijective [Module.Flat R C0] [Module.Flat R C1] [IsNoetherianRing R]
    [Module.Finite R (LinearMap.ker d)] (𝔭 : PrimeSpectrum R)
    (hker : Function.Bijective
      (kerMapBaseChange (dK d) d (ι0 d) (ι1 d) (comm d) 𝔭.asIdeal.ResidueField))
    (hcoker : Function.Bijective
      (cokerMapBaseChange (dK d) d (ι0 d) (ι1 d) (comm d) 𝔭.asIdeal.ResidueField)) :
    (Module.finrank 𝔭.asIdeal.ResidueField
        (LinearMap.ker (d.baseChange 𝔭.asIdeal.ResidueField)) : ℤ)
      - Module.finrank 𝔭.asIdeal.ResidueField
          ((𝔭.asIdeal.ResidueField ⊗[R] C1) ⧸ LinearMap.range (d.baseChange 𝔭.asIdeal.ResidueField))
    = (Module.rankAtStalk (K0 d) 𝔭 : ℤ) - Module.rankAtStalk (Fin (rank d) → R) 𝔭

theorem

isLocallyConstant_fibreEulerChar

L82 ↗

TwoChartCech.isLocallyConstant_fibreEulerChar

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_isLocallyConstant_fibreEulerChar
noncomputable section
open scoped TensorProduct
universe u
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs in
open _root_.TwoChartCech TwoChartCech_isLocallyConstant_fibreEulerChar.TwoChartCech
  _root_.TwoChartCech.Mumford TwoChartCech_isLocallyConstant_fibreEulerChar.TwoChartCech.Mumford
  in

Lean source · full declaration

theorem _root_.TwoChartCech.isLocallyConstant_fibreEulerChar
    {R : Type u} [CommRing R] [IsNoetherianRing R]
    {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
    [Module.Flat R C0] [Module.Flat R C1] (d : C0 →ₗ[R] C1)
    [Module.Finite R (LinearMap.ker d)] [Module.Finite R (C1 ⧸ LinearMap.range d)] :
    IsLocallyConstant fun 𝔭 : PrimeSpectrum R =>
      (Module.finrank 𝔭.asIdeal.ResidueField
          (LinearMap.ker (d.baseChange 𝔭.asIdeal.ResidueField)) : ℤ)
        - Module.finrank 𝔭.asIdeal.ResidueField
            ((𝔭.asIdeal.ResidueField ⊗[R] C1) ⧸ LinearMap.range (d.baseChange
              𝔭.asIdeal.ResidueField)) := by
  have := Mumford.finite_K0 d; have := Mumford.flat_K0 d
  have : Module.FinitePresentation R (Mumford.K0 d) := Module.finitePresentation_of_finite R _
  have h0 : IsLocallyConstant (Module.rankAtStalk (R := R) (Mumford.K0 d)) :=
    Module.isLocallyConstant_rankAtStalk
  have h1 : IsLocallyConstant (Module.rankAtStalk (R := R) (Fin (Mumford.rank d) → R)) :=
    Module.isLocallyConstant_rankAtStalk
  have h := (h0.prodMk h1).comp (fun p : ℕ × ℕ => (p.1 : ℤ) - p.2)
  convert h using 1
  funext 𝔭
  exact Mumford.fibreEulerChar_eq_of_bijective d 𝔭 (Mumford.bijective_kerMapBaseChange d _)
    (Mumford.bijective_cokerMapBaseChange d _)

Module documentation

Declarations

finrank_ker_sub_finrank_coker

fibreEulerChar_eq_of_bijective

isLocallyConstant_fibreEulerChar