NYLL
Module

TwoChartCech_finrank_H0_gluedLinesSections_eq_one_and_subsingleton_H1.lean

Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_finrank_H0_gluedLinesSections_eq_one_and_subsingleton_H1
23 declarations indexed from sourceView source ↗

Module documentation

Two Chart Cech finrank H0 glued Lines Sections eq one and subsingleton H1

Imports11
  • Mathlib.Algebra.Polynomial.Laurent
  • Mathlib.Algebra.Algebra.Subalgebra.Prod
  • Mathlib.LinearAlgebra.Lagrange
  • Mathlib.LinearAlgebra.Dimension.Finite
  • Mathlib.LinearAlgebra.FiniteDimensional.Defs
  • Mathlib.LinearAlgebra.Quotient.Basic
  • Mathlib.Tactic.Abel
  • Mathlib.Tactic.ByContra
  • Mathlib.Tactic.Ring
  • Mathlib.Tactic.SplitIfs
  • Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_GluedLines
Imported by2

Declarations

theorem

T_eq_single

L52 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero.TwoChartCech.GluedLinesMain.T_eq_single
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
Lean source · statement
theorem T_eq_single (j : ℤ) : (T j : k[T;T⁻¹]) = AddMonoidAlgebra.single j 1
theorem

support_mul_T

L54 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero.TwoChartCech.GluedLinesMain.support_mul_T
Source context 9 commands

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

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

mul_T_mem_invPolyPart_iff

L59 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero.TwoChartCech.GluedLinesMain.mul_T_mem_invPolyPart_iff
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
Lean source · statement
theorem mul_T_mem_invPolyPart_iff (f : k[T;T⁻¹]) (j : ℤ) :
    f * T j ∈ invPolyPart k ↔ ∀ n ∈ f.coeff.support, n + j ≤ 0
theorem

toLaurent_mem_polyPart

L69 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero.TwoChartCech.GluedLinesMain.toLaurent_mem_polyPart
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
Lean source · statement
theorem toLaurent_mem_polyPart (p : Polynomial k) : Polynomial.toLaurent p ∈ polyPart k
theorem

toLaurent_trunc_apply

L75 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero.TwoChartCech.GluedLinesMain.toLaurent_trunc_apply
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
Lean source · full declaration
theorem toLaurent_trunc_apply (f : k[T;T⁻¹]) (n : ℤ) :
    (Polynomial.toLaurent (LaurentPolynomial.trunc f)).coeff n = if 0 ≤ n then f.coeff n else 0 :=
      by
  induction f using LaurentPolynomial.induction_on' with
  | add p q hp hq =>
    rw [map_add, map_add]
    change (Polynomial.toLaurent (LaurentPolynomial.trunc p)).coeff n + (Polynomial.toLaurent
      (LaurentPolynomial.trunc q)).coeff n = _
    rw [hp, hq]
    split_ifs
    · rfl
    · exact add_zero 0
  | C_mul_T m r =>
    rw [LaurentPolynomial.trunc_C_mul_T]
    have hcoef : ∀ j : ℤ, (LaurentPolynomial.C r * T m : k[T;T⁻¹]).coeff j = if m = j then r else 0
      := fun j => by
      rw [← LaurentPolynomial.single_eq_C_mul_T, AddMonoidAlgebra.coeff_single]; exact
        Finsupp.single_apply
    split_ifs with hm hn hn
    · rw [Polynomial.toLaurent_C_mul_T, Int.toNat_of_nonneg hm, hcoef]
    · rw [Polynomial.toLaurent_C_mul_T, Int.toNat_of_nonneg hm, hcoef, ite_eq_right]
      rintro rfl; exact hn hm
    · rw [map_zero, hcoef, ite_eq_right]
      · rfl
      · rintro rfl; exact hm hn
    · rw [map_zero]; rfl
theorem

toLaurent_trunc_of_mem_polyPart

L102 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero.TwoChartCech.GluedLinesMain.toLaurent_trunc_of_mem_polyPart
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
Lean source · statement
theorem toLaurent_trunc_of_mem_polyPart {f : k[T;T⁻¹]} (hf : f ∈ polyPart k) :
    Polynomial.toLaurent (LaurentPolynomial.trunc f) = f
theorem

toLaurent_mul_T_mem_invPolyPart_iff_degree_lt

L113 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero.TwoChartCech.GluedLinesMain.toLaurent_mul_T_mem_invPolyPart_iff_degree_lt
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
Lean source · statement
theorem toLaurent_mul_T_mem_invPolyPart_iff_degree_lt (p : Polynomial k) (d : ℕ) :
    Polynomial.toLaurent p * T (-((d : ℤ) - 1)) ∈ invPolyPart k ↔ p.degree < d
theorem

eval_toLaurent

L131 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero.TwoChartCech.GluedLinesMain.eval_toLaurent
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
Lean source · statement
theorem eval_toLaurent (u : kˣ) (p : Polynomial k) : levalUnit k u (Polynomial.toLaurent p) =
  p.eval (u : k)
theorem

eval_C

L135 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero.TwoChartCech.GluedLinesMain.eval_C
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesMain
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

L138 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero.TwoChartCech.GluedLinesMain.C_mem_polyPart
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesMain
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

L143 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero.TwoChartCech.GluedLinesMain.C_mem_invPolyPart
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesMain
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

eq_C_of_mem_polyPart_of_mem_invPolyPart

L148 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero.TwoChartCech.GluedLinesMain.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.GluedLinesH0OneH1Zero
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesMain
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)
def

lpos

L162 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero.TwoChartCech.GluedLinesMain.lpos
Documentation

The nonnegative-degree part of a Laurent polynomial.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
Lean source · statement
def lpos (f : k[T;T⁻¹]) : k[T;T⁻¹]
def

lneg

L165 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero.TwoChartCech.GluedLinesMain.lneg
Documentation

The negative-degree remainder of a Laurent polynomial.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
Lean source · statement
def lneg (f : k[T;T⁻¹]) : k[T;T⁻¹]
theorem

lpos_add_lneg

L167 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero.TwoChartCech.GluedLinesMain.lpos_add_lneg
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
Lean source · statement
theorem lpos_add_lneg (f : k[T;T⁻¹]) : lpos f + lneg f = f
theorem

lpos_mem_polyPart

L169 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero.TwoChartCech.GluedLinesMain.lpos_mem_polyPart
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
Lean source · statement
theorem lpos_mem_polyPart (f : k[T;T⁻¹]) : lpos f ∈ polyPart k
theorem

lneg_mul_T_mem_invPolyPart

L171 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero.TwoChartCech.GluedLinesMain.lneg_mul_T_mem_invPolyPart
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
Lean source · statement
theorem lneg_mul_T_mem_invPolyPart (f : k[T;T⁻¹]) {j : ℤ} (hj : j ≤ 1) : lneg f * T j ∈ invPolyPart
  k
theorem

injOn_val

L181 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero.TwoChartCech.GluedLinesMain.injOn_val
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
Lean source · full declaration
theorem injOn_val (a : Fin s → kˣ) (ha : Function.Injective a) :
    Set.InjOn (fun i => (a i : k)) ↑(Finset.univ : Finset (Fin s)) :=
  fun _ _ _ _ h => ha (Units.ext h)
def

coeffSnd

L188 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero.TwoChartCech.GluedLinesMain.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.GluedLinesH0OneH1Zero
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
variable (a b lam : Fin s → kˣ)
Lean source · full declaration
def coeffSnd (n m : ℤ) : ↥(gluedLinesSections k a b lam n m).H0 →ₗ[k] k where
  toFun x := x.1.1.1.2.coeff 0
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
theorem

H0_shape

L193 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero.TwoChartCech.GluedLinesMain.H0_shape
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
variable (a b lam : Fin s → kˣ)
Lean source · statement
theorem H0_shape (x : ↥(gluedLinesSections k a b lam ((s : ℤ) - 1) 0).H0) :
    x.1.2.1 = x.1.1.1 ∧
    x.1.1.1.2 = LaurentPolynomial.C (x.1.1.1.2.coeff 0) ∧
    Polynomial.toLaurent (LaurentPolynomial.trunc x.1.1.1.1) = x.1.1.1.1 ∧
    (LaurentPolynomial.trunc x.1.1.1.1).degree < s ∧
    (∀ i, (LaurentPolynomial.trunc x.1.1.1.1).eval (a i : k) = lam i * x.1.1.1.2.coeff 0)
theorem

coeffSnd_bijective

L215 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero.TwoChartCech.GluedLinesMain.coeffSnd_bijective
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
variable (a b lam : Fin s → kˣ)
Lean source · statement
theorem coeffSnd_bijective (ha : Function.Injective a) :
    Function.Bijective (coeffSnd a b lam ((s : ℤ) - 1) 0)
theorem

cechDiff_surjective

L260 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero.TwoChartCech.GluedLinesMain.cechDiff_surjective
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
variable (a b lam : Fin s → kˣ)
Lean source · statement
theorem cechDiff_surjective (ha : Function.Injective a) :
    Function.Surjective (gluedLinesSections k a b lam ((s : ℤ) - 1) 0).cechDiff
theorem

finrank_H0_gluedLinesSections_eq_one_and_subsingleton_H1

L310 ↗
TwoChartCech.finrank_H0_gluedLinesSections_eq_one_and_subsingleton_H1
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.GluedLinesH0OneH1Zero
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u
open TwoChartCech.GluedLinesMain in
Lean source · statement
theorem _root_.TwoChartCech.finrank_H0_gluedLinesSections_eq_one_and_subsingleton_H1
    (k : Type u) [Field k] {s : ℕ} (a b lam : Fin s → kˣ) (ha : Function.Injective a) :
    Module.finrank k ↥(gluedLinesSections k a b lam ((s : ℤ) - 1) 0).H0 = 1 ∧
      Subsingleton (gluedLinesSections k a b lam ((s : ℤ) - 1) 0).H1

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