NYLL
Module

TwoChartCech_finrank_H0_gluedLinesSections_zero_zero_le_one.lean

Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_finrank_H0_gluedLinesSections_zero_zero_le_one
8 declarations indexed from sourceView source ↗

Module documentation

Two Chart Cech finrank H0 glued Lines Sections zero zero le one

Imports7
Imported by1

Declarations

theorem

eq_C_of_mem_polyPart_of_mem_invPolyPart

L47 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0ZeroTwist.TwoChartCech.GluedLinesN3c.eq_C_of_mem_polyPart_of_mem_invPolyPart
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0ZeroTwist
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesN3c
variable {k : Type u} [Field k] {s : ℕ}
Lean source · statement
theorem eq_C_of_mem_polyPart_of_mem_invPolyPart {f : k[T;T⁻¹]} (h0 : f ∈ polyPart k) (h1 : f ∈
  invPolyPart k) :
    f = LaurentPolynomial.C (f.coeff 0)
theorem

eval_C

L60 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0ZeroTwist.TwoChartCech.GluedLinesN3c.eval_C
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0ZeroTwist
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesN3c
variable {k : Type u} [Field k] {s : ℕ}
Lean source · statement
theorem eval_C (u : kˣ) (c : k) : levalUnit k u (LaurentPolynomial.C c) = c
theorem

C_mem_polyPart

L63 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0ZeroTwist.TwoChartCech.GluedLinesN3c.C_mem_polyPart
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0ZeroTwist
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesN3c
variable {k : Type u} [Field k] {s : ℕ}
Lean source · statement
theorem C_mem_polyPart (c : k) : (LaurentPolynomial.C c : k[T;T⁻¹]) ∈ polyPart k
theorem

C_mem_invPolyPart

L68 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0ZeroTwist.TwoChartCech.GluedLinesN3c.C_mem_invPolyPart
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0ZeroTwist
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesN3c
variable {k : Type u} [Field k] {s : ℕ}
Lean source · statement
theorem C_mem_invPolyPart (c : k) : (LaurentPolynomial.C c : k[T;T⁻¹]) ∈ invPolyPart k
theorem

H0_zero_zero_eq

L75 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0ZeroTwist.TwoChartCech.GluedLinesN3c.H0_zero_zero_eq
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0ZeroTwist
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesN3c
variable {k : Type u} [Field k] {s : ℕ}
variable (a b lam : Fin s → kˣ)
Lean source · statement
theorem H0_zero_zero_eq (x : ↥(gluedLinesSections k a b lam 0 0).H0) :
    (x.1.1.1 =
        (LaurentPolynomial.C (x.1.1.1.1.coeff 0),
          LaurentPolynomial.C (x.1.1.1.2.coeff 0))) ∧
      (x.1.2.1 = x.1.1.1) ∧
      (∀ i, x.1.1.1.1.coeff 0 = lam i * x.1.1.1.2.coeff 0)
def

coeffSnd

L96 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0ZeroTwist.TwoChartCech.GluedLinesN3c.coeffSnd
Documentation

The constant coefficient of the second component of a global section.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0ZeroTwist
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesN3c
variable {k : Type u} [Field k] {s : ℕ}
variable (a b lam : Fin s → kˣ)
Lean source · full declaration
def coeffSnd : ↥(gluedLinesSections k a b lam 0 0).H0 →ₗ[k] k where
  toFun x := x.1.1.1.2.coeff 0
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
theorem

coeffSnd_injective

L101 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0ZeroTwist.TwoChartCech.GluedLinesN3c.coeffSnd_injective
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0ZeroTwist
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesN3c
variable {k : Type u} [Field k] {s : ℕ}
variable (a b lam : Fin s → kˣ)
Lean source · statement
theorem coeffSnd_injective (hs : 0 < s) : Function.Injective (coeffSnd a b lam)
theorem

finrank_H0_gluedLinesSections_zero_zero_le_one

L117 ↗
TwoChartCech.finrank_H0_gluedLinesSections_zero_zero_le_one
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0ZeroTwist
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
open TwoChartCech.GluedLinesN3c in
Lean source · statement
theorem _root_.TwoChartCech.finrank_H0_gluedLinesSections_zero_zero_le_one
    (k : Type u) [Field k] {s : ℕ} (hs : 0 < s) (a b lam : Fin s → kˣ) :
    Module.finrank k ↥(gluedLinesSections k a b lam 0 0).H0 ≤ 1 ∧
      (Module.finrank k ↥(gluedLinesSections k a b lam 0 0).H0 = 1 ↔ ∀ i j, lam i = lam j)

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