NYLL
Module

CoherentBaseChange_TwoTermComplex_exists_nonempty_H0_linearEquiv_annihilator_of_fibreH0_le_one.lean

Nyll.AlgebraicCurves.Cohomology.Cech.CoherentBaseChange_TwoTermComplex_exists_nonempty_H0_linearEquiv_annihilator_of_fibreH0_le_one
40 declarations indexed from sourceView source ↗

Module documentation

Coherent Base Change Two Term Complex exists nonempty H0 linear Equiv annihilator of fibre

H0 le one

Imports26
  • Mathlib.Algebra.Exact.Basic
  • Mathlib.Algebra.GroupWithZero.Units.Basic
  • Mathlib.Algebra.Module.Submodule.Equiv
  • Mathlib.LinearAlgebra.Dimension.Constructions
  • Mathlib.LinearAlgebra.Dimension.RankNullity
  • Mathlib.LinearAlgebra.FiniteDimensional.Basic
  • Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  • Mathlib.LinearAlgebra.FreeModule.Basic
  • Mathlib.LinearAlgebra.FreeModule.Finite.Basic
  • Mathlib.LinearAlgebra.Matrix.Rank
  • Mathlib.LinearAlgebra.Matrix.ToLin
  • Mathlib.LinearAlgebra.Quotient.Defs
  • Mathlib.LinearAlgebra.Span.Basic
  • Mathlib.LinearAlgebra.TensorProduct.RightExactness
  • Mathlib.LinearAlgebra.TensorProduct.Tower
  • Mathlib.RingTheory.Finiteness.Basic
  • Mathlib.RingTheory.Ideal.Maps
  • Mathlib.RingTheory.LocalRing.Module
  • Mathlib.RingTheory.LocalRing.ResidueField.Ideal
  • Mathlib.RingTheory.Support
  • Mathlib.RingTheory.TensorProduct.Finite
  • Mathlib.RingTheory.TensorProduct.Free
  • Mathlib.Tactic.Choose
  • Mathlib.Tactic.Push
  • Mathlib.Tactic.Ring
  • Nyll.SchemeTheory.Cohomology.Sheaves.CoherentBaseChange
Imported by2

Declarations

theorem

span_one_tmul_eq_top

L63 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.span_one_tmul_eq_top
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Nakayama
variable {V : Type u} [AddCommGroup V] [Module R V]
Lean source · statement
theorem span_one_tmul_eq_top (K : Type u) [CommRing K] [Algebra R K] (Q : Type u) [AddCommGroup Q]
    [Module R Q] : Submodule.span K (Set.range (TensorProduct.mk R K Q 1)) = ⊤
theorem

exists_span_singleton

L69 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.exists_span_singleton
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Nakayama
variable {V : Type u} [AddCommGroup V] [Module R V]
Lean source · statement
theorem exists_span_singleton (W : Submodule R V) (𝔭 : PrimeSpectrum R)
    (hle : Module.finrank 𝔭.asIdeal.ResidueField (𝔭.asIdeal.ResidueField ⊗[R] (V ⧸ W)) ≤ 1)
    [Module.Finite R V] :
    ∃ q : V, ∀ w : 𝔭.asIdeal.ResidueField ⊗[R] (V ⧸ W), ∃ c : 𝔭.asIdeal.ResidueField,
      c • ((1 : 𝔭.asIdeal.ResidueField) ⊗ₜ[R] Submodule.Quotient.mk q) = w
theorem

exists_generator

L101 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.exists_generator
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Nakayama
variable {V : Type u} [AddCommGroup V] [Module R V]
Lean source · statement
theorem exists_generator (W : Submodule R V) (𝔭 : PrimeSpectrum R) [Module.Finite R V]
    (hle : Module.finrank 𝔭.asIdeal.ResidueField (𝔭.asIdeal.ResidueField ⊗[R] (V ⧸ W)) ≤ 1) :
    ∃ (q : V) (h : R), h ∉ 𝔭.asIdeal ∧ ∀ v : V, ∃ r : R, h • v - r • q ∈ W
abbrev

ι0

L155 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.ι0
Documentation

The index type of the chosen basis of the degree-zero term.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Coordinates
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
Lean source · statement
abbrev ι0 : Type u
abbrev

ι1

L158 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.ι1
Documentation

The index type of the chosen basis of the degree-one term.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Coordinates
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
Lean source · statement
abbrev ι1 : Type u
abbrev

b0

L161 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.b0
Documentation

The chosen basis of the degree-zero term.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Coordinates
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
Lean source · statement
abbrev b0 : Module.Basis (ι0 G) R G.C0
abbrev

b1

L164 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.b1
Documentation

The chosen basis of the degree-one term.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Coordinates
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
Lean source · statement
abbrev b1 : Module.Basis (ι1 G) R G.C1
def

Dm

L167 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.Dm
Documentation

The matrix of the differential in the chosen bases.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Coordinates
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
Lean source · statement
def Dm : Matrix (ι1 G) (ι0 G) R
def

W

L172 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.W
Documentation

The row span of the differential matrix, expressed as the range of its transpose.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Coordinates
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
Lean source · statement
def W : Submodule R (ι0 G → R)
theorem

row_mem_W

L174 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.row_mem_W
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Coordinates
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
Lean source · full declaration
theorem row_mem_W (j : ι1 G) : (fun i => Dm G j i) ∈ W G := by
  classical
  refine LinearMap.mem_range.mpr ⟨Pi.single j 1, ?_⟩
  funext i
  rw [Matrix.mulVecLin_apply, Matrix.mulVec_single_one]
  rfl
theorem

mem_W_iff

L181 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.mem_W_iff
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Coordinates
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
Lean source · statement
theorem mem_W_iff (y : ι0 G → R) : y ∈ W G ↔ ∃ w : ι1 G → R, ∀ i, y i = ∑ j, Dm G j i * w j
def

Kmat

L194 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.Kmat
Documentation

The kernel of the differential matrix after extension of scalars.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Coordinates
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (B : Type u) [CommRing B] [Algebra R B]
Lean source · statement
def Kmat : Submodule B (ι0 G → B)
theorem

mem_Kmat_iff

L196 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.mem_Kmat_iff
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Coordinates
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (B : Type u) [CommRing B] [Algebra R B]
Lean source · statement
theorem mem_Kmat_iff (x : ι0 G → B) :
    x ∈ Kmat G B ↔ ∀ j, ∑ i, algebraMap R B (Dm G j i) * x i = 0
abbrev

β0

L208 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.β0
Documentation

The basis of the degree-zero term after extension of scalars.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Coordinates
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (B : Type u) [CommRing B] [Algebra R B]
Lean source · statement
abbrev β0 : Module.Basis (ι0 G) B (B ⊗[R] G.C0)
abbrev

β1

L211 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.β1
Documentation

The basis of the degree-one term after extension of scalars.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Coordinates
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (B : Type u) [CommRing B] [Algebra R B]
Lean source · statement
abbrev β1 : Module.Basis (ι1 G) B (B ⊗[R] G.C1)
theorem

Dm_map_eq

L213 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.Dm_map_eq
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Coordinates
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (B : Type u) [CommRing B] [Algebra R B]
Lean source · statement
theorem Dm_map_eq : (Dm G).map (algebraMap R B) = LinearMap.toMatrix (β0 G B) (β1 G B)
  (G.d.baseChange B)
theorem

repr_baseChange

L217 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.repr_baseChange
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Coordinates
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (B : Type u) [CommRing B] [Algebra R B]
Lean source · statement
theorem repr_baseChange (y : B ⊗[R] G.C0) :
    ((β1 G B).repr (G.d.baseChange B y) : ι1 G → B) = ((Dm G).map (algebraMap R B)) *ᵥ ((β0 G
      B).repr y)
theorem

mem_H0_iff

L222 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.mem_H0_iff
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Coordinates
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (B : Type u) [CommRing B] [Algebra R B]
Lean source · statement
theorem mem_H0_iff (y : B ⊗[R] G.C0) : y ∈ G.H0 B ↔ ((β0 G B).repr y : ι0 G → B) ∈ Kmat G B
def

H0Equiv

L234 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.H0Equiv
Documentation

Identify zeroth cohomology with the kernel of the base-changed matrix.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Coordinates
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (B : Type u) [CommRing B] [Algebra R B]
Lean source · statement
def H0Equiv : G.H0 B ≃ₗ[B] Kmat G B
def

baseChangeCokerEquiv

L241 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.baseChangeCokerEquiv
Documentation

Identify the cokernel after base change with the base change of the cokernel.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Coordinates
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (B : Type u) [CommRing B] [Algebra R B]
Lean source · statement
def baseChangeCokerEquiv {P Q : Type u} [AddCommGroup P] [Module R P] [AddCommGroup Q] [Module R Q]
    (φ : P →ₗ[R] Q) (A : Type u) [CommRing A] [Algebra R A] :
    ((A ⊗[R] Q) ⧸ LinearMap.range (φ.baseChange A)) ≃ₗ[A] A ⊗[R] (Q ⧸ LinearMap.range φ)
theorem

finrank_fibre_eq

L251 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.finrank_fibre_eq
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Coordinates
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (B : Type u) [CommRing B] [Algebra R B]
Lean source · statement
theorem finrank_fibre_eq (𝔭 : PrimeSpectrum R) :
    Module.finrank 𝔭.asIdeal.ResidueField (𝔭.asIdeal.ResidueField ⊗[R] ((ι0 G → R) ⧸ W G)) =
      G.fibreH0 𝔭
def

pair

L297 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.pair
Documentation

The coordinate pairing after mapping coefficients into the extension ring.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Pairing
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (B : Type u) [CommRing B] [Algebra R B]
Lean source · statement
def pair (v : ι0 G → R) (x : ι0 G → B) : B
theorem

pair_add_left

L299 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.pair_add_left
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Pairing
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (B : Type u) [CommRing B] [Algebra R B]
Lean source · statement
theorem pair_add_left (v v' : ι0 G → R) (x : ι0 G → B) : pair G B (v + v') x = pair G B v x +
  pair G B v' x
theorem

pair_smul_left

L303 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.pair_smul_left
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Pairing
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (B : Type u) [CommRing B] [Algebra R B]
Lean source · statement
theorem pair_smul_left (r : R) (v : ι0 G → R) (x : ι0 G → B) :
    pair G B (r • v) x = algebraMap R B r * pair G B v x
theorem

pair_sub_left

L307 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.pair_sub_left
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Pairing
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (B : Type u) [CommRing B] [Algebra R B]
Lean source · statement
theorem pair_sub_left (v v' : ι0 G → R) (x : ι0 G → B) : pair G B (v - v') x = pair G B v x -
  pair G B v' x
theorem

pair_single

L311 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.pair_single
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Pairing
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (B : Type u) [CommRing B] [Algebra R B]
Lean source · statement
theorem pair_single (i : ι0 G) (x : ι0 G → B) : pair G B (Pi.single i 1) x = x i
theorem

pair_add_right

L317 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.pair_add_right
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Pairing
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (B : Type u) [CommRing B] [Algebra R B]
Lean source · statement
theorem pair_add_right (v : ι0 G → R) (x x' : ι0 G → B) : pair G B v (x + x') = pair G B v x +
  pair G B v x'
theorem

pair_smul_right

L321 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.pair_smul_right
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Pairing
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (B : Type u) [CommRing B] [Algebra R B]
Lean source · statement
theorem pair_smul_right (b : B) (v : ι0 G → R) (x : ι0 G → B) : pair G B v (b • x) = b * pair G
  B v x
theorem

pair_eq_zero_of_mem_W

L325 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.pair_eq_zero_of_mem_W
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Pairing
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (B : Type u) [CommRing B] [Algebra R B]
Lean source · statement
theorem pair_eq_zero_of_mem_W {y : ι0 G → R} (hy : y ∈ W G) {x : ι0 G → B} (hx : x ∈ Kmat G B) :
    pair G B y x = 0
def

J

L339 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.J
Documentation

The ideal of scalars sending the chosen vector into the row span.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Pairing
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (B : Type u) [CommRing B] [Algebra R B]
variable (q : ι0 G → R) (h : R)
Lean source · statement
def J : Ideal R
theorem

mem_J_iff

L341 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.mem_J_iff
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Pairing
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (B : Type u) [CommRing B] [Algebra R B]
variable (q : ι0 G → R) (h : R)
Lean source · statement
theorem mem_J_iff (r : R) : r ∈ J G q ↔ r • q ∈ W G
def

Φ

L344 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.Φ
Documentation

Evaluation of the coordinate pairing against the chosen vector on the matrix kernel.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Pairing
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (B : Type u) [CommRing B] [Algebra R B]
variable (q : ι0 G → R) (h : R)
Lean source · full declaration
def Φ : Kmat G B →ₗ[B] B where
  toFun x := pair G B q x
  map_add' x x' := pair_add_right G B q x x'
  map_smul' b x := pair_smul_right G B b q x
theorem

Φ_apply

L349 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.Φ_apply
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Pairing
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (B : Type u) [CommRing B] [Algebra R B]
variable (q : ι0 G → R) (h : R)
Lean source · statement
theorem Φ_apply (x : Kmat G B) : Φ G B q x = pair G B q x
theorem

pair_eq

L356 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.pair_eq
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Pairing
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (B : Type u) [CommRing B] [Algebra R B]
variable (q : ι0 G → R) (h : R)
variable {q h}
variable (hE : ∀ v : ι0 G → R, ∃ r : R, h • v - r • q ∈ W G) (hu : IsUnit (algebraMap R B h))
include hE hu
omit hE hu in
Lean source · statement
theorem pair_eq (v : ι0 G → R) (r : R) (hr : h • v - r • q ∈ W G) (x : Kmat G B) :
    algebraMap R B h * pair G B v x = algebraMap R B r * Φ G B q x
theorem

Φ_injective

L362 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.Φ_injective
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Pairing
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (B : Type u) [CommRing B] [Algebra R B]
variable (q : ι0 G → R) (h : R)
variable {q h}
variable (hE : ∀ v : ι0 G → R, ∃ r : R, h • v - r • q ∈ W G) (hu : IsUnit (algebraMap R B h))
include hE hu
Lean source · statement
theorem Φ_injective : Function.Injective (Φ G B q)
theorem

Φ_mem

L375 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.Φ_mem
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Pairing
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (B : Type u) [CommRing B] [Algebra R B]
variable (q : ι0 G → R) (h : R)
variable {q h}
variable (hE : ∀ v : ι0 G → R, ∃ r : R, h • v - r • q ∈ W G) (hu : IsUnit (algebraMap R B h))
include hE hu
omit hE in
Lean source · statement
theorem Φ_mem (x : Kmat G B) : Φ G B q x ∈ ((J G q).map (algebraMap R B)).annihilator
theorem

Φ_surjective

L390 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.Φ_surjective
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Pairing
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (B : Type u) [CommRing B] [Algebra R B]
variable (q : ι0 G → R) (h : R)
variable {q h}
variable (hE : ∀ v : ι0 G → R, ∃ r : R, h • v - r • q ∈ W G) (hu : IsUnit (algebraMap R B h))
include hE hu
Lean source · statement
theorem Φ_surjective (b : B) (hb : b ∈ ((J G q).map (algebraMap R B)).annihilator) :
    ∃ x : Kmat G B, Φ G B q x = b
def

KmatEquivAnn

L454 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.KmatEquivAnn
Documentation

Identify the matrix kernel with the annihilator of the extended ideal.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Pairing
open Matrix
variable (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
variable (B : Type u) [CommRing B] [Algebra R B]
variable (q : ι0 G → R) (h : R)
variable {q h}
variable (hE : ∀ v : ι0 G → R, ∃ r : R, h • v - r • q ∈ W G) (hu : IsUnit (algebraMap R B h))
include hE hu
Lean source · statement
def KmatEquivAnn : Kmat G B ≃ₗ[B] ((J G q).map (algebraMap R B)).annihilator
theorem

main

L465 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator.P2mTwoTermH0Ann.main
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
universe u
open TensorProduct
noncomputable section
namespace P2mTwoTermH0Ann
variable {R : Type u} [CommRing R]
section Main
Lean source · statement
theorem main (G : CoherentBaseChange.TwoTermComplex.{u, u} R) (𝔭 : PrimeSpectrum R) (h𝔭 :
  G.fibreH0 𝔭 ≤ 1) :
    ∃ (h : R) (J : Ideal R), h ∉ 𝔭.asIdeal ∧
      ∀ (B : Type u) [CommRing B] [Algebra R B], IsUnit (algebraMap R B h) →
        Nonempty (G.H0 B ≃ₗ[B] (J.map (algebraMap R B)).annihilator)
theorem

exists_nonempty_H0_linearEquiv_annihilator_of_fibreH0_le_one

L492 ↗
CoherentBaseChange.TwoTermComplex.exists_nonempty_H0_linearEquiv_annihilator_of_fibreH0_le_one
Source context 6 commands

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

section ProofImplementation
section PublicStatement
universe u
open _root_.TensorProduct
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs.TwoTermH0Annihilator
namespace CoherentBaseChange.TwoTermComplex
Lean source · statement
theorem exists_nonempty_H0_linearEquiv_annihilator_of_fibreH0_le_one
    {R : Type u} [CommRing R] (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
    (𝔭 : PrimeSpectrum R) (h𝔭 : G.fibreH0 𝔭 ≤ 1) :
    ∃ (h : R) (J : Ideal R), h ∉ 𝔭.asIdeal ∧
      ∀ (B : Type u) [CommRing B] [Algebra R B], IsUnit (algebraMap R B h) →
        Nonempty (G.H0 B ≃ₗ[B] (J.map (algebraMap R B)).annihilator)

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