Module

TwoChartCech_finrank_H0_sub_finrank_H1_gluedLinesSections.lean

Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_finrank_H0_sub_finrank_H1_gluedLinesSections

64 declarations indexed from sourceView source ↗

Module documentation

Two Chart Cech finrank H0 sub finrank H1 glued Lines Sections

Imports17

Mathlib.Algebra.Polynomial.Laurent
Mathlib.Algebra.Algebra.Subalgebra.Prod
Mathlib.LinearAlgebra.Lagrange
Mathlib.LinearAlgebra.FiniteDimensional.Defs
Mathlib.LinearAlgebra.FiniteDimensional.Basic
Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Mathlib.LinearAlgebra.Quotient.Basic
Mathlib.LinearAlgebra.Isomorphisms
Mathlib.RingTheory.Finiteness.Basic
Mathlib.Tactic.Abel
Mathlib.Tactic.ByContra
Mathlib.Tactic.Ext
Mathlib.Tactic.Ring
Mathlib.Tactic.LinearCombination
Mathlib.Tactic.SplitIfs
Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_GluedLines
Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_finrank_H0_gluedLinesSections_eq_one_and_subsingleton_H1

Imported by2

theorem

T_eq_single

L59 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.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.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
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

L61 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.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.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
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

L66 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.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.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
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

L76 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.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.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
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

L82 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.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.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
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]
    simp only [AddMonoidAlgebra.coeff_add, Finsupp.add_apply]
    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

L108 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.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.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
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

L119 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.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.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
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

L137 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.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.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
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

L141 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.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.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
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

L144 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.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.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
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

L149 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.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.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
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

L154 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.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.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
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

L168 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.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.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
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

L171 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.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.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
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

L173 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.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.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
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

L175 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.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.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
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

L177 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.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.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
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

L187 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.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.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
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

L194 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.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.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
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

L199 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.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.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
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

L221 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.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.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
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

L266 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.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.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
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

abbrev

Q

L332 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.ChiStep.Q

Documentation

The quotient of the larger submodule by the intersection with the smaller submodule.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
namespace TwoChartCech
open _root_.TwoChartCech
namespace ChiStep
open Module Submodule
variable {k : Type u} [Field k] {F : Type v} [AddCommGroup F] [Module k F]
variable (A B B' W : Submodule k F)

Lean source · statement

abbrev Q : Type v

def

ψ

L335 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.ChiStep.ψ

Documentation

Include the intersection into the larger submodule and pass to its quotient.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
namespace TwoChartCech
open _root_.TwoChartCech
namespace ChiStep
open Module Submodule
variable {k : Type u} [Field k] {F : Type v} [AddCommGroup F] [Module k F]
variable (A B B' W : Submodule k F)

Lean source · statement

def ψ : ↥(A ⊓ B') →ₗ[k] Q B B'

def

φbar

L338 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.ChiStep.φbar

Documentation

The map on submodule quotients induced by inclusion into the ambient submodule.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
namespace TwoChartCech
open _root_.TwoChartCech
namespace ChiStep
open Module Submodule
variable {k : Type u} [Field k] {F : Type v} [AddCommGroup F] [Module k F]
variable (A B B' W : Submodule k F)

Lean source · statement

def φbar (hB'W : B' ≤ W) : Q B B' →ₗ[k] ↥W ⧸ ((A ⊔ B).comap W.subtype)

def

π

L345 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.ChiStep.π

Documentation

The quotient map induced by enlarging the second submodule.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
namespace TwoChartCech
open _root_.TwoChartCech
namespace ChiStep
open Module Submodule
variable {k : Type u} [Field k] {F : Type v} [AddCommGroup F] [Module k F]
variable (A B B' W : Submodule k F)

Lean source · statement

def π (hBB' : B ≤ B') : (↥W ⧸ ((A ⊔ B).comap W.subtype)) →ₗ[k] ↥W ⧸ ((A ⊔ B').comap W.subtype)

theorem

ker_ψ

L348 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.ChiStep.ker_ψ

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
namespace TwoChartCech
open _root_.TwoChartCech
namespace ChiStep
open Module Submodule
variable {k : Type u} [Field k] {F : Type v} [AddCommGroup F] [Module k F]
variable (A B B' W : Submodule k F)

Lean source · statement

theorem ker_ψ : LinearMap.ker (ψ A B B') = (A ⊓ B).comap (A ⊓ B').subtype

theorem

range_ψ_eq_ker_φbar

L354 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.ChiStep.range_ψ_eq_ker_φbar

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
namespace TwoChartCech
open _root_.TwoChartCech
namespace ChiStep
open Module Submodule
variable {k : Type u} [Field k] {F : Type v} [AddCommGroup F] [Module k F]
variable (A B B' W : Submodule k F)

Lean source · statement

theorem range_ψ_eq_ker_φbar (hBB' : B ≤ B') (hB'W : B' ≤ W) :
    LinearMap.range (ψ A B B') = LinearMap.ker (φbar A B B' W hB'W)

theorem

range_φbar_eq_ker_π

L382 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.ChiStep.range_φbar_eq_ker_π

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
namespace TwoChartCech
open _root_.TwoChartCech
namespace ChiStep
open Module Submodule
variable {k : Type u} [Field k] {F : Type v} [AddCommGroup F] [Module k F]
variable (A B B' W : Submodule k F)

Lean source · statement

theorem range_φbar_eq_ker_π (hBB' : B ≤ B') (hB'W : B' ≤ W) :
    LinearMap.range (φbar A B B' W hB'W) = LinearMap.ker (π A B B' W hBB')

theorem

finite_forward

L410 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.ChiStep.finite_forward

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
namespace TwoChartCech
open _root_.TwoChartCech
namespace ChiStep
open Module Submodule
variable {k : Type u} [Field k] {F : Type v} [AddCommGroup F] [Module k F]
variable (A B B' W : Submodule k F)

Lean source · statement

theorem finite_forward (hBB' : B ≤ B') (hcodim : Module.finrank k (Q B B') = 1)
    [Module.Finite k ↥(A ⊓ B)] [Module.Finite k (↥W ⧸ ((A ⊔ B).comap W.subtype))] :
    Module.Finite k ↥(A ⊓ B') ∧ Module.Finite k (↥W ⧸ ((A ⊔ B').comap W.subtype))

theorem

finite_backward

L423 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.ChiStep.finite_backward

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
namespace TwoChartCech
open _root_.TwoChartCech
namespace ChiStep
open Module Submodule
variable {k : Type u} [Field k] {F : Type v} [AddCommGroup F] [Module k F]
variable (A B B' W : Submodule k F)

Lean source · statement

theorem finite_backward (hBB' : B ≤ B') (hB'W : B' ≤ W) (hcodim : Module.finrank k (Q B B') = 1)
    [Module.Finite k ↥(A ⊓ B')] [Module.Finite k (↥W ⧸ ((A ⊔ B').comap W.subtype))] :
    Module.Finite k ↥(A ⊓ B) ∧ Module.Finite k (↥W ⧸ ((A ⊔ B).comap W.subtype))

theorem

finrank_step

L438 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.ChiStep.finrank_step

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
namespace TwoChartCech
open _root_.TwoChartCech
namespace ChiStep
open Module Submodule
variable {k : Type u} [Field k] {F : Type v} [AddCommGroup F] [Module k F]
variable (A B B' W : Submodule k F)

Lean source · statement

theorem finrank_step (hBB' : B ≤ B') (hB'W : B' ≤ W) (hcodim : Module.finrank k (Q B B') = 1)
    [Module.Finite k ↥(A ⊓ B)] [Module.Finite k (↥W ⧸ ((A ⊔ B).comap W.subtype))]
    [Module.Finite k ↥(A ⊓ B')] [Module.Finite k (↥W ⧸ ((A ⊔ B').comap W.subtype))] :
    (Module.finrank k ↥(A ⊓ B') : ℤ) - Module.finrank k (↥W ⧸ ((A ⊔ B').comap W.subtype)) =
      (Module.finrank k ↥(A ⊓ B) : ℤ) - Module.finrank k (↥W ⧸ ((A ⊔ B).comap W.subtype)) + 1

abbrev

Amb

L484 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.Amb

Documentation

The ambient space of pairs of Laurent polynomials.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ)

Lean source · statement

abbrev Amb (k : Type u) [Field k] : Type u

def

Asub

L487 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.Asub

Documentation

First-chart sections viewed as a subspace of the ambient Laurent-polynomial pairs.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ)

Lean source · statement

def Asub : Submodule k (Amb k)

def

Bsub

L490 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.Bsub

Documentation

Second-chart sections with the specified twists, viewed as a subspace of the ambient pairs.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ)

Lean source · statement

def Bsub (n m : ℤ) : Submodule k (Amb k)

def

Wsub

L493 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.Wsub

Documentation

Overlap sections viewed as a subspace of the ambient pairs.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ)

Lean source · statement

def Wsub : Submodule k (Amb k)

theorem

A_le_W

L495 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.A_le_W

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ)

Lean source · statement

theorem A_le_W : Asub a b lam ≤ Wsub a b lam

theorem

B_le_W

L496 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.B_le_W

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ)

Lean source · statement

theorem B_le_W (n m : ℤ) : Bsub a b lam n m ≤ Wsub a b lam

theorem

mul_T_mem_invPolyPart_mono

L498 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.mul_T_mem_invPolyPart_mono

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ)

Lean source · statement

theorem mul_T_mem_invPolyPart_mono {f : k[T;T⁻¹]} {j j' : ℤ} (hj : j' ≤ j) (h : f * T j ∈
  invPolyPart k) :
    f * T j' ∈ invPolyPart k

theorem

B_mono_fst

L504 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.B_mono_fst

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ)

Lean source · statement

theorem B_mono_fst (n m : ℤ) : Bsub a b lam (n - 1) m ≤ Bsub a b lam n m

theorem

B_mono_snd

L507 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.B_mono_snd

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ)

Lean source · statement

theorem B_mono_snd (n m : ℤ) : Bsub a b lam n (m - 1) ≤ Bsub a b lam n m

def

H0equiv

L511 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.H0equiv

Documentation

Identify global sections with the intersection of the two chart subspaces.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ)

Lean source · full declaration

def H0equiv (n m : ℤ) : ↥(gluedLinesSections k a b lam n m).H0 ≃ₗ[k] ↥(Asub a b lam ⊓ Bsub a b lam
  n m) where
  toFun x := ⟨x.1.1.1, x.1.1.2, by
    have hH := ((gluedLinesSections k a b lam n m).mem_H0_iff x.1).mp x.2
    have heq : x.1.2.1 = x.1.1.1 := (congrArg Subtype.val hH).symm
    rw [← heq]; exact x.1.2.2⟩
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  invFun v := ⟨(⟨v.1, v.2.1⟩, ⟨v.1, v.2.2⟩), ((gluedLinesSections k a b lam n m).mem_H0_iff _).mpr
    rfl⟩
  left_inv x := by
    have hH := ((gluedLinesSections k a b lam n m).mem_H0_iff x.1).mp x.2
    have heq : x.1.2.1 = x.1.1.1 := (congrArg Subtype.val hH).symm
    apply Subtype.ext; apply Prod.ext
    · rfl
    · exact Subtype.ext heq.symm
  right_inv v := rfl

def

M01equiv

L530 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.M01equiv

Documentation

Identify overlap sections with their ambient subspace.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ)

Lean source · full declaration

def M01equiv : (gluedLinesSections k a b lam 0 0).M01 ≃ₗ[k] ↥(Wsub a b lam) where
  toFun w := ⟨w.1, w.2⟩
  map_add' _ _ := rfl
  map_smul' _ _ := rfl
  invFun w := ⟨w.1, w.2⟩
  left_inv _ := rfl
  right_inv _ := rfl

theorem

map_range_cechDiff

L538 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.map_range_cechDiff

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ)

Lean source · statement

theorem map_range_cechDiff (n m : ℤ) :
    (LinearMap.range (gluedLinesSections k a b lam n m).cechDiff).map (M01equiv a b
      lam).toLinearMap =
      (Asub a b lam ⊔ Bsub a b lam n m).comap (Wsub a b lam).subtype

def

H1equiv

L560 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.H1equiv

Documentation

Identify first cohomology with the overlap subspace modulo the chart subspaces.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule
variable {k : Type u} [Field k] {s : ℕ} (a b lam : Fin s → kˣ)

Lean source · statement

def H1equiv (n m : ℤ) :
    (gluedLinesSections k a b lam n m).H1 ≃ₗ[k] ↥(Wsub a b lam) ⧸ (Asub a b lam ⊔ Bsub a b lam n
      m).comap (Wsub a b lam).subtype

theorem

levalUnit_invert

L587 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.levalUnit_invert

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}

Lean source · statement

theorem levalUnit_invert (u : kˣ) (f : k[T;T⁻¹]) :
    levalUnit k u (LaurentPolynomial.invert f) = levalUnit k u⁻¹ f

theorem

mul_T_apply

L598 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.mul_T_apply

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}

Lean source · statement

theorem mul_T_apply (f : k[T;T⁻¹]) (j m : ℤ) : (f * T j : k[T;T⁻¹]).coeff m = f.coeff (m - j)

theorem

T_apply_self

L601 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.T_apply_self

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}

Lean source · statement

theorem T_apply_self (j : ℤ) : (T j : k[T;T⁻¹]).coeff j = 1

theorem

toLaurent_apply_neg

L604 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.toLaurent_apply_neg

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}

Lean source · statement

theorem toLaurent_apply_neg (r : Polynomial k) {j : ℤ} (hj : j < 0) : (Polynomial.toLaurent
  r).coeff j = 0

theorem

exists_laurent_eval_eq

L610 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.exists_laurent_eval_eq

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}

Lean source · statement

theorem exists_laurent_eval_eq (a : Fin s → kˣ) (ha : Function.Injective a) (n : ℤ) (t : Fin s → k)
  :
    ∃ p : k[T;T⁻¹], p * T (-(n - 1)) ∈ invPolyPart k ∧ p.coeff n = 0 ∧ ∀ i, levalUnit k (a i) p = t
      i

def

lead

L643 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.lead

Documentation

The coefficient in degree n of the first component on the second chart.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
variable (a b lam : Fin s → kˣ)

Lean source · full declaration

def lead (n m : ℤ) : ↥(Bsub a b lam n m) →ₗ[k] k where
  toFun v := v.1.1.coeff n
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

theorem

ker_lead

L648 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.ker_lead

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
variable (a b lam : Fin s → kˣ)

Lean source · statement

theorem ker_lead (n m : ℤ) : LinearMap.ker (lead a b lam n m) = (Bsub a b lam (n - 1) m).comap
  (Bsub a b lam n m).subtype

theorem

lead_surjective

L669 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.lead_surjective

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
variable (a b lam : Fin s → kˣ)

Lean source · statement

theorem lead_surjective (ha : Function.Injective a) (n m : ℤ) : Function.Surjective (lead a b lam n
  m)

theorem

codim_fst

L690 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.codim_fst

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
variable (a b lam : Fin s → kˣ)

Lean source · statement

theorem codim_fst (ha : Function.Injective a) (n m : ℤ) :
    Module.finrank k (↥(Bsub a b lam n m) ⧸ (Bsub a b lam (n - 1) m).comap (Bsub a b lam n
      m).subtype) = 1

def

lead₂

L699 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.lead₂

Documentation

The coefficient in degree m of the second component on the second chart.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
variable (a b lam : Fin s → kˣ)

Lean source · full declaration

def lead₂ (n m : ℤ) : ↥(Bsub a b lam n m) →ₗ[k] k where
  toFun v := v.1.2.coeff m
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

theorem

ker_lead₂

L704 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.ker_lead₂

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
variable (a b lam : Fin s → kˣ)

Lean source · statement

theorem ker_lead₂ (n m : ℤ) : LinearMap.ker (lead₂ a b lam n m) = (Bsub a b lam n (m - 1)).comap
  (Bsub a b lam n m).subtype

theorem

lead₂_surjective

L725 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.lead₂_surjective

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
variable (a b lam : Fin s → kˣ)

Lean source · statement

theorem lead₂_surjective (ha : Function.Injective a) (n m : ℤ) : Function.Surjective (lead₂ a b lam
  n m)

theorem

codim_snd

L741 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.codim_snd

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
variable (a b lam : Fin s → kˣ)

Lean source · statement

theorem codim_snd (ha : Function.Injective a) (n m : ℤ) :
    Module.finrank k (↥(Bsub a b lam n m) ⧸ (Bsub a b lam n (m - 1)).comap (Bsub a b lam n
      m).subtype) = 1

def

Claim

L750 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.Claim

Documentation

The finite-dimensionality and Euler-characteristic assertion for the two twists.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
variable (a b lam : Fin s → kˣ)

Lean source · statement

def Claim (n m : ℤ) : Prop

theorem

claim_step_fst

L758 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.claim_step_fst

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
variable (a b lam : Fin s → kˣ)

Lean source · statement

theorem claim_step_fst (ha : Function.Injective a) (n m : ℤ) : Claim a b lam (n - 1) m ↔ Claim a b
  lam n m

theorem

claim_step_snd

L779 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.claim_step_snd

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
variable (a b lam : Fin s → kˣ)

Lean source · statement

theorem claim_step_snd (ha : Function.Injective a) (n m : ℤ) : Claim a b lam n (m - 1) ↔ Claim a b
  lam n m

theorem

claim_base

L800 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.claim_base

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
variable (a b lam : Fin s → kˣ)

Lean source · statement

theorem claim_base
    (hmain : Module.finrank k ↥(gluedLinesSections k a b lam ((s : ℤ) - 1) 0).H0 = 1 ∧
      Subsingleton (gluedLinesSections k a b lam ((s : ℤ) - 1) 0).H1) :
    Claim a b lam ((s : ℤ) - 1) 0

theorem

claim_all

L817 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech.GluedLinesChi.claim_all

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
noncomputable section
namespace TwoChartCech
open _root_.TwoChartCech
namespace GluedLinesChi
open Module Submodule GluedLinesMain
variable {k : Type u} [Field k] {s : ℕ}
variable (a b lam : Fin s → kˣ)

Lean source · statement

theorem claim_all (ha : Function.Injective a)
    (hmain : Module.finrank k ↥(gluedLinesSections k a b lam ((s : ℤ) - 1) 0).H0 = 1 ∧
      Subsingleton (gluedLinesSections k a b lam ((s : ℤ) - 1) 0).H1)
    (n m : ℤ) : Claim a b lam n m

theorem

finrank_H0_sub_finrank_H1_gluedLinesSections

L849 ↗

TwoChartCech.finrank_H0_sub_finrank_H1_gluedLinesSections

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1
open _root_.TwoChartCech
open _root_.LaurentPolynomial
universe u v
open _root_.TwoChartCech
  _root_.AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartFinrankH0SubFinrankH1.TwoChartCech
  TwoChartCech.GluedLinesChi in

Lean source · statement

theorem _root_.TwoChartCech.finrank_H0_sub_finrank_H1_gluedLinesSections
    (k : Type u) [Field k] {s : ℕ} (a b lam : Fin s → kˣ) (ha : Function.Injective a) (n m : ℤ) :
    Module.Finite k ↥(gluedLinesSections k a b lam n m).H0 ∧
      Module.Finite k (gluedLinesSections k a b lam n m).H1 ∧
      (Module.finrank k ↥(gluedLinesSections k a b lam n m).H0 : ℤ)
        - Module.finrank k (gluedLinesSections k a b lam n m).H1 = n + m + 2 - s

Module documentation

Two Chart Cech finrank H0 sub finrank H1 glued Lines Sections

Declarations