NYLL
Module

CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const.lean

Nyll.AlgebraicCurves.Cohomology.Cech.CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
34 declarations indexed from sourceView source ↗

Module documentation

Projective kernels of two-term complexes over a reduced ring. Constant fibre-kernel dimension gives projectivity and bijective kernel base change.

Imports22
  • Mathlib.Algebra.Module.Projective
  • Mathlib.RingTheory.Nilpotent.Defs
  • Nyll.SchemeTheory.Cohomology.Sheaves.CoherentBaseChange
  • Mathlib.Algebra.Module.FinitePresentation
  • Mathlib.LinearAlgebra.Dimension.Constructions
  • Mathlib.LinearAlgebra.Dimension.RankNullity
  • Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  • Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
  • Mathlib.LinearAlgebra.LinearIndependent.Lemmas
  • Mathlib.LinearAlgebra.TensorProduct.Pi
  • Mathlib.LinearAlgebra.TensorProduct.RightExactness
  • Mathlib.RingTheory.TensorProduct.Finite
  • Mathlib.RingTheory.TensorProduct.Free
  • Mathlib.RingTheory.Support
  • Mathlib.RingTheory.LocalRing.Module
  • Mathlib.RingTheory.LocalProperties.Projective
  • Mathlib.RingTheory.LocalProperties.Reduced
  • Mathlib.RingTheory.Localization.Integer
  • Mathlib.RingTheory.Localization.Ideal
  • Mathlib.RingTheory.Localization.BaseChange
  • Mathlib.RingTheory.Nilpotent.Lemmas
  • Mathlib.RingTheory.Noetherian.Basic
Imported by2

Declarations

def

kerRetraction

L62 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const.CBCSol.kerRetraction
Documentation

Retract the source onto the kernel using a section of the differential.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CBCSol
section SplitKer
variable {R : Type u} [CommRing R]
variable {M : Type v} [AddCommGroup M] [Module R M]
variable {N : Type w} [AddCommGroup N] [Module R N]
Lean source · statement
def kerRetraction (d : M →ₗ[R] N) {s : N →ₗ[R] M} (hs : d ∘ₗ s = LinearMap.id) :
    M →ₗ[R] LinearMap.ker d
theorem

kerRetraction_apply_coe

L68 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const.CBCSol.kerRetraction_apply_coe
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CBCSol
section SplitKer
variable {R : Type u} [CommRing R]
variable {M : Type v} [AddCommGroup M] [Module R M]
variable {N : Type w} [AddCommGroup N] [Module R N]
Lean source · statement
theorem kerRetraction_apply_coe (d : M →ₗ[R] N) {s : N →ₗ[R] M}
    (hs : d ∘ₗ s = LinearMap.id) (x : M) :
    (kerRetraction d hs x : M) = x - s (d x)
theorem

kerRetraction_comp_subtype

L72 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const.CBCSol.kerRetraction_comp_subtype
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CBCSol
section SplitKer
variable {R : Type u} [CommRing R]
variable {M : Type v} [AddCommGroup M] [Module R M]
variable {N : Type w} [AddCommGroup N] [Module R N]
Lean source · statement
theorem kerRetraction_comp_subtype (d : M →ₗ[R] N) {s : N →ₗ[R] M}
    (hs : d ∘ₗ s = LinearMap.id) :
    (kerRetraction d hs) ∘ₗ (LinearMap.ker d).subtype = LinearMap.id
def

kerBaseChangeHomOf

L82 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const.CBCSol.kerBaseChangeHomOf
Documentation

The canonical map from the base-changed kernel to the kernel of the base-changed map.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CBCSol
section SplitKer
variable {R : Type u} [CommRing R]
variable {M : Type v} [AddCommGroup M] [Module R M]
variable {N : Type w} [AddCommGroup N] [Module R N]
variable (A : Type*) [CommRing A] [Algebra R A]
Lean source · statement
def kerBaseChangeHomOf (d : M →ₗ[R] N) :
    A ⊗[R] (LinearMap.ker d) →ₗ[A] LinearMap.ker (d.baseChange A)
theorem

kerBaseChangeHomOf_apply_coe

L89 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const.CBCSol.kerBaseChangeHomOf_apply_coe
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CBCSol
section SplitKer
variable {R : Type u} [CommRing R]
variable {M : Type v} [AddCommGroup M] [Module R M]
variable {N : Type w} [AddCommGroup N] [Module R N]
variable (A : Type*) [CommRing A] [Algebra R A]
Lean source · statement
theorem kerBaseChangeHomOf_apply_coe (d : M →ₗ[R] N) (x : A ⊗[R] (LinearMap.ker d)) :
    (kerBaseChangeHomOf A d x : A ⊗[R] M) = (LinearMap.ker d).subtype.baseChange A x
theorem

kerBaseChangeHomOf_bijective

L92 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const.CBCSol.kerBaseChangeHomOf_bijective
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CBCSol
section SplitKer
variable {R : Type u} [CommRing R]
variable {M : Type v} [AddCommGroup M] [Module R M]
variable {N : Type w} [AddCommGroup N] [Module R N]
variable (A : Type*) [CommRing A] [Algebra R A]
Lean source · statement
theorem kerBaseChangeHomOf_bijective [Module.Projective R N] (d : M →ₗ[R] N)
    (hd : Function.Surjective d) :
    Function.Bijective (kerBaseChangeHomOf A d)
theorem

projective_ker_of_surjective_of_projective

L113 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const.CBCSol.projective_ker_of_surjective_of_projective
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CBCSol
section SplitKer
variable {R : Type u} [CommRing R]
variable {M : Type v} [AddCommGroup M] [Module R M]
variable {N : Type w} [AddCommGroup N] [Module R N]
variable (A : Type*) [CommRing A] [Algebra R A]
Lean source · statement
theorem projective_ker_of_surjective_of_projective
    [Module.Projective R M] [Module.Projective R N]
    (d : M →ₗ[R] N) (hd : Function.Surjective d) :
    Module.Projective R (LinearMap.ker d)
theorem

finite_ker_of_surjective_of_projective

L121 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const.CBCSol.finite_ker_of_surjective_of_projective
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CBCSol
section SplitKer
variable {R : Type u} [CommRing R]
variable {M : Type v} [AddCommGroup M] [Module R M]
variable {N : Type w} [AddCommGroup N] [Module R N]
variable (A : Type*) [CommRing A] [Algebra R A]
Lean source · statement
theorem finite_ker_of_surjective_of_projective
    [Module.Finite R M] [Module.Projective R N]
    (d : M →ₗ[R] N) (hd : Function.Surjective d) :
    Module.Finite R (LinearMap.ker d)
abbrev

κ

L137 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const.CBCSol.κ
Documentation

The residue field at a prime of the base ring.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CBCSol
section FittingFree
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
Lean source · statement
abbrev κ (𝔭 : PrimeSpectrum R) : Type u
theorem

span_one_tmul_eq_top

L139 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const.CBCSol.span_one_tmul_eq_top
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CBCSol
section FittingFree
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
Lean source · full declaration
theorem span_one_tmul_eq_top (𝔭 : PrimeSpectrum R) :
    Submodule.span (κ 𝔭) (Set.range fun x : M => (1 : κ 𝔭) ⊗ₜ[R] x) = ⊤ := by
  rw [eq_top_iff]
  rintro t -
  induction t using TensorProduct.inductionOn with
  | tmul a x =>
    have : a ⊗ₜ[R] x = a • ((1 : κ 𝔭) ⊗ₜ[R] x) := by
      rw [TensorProduct.smul_tmul', smul_eq_mul, mul_one]
    rw [this]
    exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨x, rfl⟩)
  | add s t hs ht => exact Submodule.add_mem _ hs ht
theorem

exists_basis_one_tmul

L151 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const.CBCSol.exists_basis_one_tmul
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CBCSol
section FittingFree
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
Lean source · statement
theorem exists_basis_one_tmul [Module.Finite R M] (𝔭 : PrimeSpectrum R) :
    ∃ (ι : Type v) (_ : Fintype ι) (m : ι → M) (b : Module.Basis ι (κ 𝔭) (κ 𝔭 ⊗[R] M)),
      ∀ i, b i = (1 : κ 𝔭) ⊗ₜ[R] m i
theorem

subsingleton_residue_tensor_coker

L162 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const.CBCSol.subsingleton_residue_tensor_coker
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CBCSol
section FittingFree
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
Lean source · statement
theorem subsingleton_residue_tensor_coker (𝔭 : PrimeSpectrum R) {ι : Type v} [Fintype ι]
    (m : ι → M) (b : Module.Basis ι (κ 𝔭) (κ 𝔭 ⊗[R] M)) (hb : ∀ i, b i = (1 : κ 𝔭) ⊗ₜ[R] m i) :
    Subsingleton (κ 𝔭 ⊗[R] (M ⧸ LinearMap.range (Fintype.linearCombination R m)))
theorem

baseChange_injective_of_le

L189 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const.CBCSol.baseChange_injective_of_le
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CBCSol
section FittingFree
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
Lean source · statement
theorem baseChange_injective_of_le [Module.Finite R M] {e : ℕ}
    (hconst : ∀ 𝔮 : PrimeSpectrum R, Module.finrank (κ 𝔮) (κ 𝔮 ⊗[R] M) = e)
    (𝔭 : PrimeSpectrum R) {ι : Type v}
    [Fintype ι] (m : ι → M) (b : Module.Basis ι (κ 𝔭) (κ 𝔭 ⊗[R] M))
    (hb : ∀ i, b i = (1 : κ 𝔭) ⊗ₜ[R] m i) {𝔮 : PrimeSpectrum R} (hle : 𝔮 ≤ 𝔭) :
    Function.Injective ((Fintype.linearCombination R m).baseChange (κ 𝔮))
theorem

coeff_mem_of_rel

L227 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const.CBCSol.coeff_mem_of_rel
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CBCSol
section FittingFree
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
Lean source · statement
theorem coeff_mem_of_rel [Module.Finite R M] {e : ℕ}
    (hconst : ∀ 𝔮 : PrimeSpectrum R, Module.finrank (κ 𝔮) (κ 𝔮 ⊗[R] M) = e)
    (𝔭 : PrimeSpectrum R) {ι : Type v} [Fintype ι]
    (m : ι → M) (b : Module.Basis ι (κ 𝔭) (κ 𝔭 ⊗[R] M))
    (hb : ∀ i, b i = (1 : κ 𝔭) ⊗ₜ[R] m i) {𝔮 : PrimeSpectrum R} (hle : 𝔮 ≤ 𝔭)
    (x : ι → R) (hx : Fintype.linearCombination R m x = 0) (i : ι) : x i ∈ 𝔮.asIdeal
theorem

algebraMap_coeff_eq_zero

L245 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const.CBCSol.algebraMap_coeff_eq_zero
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CBCSol
section FittingFree
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
Lean source · statement
theorem algebraMap_coeff_eq_zero [IsReduced R] [Module.Finite R M] {e : ℕ}
    (hconst : ∀ 𝔮 : PrimeSpectrum R, Module.finrank (κ 𝔮) (κ 𝔮 ⊗[R] M) = e)
    (𝔭 : PrimeSpectrum R)
    {ι : Type v} [Fintype ι] (m : ι → M) (b : Module.Basis ι (κ 𝔭) (κ 𝔭 ⊗[R] M))
    (hb : ∀ i, b i = (1 : κ 𝔭) ⊗ₜ[R] m i)
    (x : ι → R) (hx : Fintype.linearCombination R m x = 0) (i : ι) :
    algebraMap R (Localization.AtPrime 𝔭.asIdeal) (x i) = 0
theorem

free_localizedModule_of_isReduced

L265 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const.CBCSol.free_localizedModule_of_isReduced
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CBCSol
section FittingFree
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
Lean source · statement
theorem free_localizedModule_of_isReduced [IsReduced R] [Module.Finite R M] {e : ℕ}
    (hconst : ∀ 𝔮 : PrimeSpectrum R, Module.finrank (κ 𝔮) (κ 𝔮 ⊗[R] M) = e)
    (𝔭 : PrimeSpectrum R) :
    Module.Free (Localization.AtPrime 𝔭.asIdeal)
      (LocalizedModule 𝔭.asIdeal.primeCompl M)
theorem

projective_of_isReduced_of_finrank_const

L318 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const.CBCSol.projective_of_isReduced_of_finrank_const
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CBCSol
section FittingFree
variable {R : Type u} [CommRing R] {M : Type v} [AddCommGroup M] [Module R M]
Lean source · statement
theorem projective_of_isReduced_of_finrank_const [IsReduced R] [Module.FinitePresentation R M]
    {e : ℕ} (hconst : ∀ 𝔮 : PrimeSpectrum R, Module.finrank (κ 𝔮) (κ 𝔮 ⊗[R] M) = e) :
    Module.Projective R M
def

fibreRank

L340 ↗
CoherentBaseChange.TwoTermComplex.fibreRank
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
Lean source · statement
def _root_.CoherentBaseChange.TwoTermComplex.fibreRank (𝔭 : PrimeSpectrum R) : ℕ
theorem

fibreH0_add_fibreRank

L344 ↗
CoherentBaseChange.TwoTermComplex.fibreH0_add_fibreRank
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
open _root_.CoherentBaseChange.TwoTermComplex
Lean source · statement
theorem _root_.CoherentBaseChange.TwoTermComplex.fibreH0_add_fibreRank (𝔭 : PrimeSpectrum
    R) :
    G.fibreH0 𝔭 + G.fibreRank 𝔭 = Module.finrank (κ 𝔭) (κ 𝔭 ⊗[R] G.C0)
theorem

fibreRank_add_fibreH1

L353 ↗
CoherentBaseChange.TwoTermComplex.fibreRank_add_fibreH1
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
Lean source · statement
theorem _root_.CoherentBaseChange.TwoTermComplex.fibreRank_add_fibreH1 (𝔭 : PrimeSpectrum
    R) :
    G.fibreRank 𝔭 + G.fibreH1 𝔭 = Module.finrank (κ 𝔭) (κ 𝔭 ⊗[R] G.C1)
theorem

fibre_euler

L365 ↗
CoherentBaseChange.TwoTermComplex.fibre_euler
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
Lean source · statement
theorem _root_.CoherentBaseChange.TwoTermComplex.fibre_euler [StrongRankCondition R] (𝔭 :
    PrimeSpectrum R) :
    (G.fibreH0 𝔭 : ℤ) - (G.fibreH1 𝔭 : ℤ)
      = (Module.finrank R G.C0 : ℤ) - (Module.finrank R G.C1 : ℤ)
abbrev

coker

L380 ↗
CoherentBaseChange.TwoTermComplex.coker
Source context 19 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
Lean source · statement
abbrev _root_.CoherentBaseChange.TwoTermComplex.coker : Type v
instance

coker_finitePresentation

L383 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const.CoherentBaseChange.TwoTermComplex.coker_finitePresentation
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
Lean source · statement
instance coker_finitePresentation : Module.FinitePresentation R G.coker
def

cokerBaseChangeEquiv

L389 ↗
CoherentBaseChange.TwoTermComplex.cokerBaseChangeEquiv
Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
Lean source · statement
def _root_.CoherentBaseChange.TwoTermComplex.cokerBaseChangeEquiv (𝔭 : PrimeSpectrum R) :
    ((κ 𝔭 ⊗[R] G.C1) ⧸ LinearMap.range (G.d.baseChange (κ 𝔭))) ≃ₗ[κ 𝔭] κ 𝔭 ⊗[R] G.coker
theorem

finrank_residue_tensor_coker

L402 ↗
CoherentBaseChange.TwoTermComplex.finrank_residue_tensor_coker
Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
Lean source · statement
theorem _root_.CoherentBaseChange.TwoTermComplex.finrank_residue_tensor_coker (𝔭 :
    PrimeSpectrum R) :
    Module.finrank (κ 𝔭) (κ 𝔭 ⊗[R] G.coker) = G.fibreH1 𝔭
theorem

fibreH1_eq_of_fibreH0_const

L409 ↗
CoherentBaseChange.TwoTermComplex.fibreH1_eq_of_fibreH0_const
Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
Lean source · statement
theorem _root_.CoherentBaseChange.TwoTermComplex.fibreH1_eq_of_fibreH0_const {c : ℕ} (h0 :
    ∀ 𝔭, G.fibreH0 𝔭 = c)
    (𝔭 𝔮 : PrimeSpectrum R) : G.fibreH1 𝔭 = G.fibreH1 𝔮
theorem

projective_coker_of_isReduced_of_fibreH0_const

L423 ↗
CoherentBaseChange.TwoTermComplex.projective_coker_of_isReduced_of_fibreH0_const
Source context 23 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
Lean source · statement
theorem
    _root_.CoherentBaseChange.TwoTermComplex.projective_coker_of_isReduced_of_fibreH0_const
    [IsReduced R] {c : ℕ}
    (h0 : ∀ 𝔭, G.fibreH0 𝔭 = c) : Module.Projective R G.coker
theorem

exists_retraction_range

L435 ↗
CoherentBaseChange.TwoTermComplex.exists_retraction_range
Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
Lean source · statement
theorem _root_.CoherentBaseChange.TwoTermComplex.exists_retraction_range
    [Module.Projective R G.coker] :
    ∃ r : G.C1 →ₗ[R] LinearMap.range G.d,
      r ∘ₗ (LinearMap.range G.d).subtype = LinearMap.id
theorem

projective_range_of_isReduced_of_fibreH0_const

L456 ↗
CoherentBaseChange.TwoTermComplex.projective_range_of_isReduced_of_fibreH0_const
Source context 25 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
Lean source · statement
theorem
    _root_.CoherentBaseChange.TwoTermComplex.projective_range_of_isReduced_of_fibreH0_const
    [IsReduced R] {c : ℕ}
    (h0 : ∀ 𝔭, G.fibreH0 𝔭 = c) : Module.Projective R (LinearMap.range G.d)
theorem

projective_ker_of_isReduced_impl

L466 ↗
CoherentBaseChange.TwoTermComplex.projective_ker_of_isReduced_impl
Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
Lean source · statement
theorem _root_.CoherentBaseChange.TwoTermComplex.projective_ker_of_isReduced_impl
    [IsReduced R] {c : ℕ}
    (h0 : ∀ 𝔭, G.fibreH0 𝔭 = c) : Module.Projective R (LinearMap.ker G.d)
theorem

kerBaseChangeHom_eq

L476 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const.CoherentBaseChange.TwoTermComplex.kerBaseChangeHom_eq
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
Lean source · statement
theorem kerBaseChangeHom_eq (A : Type w) [CommRing A] [Algebra R A] :
    G.kerBaseChangeHom A = kerBaseChangeHomOf A G.d
theorem

kerBaseChangeHom_bijective_of_isReduced_impl

L479 ↗
CoherentBaseChange.TwoTermComplex.kerBaseChangeHom_bijective_of_isReduced_impl
Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
Lean source · statement
theorem
    _root_.CoherentBaseChange.TwoTermComplex.kerBaseChangeHom_bijective_of_isReduced_impl
    [IsReduced R] {c : ℕ}
    (h0 : ∀ 𝔭, G.fibreH0 𝔭 = c) (A : Type w) [CommRing A] [Algebra R A] :
    Function.Bijective (G.kerBaseChangeHom A)
theorem

finrank_residue_ker_of_isReduced_impl

L536 ↗
CoherentBaseChange.TwoTermComplex.finrank_residue_ker_of_isReduced_impl
Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
namespace CoherentBaseChange
open _root_.CoherentBaseChange
namespace TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange
open CBCSol
variable {R : Type u} [CommRing R] (G : TwoTermComplex.{u, v} R)
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
open _root_.CoherentBaseChange.TwoTermComplex
Lean source · statement
theorem _root_.CoherentBaseChange.TwoTermComplex.finrank_residue_ker_of_isReduced_impl
    [IsReduced R] {c : ℕ}
    (h0 : ∀ 𝔭, G.fibreH0 𝔭 = c) (𝔭 : PrimeSpectrum R) :
    Module.finrank (κ 𝔭) (κ 𝔭 ⊗[R] LinearMap.ker G.d) = c
theorem

projective_ker_of_isReduced_of_fibreH0_const

L547 ↗
CoherentBaseChange.TwoTermComplex.projective_ker_of_isReduced_of_fibreH0_const
Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
noncomputable section
universe u v w
open scoped TensorProduct
open _root_.CoherentBaseChange
Lean source · statement
theorem _root_.CoherentBaseChange.TwoTermComplex.projective_ker_of_isReduced_of_fibreH0_const
    {R : Type u} [CommRing R] [IsReduced R] (G : TwoTermComplex.{u, v} R) {c : ℕ}
    (h0 : ∀ 𝔭 : PrimeSpectrum R, G.fibreH0 𝔭 = c) :
    Module.Projective R (LinearMap.ker G.d) ∧
      (∀ (A : Type w) [CommRing A] [Algebra R A], Function.Bijective (G.kerBaseChangeHom A)) ∧
      ∀ 𝔭 : PrimeSpectrum R, Module.finrank 𝔭.asIdeal.ResidueField
        (𝔭.asIdeal.ResidueField ⊗[R] LinearMap.ker G.d) = c

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