NYLL
Module

TwoChartCech_finrank_H0_gluedLinesSections_of_sub_one_le_of_neg.lean

Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_finrank_H0_gluedLinesSections_of_sub_one_le_of_neg
29 declarations indexed from sourceView source ↗

Module documentation

Two Chart Cech finrank H0 glued Lines Sections of sub one le of neg

Imports14
  • Mathlib.Algebra.Algebra.Subalgebra.Prod
  • Mathlib.Algebra.MonoidAlgebra.Support
  • Mathlib.Algebra.Module.Submodule.Ker
  • Mathlib.Algebra.Polynomial.Degree.Operations
  • Mathlib.Algebra.Polynomial.Laurent
  • Mathlib.Data.Finsupp.Defs
  • Mathlib.LinearAlgebra.Dimension.Constructions
  • Mathlib.LinearAlgebra.Dimension.Finrank
  • Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
  • Mathlib.LinearAlgebra.Lagrange
  • Mathlib.RingTheory.Polynomial.Basic
  • Mathlib.RingTheory.Polynomial.DegreeLT
  • Mathlib.Tactic.Push
  • Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_GluedLines
Imported by1

Declarations

theorem

support_mul_T

L43 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist.GLH0Neg.support_mul_T
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech 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

L49 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist.GLH0Neg.le_of_mul_T_mem_invPolyPart
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech 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

L57 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist.GLH0Neg.eq_zero_of_neg
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech 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

L65 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist.GLH0Neg.exists_eq_toLaurent
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech 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

L82 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist.GLH0Neg.toLaurent_support_bound
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech 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

L98 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist.GLH0Neg.evalAt
Documentation

Evaluate a polynomial of bounded degree at the chosen units.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech 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

L103 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist.GLH0Neg.evalAt_surjective
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech 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

L118 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist.GLH0Neg.finrank_ker_evalAt
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech 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

L135 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist.GLH0Neg.fstL
Documentation

The first Laurent-polynomial component of a global section.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech 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

L139 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist.GLH0Neg.sndL
Documentation

The second Laurent-polynomial component of a global section.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech 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

L142 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist.GLH0Neg.fstL_add
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech 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

L144 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist.GLH0Neg.sndL_add
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech 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

L146 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist.GLH0Neg.fstL_smul
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech 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

L148 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist.GLH0Neg.sndL_smul
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech 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

L151 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist.GLH0Neg.val_M1_eq
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech 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

L156 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist.GLH0Neg.fst_mem_polyPart
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech 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

L159 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist.GLH0Neg.snd_mem_polyPart
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech 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

L162 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist.GLH0Neg.fst_mul_T_mem
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech 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

L167 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist.GLH0Neg.snd_mul_T_mem
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech 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

L172 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist.GLH0Neg.gluedCond
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech 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

L175 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist.GLH0Neg.fst_support
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech 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

L180 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist.GLH0Neg.ext_of_fst_snd
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech 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

L192 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist.GLH0Neg.mkH0
Documentation

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

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech 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

L198 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist.GLH0Neg.fstL_mkH0
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech 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

L200 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist.GLH0Neg.sndL_mkH0
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech 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

L203 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist.GLH0Neg.toLaurent_conds
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech 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 : (N : ℤ) ≤ n + 1) :
    toLaurent p ∈ polyPart k ∧ toLaurent p * T (-n) ∈ invPolyPart k
theorem

levalUnit_toLaurent

L214 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist.GLH0Neg.levalUnit_toLaurent
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech 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

L218 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist.GLH0Neg.finrank_H0_of_neg
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech 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

L276 ↗
TwoChartCech.finrank_H0_gluedLinesSections_of_sub_one_le_of_neg
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0NegativeTwist
open LaurentPolynomial TwoChartCech Polynomial
universe u
attribute [local simp]
  GLH0Neg.fstL_mkH0
attribute [local simp]
  GLH0Neg.sndL_mkH0
Lean source · statement
theorem _root_.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

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