NYLL
Module

TwoChartCech_toNat_add_toNat_le_finrank_H0_gluedLinesSections_add.lean

Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_toNat_add_toNat_le_finrank_H0_gluedLinesSections_add
32 declarations indexed from sourceView source ↗

Module documentation

Two Chart Cech to Nat add to Nat le finrank H0 glued Lines Sections add

Imports15
Imported by1

Declarations

theorem

support_mul_T

L48 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.support_mul_T
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
namespace GLH0Neg
variable {k : Type u} [Field k]
Lean source · statement
theorem support_mul_T (f : k[T;T⁻¹]) (e : ℤ) :
    (f * T e).coeff.support = f.coeff.support.map (addRightEmbedding e)
theorem

le_of_mul_T_mem_invPolyPart

L54 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.le_of_mul_T_mem_invPolyPart
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
namespace GLH0Neg
variable {k : Type u} [Field k]
Lean source · statement
theorem le_of_mul_T_mem_invPolyPart {f : k[T;T⁻¹]} {m : ℤ} (h : f * T (-m) ∈ invPolyPart k) :
    ∀ d ∈ f.coeff.support, d ≤ m
theorem

eq_zero_of_neg

L62 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.eq_zero_of_neg
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
namespace GLH0Neg
variable {k : Type u} [Field k]
Lean source · statement
theorem eq_zero_of_neg {f : k[T;T⁻¹]} {m : ℤ} (hm : m < 0) (h0 : f ∈ polyPart k)
    (h1 : f * T (-m) ∈ invPolyPart k) : f = 0
theorem

exists_eq_toLaurent

L71 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.exists_eq_toLaurent
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
namespace GLH0Neg
variable {k : Type u} [Field k]
Lean source · statement
theorem exists_eq_toLaurent {f : k[T;T⁻¹]} {N : ℕ} (h : ∀ d ∈ f.coeff.support, 0 ≤ d ∧ d < N) :
    ∃ p : k[X], p ∈ degreeLT k N ∧ toLaurent p = f
theorem

toLaurent_support_bound

L88 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.toLaurent_support_bound
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
namespace GLH0Neg
variable {k : Type u} [Field k]
Lean source · statement
theorem toLaurent_support_bound {p : k[X]} {N : ℕ} (hp : p ∈ degreeLT k N) :
    ∀ d ∈ (toLaurent p).coeff.support, 0 ≤ d ∧ d < N
def

evalAt

L104 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.evalAt
Documentation

Evaluate a polynomial of bounded degree at the chosen units.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
namespace GLH0Neg
variable {k : Type u} [Field k]
Lean source · full declaration
def evalAt {s : ℕ} (a : Fin s → kˣ) (N : ℕ) : ↥(degreeLT k N) →ₗ[k] (Fin s → k) where
  toFun p := fun i => (p.1).eval (a i : k)
  map_add' p q := by ext i; simp
  map_smul' c p := by ext i; simp
theorem

evalAt_surjective

L109 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.evalAt_surjective
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
namespace GLH0Neg
variable {k : Type u} [Field k]
Lean source · statement
theorem evalAt_surjective {s : ℕ} (a : Fin s → kˣ) (ha : Function.Injective a) (N : ℕ) (hN : s ≤ N)
  :
    Function.Surjective (evalAt a N)
theorem

finrank_ker_evalAt

L124 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.finrank_ker_evalAt
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
namespace GLH0Neg
variable {k : Type u} [Field k]
Lean source · statement
theorem finrank_ker_evalAt {s : ℕ} (a : Fin s → kˣ) (ha : Function.Injective a) (N : ℕ) (hN : s ≤
  N) :
    Module.finrank k (LinearMap.ker (evalAt a N)) = N - s
def

fstL

L141 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.fstL
Documentation

The first Laurent-polynomial component of a global section.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
namespace GLH0Neg
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ) (n m : ℤ)
Lean source · statement
def fstL (x : ↥(gluedLinesSections k a b lam n m).H0) : k[T;T⁻¹]
def

sndL

L145 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.sndL
Documentation

The second Laurent-polynomial component of a global section.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
namespace GLH0Neg
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ) (n m : ℤ)
Lean source · statement
def sndL (x : ↥(gluedLinesSections k a b lam n m).H0) : k[T;T⁻¹]
theorem

fstL_add

L148 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.fstL_add
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
namespace GLH0Neg
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ) (n m : ℤ)
Lean source · statement
theorem fstL_add (x y : ↥(gluedLinesSections k a b lam n m).H0) : fstL a b lam n m (x + y) = fstL a
  b lam n m x + fstL a b lam n m y
theorem

sndL_add

L150 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.sndL_add
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
namespace GLH0Neg
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ) (n m : ℤ)
Lean source · statement
theorem sndL_add (x y : ↥(gluedLinesSections k a b lam n m).H0) : sndL a b lam n m (x + y) = sndL a
  b lam n m x + sndL a b lam n m y
theorem

fstL_smul

L152 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.fstL_smul
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
namespace GLH0Neg
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ) (n m : ℤ)
Lean source · statement
theorem fstL_smul (c : k) (x : ↥(gluedLinesSections k a b lam n m).H0) : fstL a b lam n m (c • x) =
  c • fstL a b lam n m x
theorem

sndL_smul

L154 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.sndL_smul
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
namespace GLH0Neg
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ) (n m : ℤ)
Lean source · statement
theorem sndL_smul (c : k) (x : ↥(gluedLinesSections k a b lam n m).H0) : sndL a b lam n m (c • x) =
  c • sndL a b lam n m x
theorem

val_M1_eq

L157 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.val_M1_eq
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
namespace GLH0Neg
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ) (n m : ℤ)
Lean source · statement
theorem val_M1_eq (x : ↥(gluedLinesSections k a b lam n m).H0) :
    ((x.1).2 : ↥(gluedLinesM1 k a b lam n m)).1 = ((x.1).1 : ↥(gluedLinesM0 k a b lam)).1
theorem

fst_mem_polyPart

L162 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.fst_mem_polyPart
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
namespace GLH0Neg
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ) (n m : ℤ)
Lean source · statement
theorem fst_mem_polyPart (x : ↥(gluedLinesSections k a b lam n m).H0) : fstL a b lam n m x ∈
  polyPart k
theorem

snd_mem_polyPart

L165 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.snd_mem_polyPart
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
namespace GLH0Neg
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ) (n m : ℤ)
Lean source · statement
theorem snd_mem_polyPart (x : ↥(gluedLinesSections k a b lam n m).H0) : sndL a b lam n m x ∈
  polyPart k
theorem

fst_mul_T_mem

L168 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.fst_mul_T_mem
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
namespace GLH0Neg
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ) (n m : ℤ)
Lean source · statement
theorem fst_mul_T_mem (x : ↥(gluedLinesSections k a b lam n m).H0) : fstL a b lam n m x * T (-n) ∈
  invPolyPart k
theorem

snd_mul_T_mem

L173 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.snd_mul_T_mem
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
namespace GLH0Neg
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ) (n m : ℤ)
Lean source · statement
theorem snd_mul_T_mem (x : ↥(gluedLinesSections k a b lam n m).H0) : sndL a b lam n m x * T (-m) ∈
  invPolyPart k
theorem

gluedCond

L178 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.gluedCond
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
namespace GLH0Neg
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ) (n m : ℤ)
Lean source · statement
theorem gluedCond (x : ↥(gluedLinesSections k a b lam n m).H0) :
    GluedCond a b lam (fstL a b lam n m x, sndL a b lam n m x)
theorem

fst_support

L181 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.fst_support
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
namespace GLH0Neg
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ) (n m : ℤ)
Lean source · statement
theorem fst_support (x : ↥(gluedLinesSections k a b lam n m).H0) :
    ∀ d ∈ (fstL a b lam n m x).coeff.support, 0 ≤ d ∧ d < n + 1
theorem

ext_of_fst_snd

L186 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.ext_of_fst_snd
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
namespace GLH0Neg
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ) (n m : ℤ)
Lean source · statement
theorem ext_of_fst_snd {x y : ↥(gluedLinesSections k a b lam n m).H0}
    (h1 : fstL a b lam n m x = fstL a b lam n m y) (h2 : sndL a b lam n m x = sndL a b lam n m y) :
      x = y
def

mkH0

L198 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.mkH0
Documentation

Construct a global section from a pair satisfying the gluing and degree conditions.

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
namespace GLH0Neg
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ) (n m : ℤ)
Lean source · statement
def mkH0 (f : k[T;T⁻¹] × k[T;T⁻¹]) (hc : GluedCond a b lam f) (hp : f ∈ (polyPart k).prod (polyPart
  k))
    (h1 : f.1 * T (-n) ∈ invPolyPart k) (h2 : f.2 * T (-m) ∈ invPolyPart k) :
    ↥(gluedLinesSections k a b lam n m).H0
theorem

fstL_mkH0

L204 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.fstL_mkH0
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
namespace GLH0Neg
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ) (n m : ℤ)
Lean source · statement
theorem fstL_mkH0 (f : k[T;T⁻¹] × k[T;T⁻¹]) (hc hp h1 h2) : fstL a b lam n m (mkH0 a
  b lam n m f hc hp h1 h2) = f.1
theorem

sndL_mkH0

L206 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.sndL_mkH0
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
namespace GLH0Neg
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ) (n m : ℤ)
Lean source · statement
theorem sndL_mkH0 (f : k[T;T⁻¹] × k[T;T⁻¹]) (hc hp h1 h2) : sndL a b lam n m (mkH0 a
  b lam n m f hc hp h1 h2) = f.2
theorem

toLaurent_conds

L209 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.toLaurent_conds
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
namespace GLH0Neg
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ) (n m : ℤ)
Lean source · statement
theorem toLaurent_conds {p : k[X]} {N : ℕ} (hp : p ∈ degreeLT k N) (hN : ∀ d : ℕ, d < N → (d : ℤ) ≤
  n) :
    toLaurent p ∈ polyPart k ∧ toLaurent p * T (-n) ∈ invPolyPart k
theorem

levalUnit_toLaurent

L223 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.levalUnit_toLaurent
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
namespace GLH0Neg
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ) (n m : ℤ)
Lean source · statement
theorem levalUnit_toLaurent (u : kˣ) (p : k[X]) : levalUnit k u (toLaurent p) = p.eval (u : k)
theorem

finrank_H0_of_neg

L227 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.finrank_H0_of_neg
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
namespace GLH0Neg
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ) (n m : ℤ)
Lean source · statement
theorem finrank_H0_of_neg (ha : Function.Injective a) (hn : (s : ℤ) - 1 ≤ n) (hm : m < 0) :
    Module.finrank k ↥(gluedLinesSections k a b lam n m).H0 = (n + 1 - s).toNat
theorem

finrank_H0_gluedLinesSections_of_sub_one_le_of_neg

L292 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.TwoChartCech.finrank_H0_gluedLinesSections_of_sub_one_le_of_neg
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
attribute [local simp]
  GLH0Neg.fstL_mkH0
attribute [local simp]
  GLH0Neg.sndL_mkH0
open scoped _root_.TwoChartCech in
Lean source · statement
theorem TwoChartCech.finrank_H0_gluedLinesSections_of_sub_one_le_of_neg
    (k : Type u) [Field k] {s : ℕ} (a b lam : Fin s → kˣ) (ha : Function.Injective a) (n m : ℤ)
    (hn : (s : ℤ) - 1 ≤ n) (hm : m < 0) :
    Module.finrank k ↥(gluedLinesSections k a b lam n m).H0 = (n + 1 - s).toNat
def

nodeDiff

L303 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.nodeDiff
Documentation

The differences of the two polynomial values at the nodes, weighted by the gluing units.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
attribute [local simp]
  GLH0Neg.fstL_mkH0
attribute [local simp]
  GLH0Neg.sndL_mkH0
namespace GLH0Neg
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ) (n m : ℤ)
Lean source · full declaration
def nodeDiff (N M : ℕ) : (↥(degreeLT k N) × ↥(degreeLT k M)) →ₗ[k] (Fin s → k) where
  toFun pq := fun i => (pq.1.1).eval (a i : k) - (lam i : k) * (pq.2.1).eval (b i : k)
  map_add' p q := by ext i; simp; ring
  map_smul' c p := by ext i; simp; ring
theorem

finrank_H0_ge

L308 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0.GLH0Neg.finrank_H0_ge
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
attribute [local simp]
  GLH0Neg.fstL_mkH0
attribute [local simp]
  GLH0Neg.sndL_mkH0
namespace GLH0Neg
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ) (n m : ℤ)
Lean source · statement
theorem finrank_H0_ge (ha : Function.Injective a) (N M : ℕ) (hN : ∀ d : ℕ, d < N → (d : ℤ) ≤ n) (hM
  : ∀ d : ℕ, d < M → (d : ℤ) ≤ m) :
    N + M ≤ Module.finrank k ↥(gluedLinesSections k a b lam n m).H0 + s
theorem

toNat_add_toNat_le_finrank_H0_gluedLinesSections_add

L372 ↗
TwoChartCech.toNat_add_toNat_le_finrank_H0_gluedLinesSections_add
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartToNatAddToNatLeFinrankH0
open _root_.LaurentPolynomial
open _root_.TwoChartCech
open _root_.Polynomial
universe u
attribute [local simp]
  GLH0Neg.fstL_mkH0
attribute [local simp]
  GLH0Neg.sndL_mkH0
attribute [local simp]
  GLH0Neg.fstL_mkH0
attribute [local simp]
  GLH0Neg.sndL_mkH0
Lean source · statement
theorem _root_.TwoChartCech.toNat_add_toNat_le_finrank_H0_gluedLinesSections_add
    (k : Type u) [Field k] {s : ℕ} (a b lam : Fin s → kˣ) (ha : Function.Injective a) (n m : ℤ) :
    (n + 1).toNat + (m + 1).toNat ≤ Module.finrank k ↥(gluedLinesSections k a b lam n m).H0 + s

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