Module

TwoChartCech_Sections_finite_H0_of_chartFinite.lean

Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_Sections_finite_H0_of_chartFinite

43 declarations indexed from sourceView source ↗

Module documentation

Finiteness of matching sections from finite chart modules and localization on the overlap. A projective-line presentation and its kernel section system supply the comparison.

Imports7

Nyll.SchemeTheory.Cohomology.Cech.TwoChartCech
Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_Sections_finite_H1_of_chartFinite
Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_kerMap_injective_of_H0_eq_zero
Mathlib.Algebra.Polynomial.Laurent
Mathlib.RingTheory.Adjoin.Basic
Mathlib.RingTheory.Finiteness.Defs
Mathlib.RingTheory.Noetherian.Basic

Imported by3

def

P1Cover

L42 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.P1Cover

Documentation

The standard polynomial and Laurent-polynomial two-chart cover of the projective line.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable (R : Type u) [CommRing R]

Lean source · full declaration

def P1Cover : TwoChartCech.Cover.{u, u} R where
  A0 := R[X]
  A1 := R[X]
  A01 := R[T;T⁻¹]
  ρ0 := Polynomial.toLaurentAlg
  ρ1 := (LaurentPolynomial.invert (R := R)).toAlgHom.comp Polynomial.toLaurentAlg

theorem

P1Cover_ρ0_apply

L49 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.P1Cover_ρ0_apply

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable (R : Type u) [CommRing R]

Lean source · statement

theorem P1Cover_ρ0_apply (p : R[X]) : (P1Cover R).ρ0 p = Polynomial.toLaurent p

theorem

P1Cover_ρ1_apply

L50 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.P1Cover_ρ1_apply

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable (R : Type u) [CommRing R]

Lean source · statement

theorem P1Cover_ρ1_apply (p : R[X]) :
    (P1Cover R).ρ1 p = LaurentPolynomial.invert (Polynomial.toLaurent p)

def

twistSections

L54 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.twistSections

Documentation

The section system of a finite free twist on the standard projective-line cover.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable (R : Type u) [CommRing R]

Lean source · full declaration

def twistSections (m a : ℕ) : TwoChartCech.Sections.{u, u, u} (P1Cover
  R) where
  M0 := Fin m → R[X]
  M1 := Fin m → R[X]
  M01 := Fin m → R[T;T⁻¹]
  r0 :=
    { toFun := fun v i => Polynomial.toLaurent (v i)
      map_add' := fun v w => funext fun i => map_add _ _ _
      map_smul' := fun r v => funext fun i => by
        simp only [Pi.smul_apply, RingHom.id_apply]
        exact map_smul (Polynomial.toLaurentAlg (R := R)) r (v i) }
  r1 :=
    { toFun := fun v i => T (-(a : ℤ)) * LaurentPolynomial.invert (Polynomial.toLaurent (v i))
      map_add' := fun v w => funext fun i => by
        simp only [Pi.add_apply, map_add, mul_add]
      map_smul' := fun r v => funext fun i => by
        simp only [Pi.smul_apply, RingHom.id_apply]
        have h1 : Polynomial.toLaurent (r • v i) = r • Polynomial.toLaurent (v i) :=
          map_smul (Polynomial.toLaurentAlg (R := R)) r (v i)
        rw [h1, map_smul, mul_smul_comm] }
  r0_smul p v := funext fun i => by
    change Polynomial.toLaurent ((p • v) i) = Polynomial.toLaurent p * Polynomial.toLaurent (v i)
    simp only [Pi.smul_apply, smul_eq_mul, map_mul]
  r1_smul p v := funext fun i => by
    change T (-(a : ℤ)) * LaurentPolynomial.invert (Polynomial.toLaurent ((p • v) i))
      = LaurentPolynomial.invert (Polynomial.toLaurent p)
          * (T (-(a : ℤ)) * LaurentPolynomial.invert (Polynomial.toLaurent (v i)))
    simp only [Pi.smul_apply, smul_eq_mul, map_mul]
    ring

theorem

twistSections_r0_apply

L94 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.twistSections_r0_apply

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R]

Lean source · statement

theorem twistSections_r0_apply (m a : ℕ) (v : Fin m → R[X]) (i : Fin m) :
    ((twistSections R m a).r0 v : Fin m → R[T;T⁻¹]) i = Polynomial.toLaurent (v i)

theorem

twistSections_r1_apply

L97 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.twistSections_r1_apply

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R]

Lean source · statement

theorem twistSections_r1_apply (m a : ℕ) (v : Fin m → R[X]) (i : Fin m) :
    ((twistSections R m a).r1 v : Fin m → R[T;T⁻¹]) i
      = T (-(a : ℤ)) * LaurentPolynomial.invert (Polynomial.toLaurent (v i))

theorem

twistSections_cechDiff_apply

L101 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.twistSections_cechDiff_apply

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R]

Lean source · statement

theorem twistSections_cechDiff_apply (m a : ℕ) (p : (Fin m → R[X]) × (Fin m → R[X])) (i : Fin m) :
    ((twistSections R m a).cechDiff p : Fin m → R[T;T⁻¹]) i
      = T (-(a : ℤ)) * LaurentPolynomial.invert (Polynomial.toLaurent (p.2 i))
        - Polynomial.toLaurent (p.1 i)

theorem

toLaurent_apply_natCast

L107 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.toLaurent_apply_natCast

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R]

Lean source · statement

theorem toLaurent_apply_natCast (p : R[X]) (k : ℕ) :
    (Polynomial.toLaurent p : R[T;T⁻¹]).coeff (k : ℤ) = p.coeff k

theorem

toLaurent_apply_of_neg

L112 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.toLaurent_apply_of_neg

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R]

Lean source · statement

theorem toLaurent_apply_of_neg (p : R[X]) {n : ℤ} (hn : n < 0) :
    (Polynomial.toLaurent p : R[T;T⁻¹]).coeff n = 0

theorem

T_mul_apply

L119 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.T_mul_apply

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R]

Lean source · statement

theorem T_mul_apply (n : ℤ) (f : R[T;T⁻¹]) (k : ℤ) :
    (T n * f : R[T;T⁻¹]).coeff k = f.coeff (k - n)

theorem

eq_zero_of_toLaurent_eq_T_neg_mul_invert

L127 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.eq_zero_of_toLaurent_eq_T_neg_mul_invert

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R]

Lean source · statement

theorem eq_zero_of_toLaurent_eq_T_neg_mul_invert {a : ℕ} (ha : 1 ≤ a) {p q : R[X]}
    (h : (Polynomial.toLaurent p : R[T;T⁻¹])
      = T (-(a : ℤ)) * LaurentPolynomial.invert (Polynomial.toLaurent q)) : p = 0 ∧ q = 0

theorem

ker_cechDiff_twistSections_eq_bot

L148 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.ker_cechDiff_twistSections_eq_bot

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R]

Lean source · statement

theorem ker_cechDiff_twistSections_eq_bot (m a : ℕ) (ha : 1 ≤ a) :
    LinearMap.ker (twistSections R m a).cechDiff = ⊥

def

evalUnit

L180 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.evalUnit

Documentation

Evaluate a Laurent polynomial at the specified unit.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R]
section evalUnit
variable {A : Type u} [CommRing A] [Algebra R A] (u : A) (hu : IsUnit u)

Lean source · statement

def evalUnit : R[T;T⁻¹] →+* A

theorem

evalUnit_toLaurent

L184 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.evalUnit_toLaurent

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R]
section evalUnit
variable {A : Type u} [CommRing A] [Algebra R A] (u : A) (hu : IsUnit u)

Lean source · statement

theorem evalUnit_toLaurent (p : R[X]) : evalUnit u hu (Polynomial.toLaurent p) = Polynomial.aeval
    u p

theorem

evalUnit_C

L189 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.evalUnit_C

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R]
section evalUnit
variable {A : Type u} [CommRing A] [Algebra R A] (u : A) (hu : IsUnit u)

Lean source · statement

theorem evalUnit_C (r : R) : evalUnit u hu (LaurentPolynomial.C r) = algebraMap R A r

theorem

evalUnit_algebraMap

L192 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.evalUnit_algebraMap

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R]
section evalUnit
variable {A : Type u} [CommRing A] [Algebra R A] (u : A) (hu : IsUnit u)

Lean source · statement

theorem evalUnit_algebraMap (r : R) : evalUnit u hu (algebraMap R R[T;T⁻¹] r) = algebraMap R A r

def

evalUnitAlg

L199 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.evalUnitAlg

Documentation

Laurent-polynomial evaluation at the unit as an algebra homomorphism.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R]
section evalUnit
variable {A : Type u} [CommRing A] [Algebra R A] (u : A) (hu : IsUnit u)

Lean source · statement

def evalUnitAlg : R[T;T⁻¹] →ₐ[R] A

theorem

evalUnitAlg_apply

L202 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.evalUnitAlg_apply

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R]
section evalUnit
variable {A : Type u} [CommRing A] [Algebra R A] (u : A) (hu : IsUnit u)

Lean source · statement

theorem evalUnitAlg_apply (ℓ : R[T;T⁻¹]) : evalUnitAlg u hu ℓ = evalUnit u hu ℓ

theorem

evalUnit_T_one

L204 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.evalUnit_T_one

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R]
section evalUnit
variable {A : Type u} [CommRing A] [Algebra R A] (u : A) (hu : IsUnit u)

Lean source · statement

theorem evalUnit_T_one : evalUnit u hu (T 1 : R[T;T⁻¹]) = u

theorem

evalUnit_T_natCast

L207 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.evalUnit_T_natCast

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R]
section evalUnit
variable {A : Type u} [CommRing A] [Algebra R A] (u : A) (hu : IsUnit u)

Lean source · statement

theorem evalUnit_T_natCast (n : ℕ) : evalUnit u hu (T (n : ℤ) : R[T;T⁻¹]) = u ^ n

theorem

evalUnit_T_neg_one_mul

L210 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.evalUnit_T_neg_one_mul

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R]
section evalUnit
variable {A : Type u} [CommRing A] [Algebra R A] (u : A) (hu : IsUnit u)

Lean source · statement

theorem evalUnit_T_neg_one_mul : evalUnit u hu (T (-1) : R[T;T⁻¹]) * u = 1

theorem

evalUnit_smul

L217 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.evalUnit_smul

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R]
section evalUnit
variable {A : Type u} [CommRing A] [Algebra R A] (u : A) (hu : IsUnit u)

Lean source · statement

theorem evalUnit_smul (r : R) (ℓ : R[T;T⁻¹]) : evalUnit u hu (r • ℓ) = r • evalUnit u hu ℓ

theorem

evalUnit_invert_toLaurent

L220 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.evalUnit_invert_toLaurent

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R]
section evalUnit
variable {A : Type u} [CommRing A] [Algebra R A] (u : A) (hu : IsUnit u)

Lean source · statement

theorem evalUnit_invert_toLaurent {w : A} (hw : u * w = 1) (p : R[X]) :
    evalUnit u hu (LaurentPolynomial.invert (Polynomial.toLaurent p)) = Polynomial.aeval w p

structure

SerreData

L253 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.SerreData

Documentation

A surjective two-chart presentation by a finite free twist, compatible with overlap restriction.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}

Lean source · full declaration

structure SerreData (S : TwoChartCech.Sections.{u, u, u} 𝒰) (f : 𝒰.A0) (g : 𝒰.A1) where
  /-- The number of free generators in the presentation. -/
  m : ℕ
  /-- The positive twist parameter in the presentation. -/
  a : ℕ
  /-- The twist parameter is at least one. -/
  one_le_a : 1 ≤ a
  /-- The image of the first chart coordinate is a unit on the overlap. -/
  hu : IsUnit (𝒰.ρ0 f)
  /-- The presentation map on the first chart. -/
  π0 : (Fin m → R[X]) →ₗ[R] S.M0
  /-- The presentation map on the second chart. -/
  π1 : (Fin m → R[X]) →ₗ[R] S.M1
  /-- The presentation map on the Laurent-polynomial overlap. -/
  π01 : (Fin m → R[T;T⁻¹]) →ₗ[R] S.M01
  /--
  The first presentation map respects polynomial scalar multiplication evaluated at the chart
  coordinate.
  -/
  π0_smul : ∀ (p : R[X]) (v : Fin m → R[X]), π0 (p • v) = Polynomial.aeval f p • π0 v
  /--
  The second presentation map respects polynomial scalar multiplication evaluated at the chart
  coordinate.
  -/
  π1_smul : ∀ (p : R[X]) (v : Fin m → R[X]), π1 (p • v) = Polynomial.aeval g p • π1 v
  /--
  The overlap presentation map respects Laurent-polynomial scalar multiplication evaluated at the
  unit.
  -/
  π01_smul : ∀ (ℓ : R[T;T⁻¹]) (w : Fin m → R[T;T⁻¹]), π01 (ℓ • w) = evalUnit (𝒰.ρ0 f) hu ℓ • π01 w
  /-- The first presentation map commutes with overlap restriction. -/
  comm0 : S.r0 ∘ₗ π0 = π01 ∘ₗ (twistSections R m a).r0
  /-- The second presentation map commutes with overlap restriction. -/
  comm1 : S.r1 ∘ₗ π1 = π01 ∘ₗ (twistSections R m a).r1
  /-- The first chart presentation map is surjective. -/
  surj0 : Function.Surjective π0
  /-- The second chart presentation map is surjective. -/
  surj1 : Function.Surjective π1
  /-- The overlap presentation map is surjective. -/
  surj01 : Function.Surjective π01

def

K0

L299 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.SerreData.K0

Documentation

The polynomial submodule killed by the first chart presentation map.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
namespace SerreData
variable {S : TwoChartCech.Sections.{u, u, u} 𝒰} {f : 𝒰.A0} {g : 𝒰.A1} (D : SerreData S f g)

Lean source · full declaration

def K0 : Submodule R[X] (Fin D.m → R[X]) where
  carrier := {v | D.π0 v = 0}
  add_mem' {v w} hv hw := by
    simp only [Set.mem_ofPred_eq] at hv hw ⊢
    rw [map_add, hv, hw, add_zero]
  zero_mem' := by simp only [Set.mem_ofPred_eq, map_zero]
  smul_mem' p v hv := by
    simp only [Set.mem_ofPred_eq] at hv ⊢
    rw [D.π0_smul, hv, smul_zero]

def

K1

L310 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.SerreData.K1

Documentation

The polynomial submodule killed by the second chart presentation map.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
namespace SerreData
variable {S : TwoChartCech.Sections.{u, u, u} 𝒰} {f : 𝒰.A0} {g : 𝒰.A1} (D : SerreData S f g)

Lean source · full declaration

def K1 : Submodule R[X] (Fin D.m → R[X]) where
  carrier := {v | D.π1 v = 0}
  add_mem' {v w} hv hw := by
    simp only [Set.mem_ofPred_eq] at hv hw ⊢
    rw [map_add, hv, hw, add_zero]
  zero_mem' := by simp only [Set.mem_ofPred_eq, map_zero]
  smul_mem' p v hv := by
    simp only [Set.mem_ofPred_eq] at hv ⊢
    rw [D.π1_smul, hv, smul_zero]

def

K01

L321 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.SerreData.K01

Documentation

The Laurent-polynomial submodule killed by the overlap presentation map.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
namespace SerreData
variable {S : TwoChartCech.Sections.{u, u, u} 𝒰} {f : 𝒰.A0} {g : 𝒰.A1} (D : SerreData S f g)

Lean source · full declaration

def K01 : Submodule R[T;T⁻¹] (Fin D.m → R[T;T⁻¹]) where
  carrier := {w | D.π01 w = 0}
  add_mem' {v w} hv hw := by
    simp only [Set.mem_ofPred_eq] at hv hw ⊢
    rw [map_add, hv, hw, add_zero]
  zero_mem' := by simp only [Set.mem_ofPred_eq, map_zero]
  smul_mem' p v hv := by
    simp only [Set.mem_ofPred_eq] at hv ⊢
    rw [D.π01_smul, hv, smul_zero]

theorem

mem_K0_iff

L331 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.SerreData.mem_K0_iff

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
namespace SerreData
variable {S : TwoChartCech.Sections.{u, u, u} 𝒰} {f : 𝒰.A0} {g : 𝒰.A1} (D : SerreData S f g)

Lean source · statement

theorem mem_K0_iff (v) : v ∈ D.K0 ↔ D.π0 v = 0

theorem

mem_K1_iff

L332 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.SerreData.mem_K1_iff

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
namespace SerreData
variable {S : TwoChartCech.Sections.{u, u, u} 𝒰} {f : 𝒰.A0} {g : 𝒰.A1} (D : SerreData S f g)

Lean source · statement

theorem mem_K1_iff (v) : v ∈ D.K1 ↔ D.π1 v = 0

theorem

mem_K01_iff

L333 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.SerreData.mem_K01_iff

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
namespace SerreData
variable {S : TwoChartCech.Sections.{u, u, u} 𝒰} {f : 𝒰.A0} {g : 𝒰.A1} (D : SerreData S f g)

Lean source · statement

theorem mem_K01_iff (w) : w ∈ D.K01 ↔ D.π01 w = 0

theorem

r0_mem_K01

L335 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.SerreData.r0_mem_K01

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
namespace SerreData
variable {S : TwoChartCech.Sections.{u, u, u} 𝒰} {f : 𝒰.A0} {g : 𝒰.A1} (D : SerreData S f g)

Lean source · statement

theorem r0_mem_K01 {v} (hv : v ∈ D.K0) : (twistSections R D.m D.a).r0 v ∈ D.K01

theorem

r1_mem_K01

L341 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.SerreData.r1_mem_K01

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
namespace SerreData
variable {S : TwoChartCech.Sections.{u, u, u} 𝒰} {f : 𝒰.A0} {g : 𝒰.A1} (D : SerreData S f g)

Lean source · statement

theorem r1_mem_K01 {v} (hv : v ∈ D.K1) : (twistSections R D.m D.a).r1 v ∈ D.K01

def

kerSections

L348 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.SerreData.kerSections

Documentation

The kernel section system of the two-chart presentation.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
namespace SerreData
variable {S : TwoChartCech.Sections.{u, u, u} 𝒰} {f : 𝒰.A0} {g : 𝒰.A1} (D : SerreData S f g)

Lean source · full declaration

def kerSections : TwoChartCech.Sections.{u, u, u} (P1Cover R) where
  M0 := ↥D.K0
  M1 := ↥D.K1
  M01 := ↥D.K01
  r0 :=
    { toFun := fun v => ⟨(twistSections R D.m D.a).r0 (v : Fin D.m → R[X]), D.r0_mem_K01 v.2⟩
      map_add' := fun v w => Subtype.ext (map_add _ _ _)
      map_smul' := fun r v => Subtype.ext (by
        simp only [Submodule.coe_smul_of_tower, RingHom.id_apply]
        exact map_smul _ r (v : Fin D.m → R[X])) }
  r1 :=
    { toFun := fun v => ⟨(twistSections R D.m D.a).r1 (v : Fin D.m → R[X]), D.r1_mem_K01 v.2⟩
      map_add' := fun v w => Subtype.ext (map_add _ _ _)
      map_smul' := fun r v => Subtype.ext (by
        simp only [Submodule.coe_smul_of_tower, RingHom.id_apply]
        exact map_smul _ r (v : Fin D.m → R[X])) }
  r0_smul p v := Subtype.ext ((twistSections R D.m D.a).r0_smul p (v : Fin D.m → R[X]))
  r1_smul p v := Subtype.ext ((twistSections R D.m D.a).r1_smul p (v : Fin D.m → R[X]))

theorem

eq_of_mul_eq_one_of_mul_eq_one

L383 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.eq_of_mul_eq_one_of_mul_eq_one

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
section construction
variable (S : TwoChartCech.Sections.{u, u, u} 𝒰) (f : 𝒰.A0) (g : 𝒰.A1)

Lean source · statement

theorem eq_of_mul_eq_one_of_mul_eq_one {A : Type*} [CommMonoid A] {x y z : A}
    (hx : x * z = 1) (hy : y * z = 1) : x = y

theorem

exists_generators_aeval

L389 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.exists_generators_aeval

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
section construction
variable (S : TwoChartCech.Sections.{u, u, u} 𝒰) (f : 𝒰.A0) (g : 𝒰.A1)

Lean source · statement

theorem exists_generators_aeval {A : Type u} [CommRing A] [Algebra R A] (a : A)
    (M : Type u) [AddCommGroup M] [Module R M] [Module A M] [IsScalarTower R A M]
    (hfin : Module.Finite (Algebra.adjoin R ({a} : Set A)) M) :
    ∃ (p : ℕ) (e : Fin p → M), ∀ x : M, ∃ c : Fin p → R[X], x = ∑ i, Polynomial.aeval a (c i) • e
      i

theorem

exists_serreData

L424 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.exists_serreData

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
section construction
variable (S : TwoChartCech.Sections.{u, u, u} 𝒰) (f : 𝒰.A0) (g : 𝒰.A1)
variable {S f g}

Lean source · statement

theorem exists_serreData (hfg : 𝒰.ρ0 f * 𝒰.ρ1 g = 1)
    (hfin0 : Module.Finite (Algebra.adjoin R ({f} : Set 𝒰.A0)) S.M0)
    (hfin1 : Module.Finite (Algebra.adjoin R ({g} : Set 𝒰.A1)) S.M1)
    (hloc0 : ∀ m : S.M01, ∃ n : ℕ, (𝒰.ρ0 f) ^ n • m ∈ LinearMap.range S.r0)
    (hloc1 : ∀ m : S.M01, ∃ n : ℕ, (𝒰.ρ1 g) ^ n • m ∈ LinearMap.range S.r1) :
    Nonempty (SerreData S f g)

theorem

kerSections_hfin0

L591 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.SerreData.kerSections_hfin0

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
namespace SerreData
variable {S : TwoChartCech.Sections.{u, u, u} 𝒰} {f : 𝒰.A0} {g : 𝒰.A1} (D : SerreData S f g)

Lean source · statement

theorem kerSections_hfin0 [IsNoetherianRing R] :
    Module.Finite (Algebra.adjoin R ({X} : Set (P1Cover R).A0)) D.kerSections.M0

theorem

exists_T_pow_smul_eq

L607 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.SerreData.exists_T_pow_smul_eq

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
namespace SerreData
variable {S : TwoChartCech.Sections.{u, u, u} 𝒰} {f : 𝒰.A0} {g : 𝒰.A1} (D : SerreData S f g)

Lean source · statement

theorem exists_T_pow_smul_eq (m : ℕ) (kv : Fin m → R[T;T⁻¹]) :
    ∃ (N : ℕ) (ev : Fin m → R[X]), ∀ i, T (N : ℤ) * kv i = Polynomial.toLaurent (ev i)

theorem

kerSections_hloc0

L619 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.SerreData.kerSections_hloc0

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
namespace SerreData
variable {S : TwoChartCech.Sections.{u, u, u} 𝒰} {f : 𝒰.A0} {g : 𝒰.A1} (D : SerreData S f g)

Lean source · statement

theorem kerSections_hloc0 (htors0 : ∀ x : S.M0, S.r0 x = 0 → ∃ n : ℕ, f ^ n • x = 0) :
    ∀ k : D.kerSections.M01, ∃ n : ℕ, ((P1Cover R).ρ0 X) ^ n • k ∈ LinearMap.range
      D.kerSections.r0

theorem

kerSections_hloc1

L645 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.SerreData.kerSections_hloc1

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
namespace SerreData
variable {S : TwoChartCech.Sections.{u, u, u} 𝒰} {f : 𝒰.A0} {g : 𝒰.A1} (D : SerreData S f g)

Lean source · statement

theorem kerSections_hloc1
    (htors1 : ∀ y : S.M1, S.r1 y = 0 → ∃ n : ℕ, g ^ n • y = 0) :
    ∀ k : D.kerSections.M01, ∃ n : ℕ, ((P1Cover R).ρ1 X) ^ n • k ∈ LinearMap.range
      D.kerSections.r1

theorem

P1Cover_hfg

L697 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.P1Cover_hfg

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}

Lean source · statement

theorem P1Cover_hfg : (P1Cover R).ρ0 X * (P1Cover R).ρ1 X = 1

theorem

finite_H0

L706 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite.TwoChartCech.SerreH0.SerreData.finite_H0

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u
namespace TwoChartCech
open _root_.TwoChartCech
namespace SerreH0
open _root_.TwoChartCech
open Polynomial LaurentPolynomial
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
namespace SerreData
variable {S : TwoChartCech.Sections.{u, u, u} 𝒰} {f : 𝒰.A0} {g : 𝒰.A1} (D : SerreData S f g)

Lean source · statement

theorem finite_H0 [IsNoetherianRing R] (D : SerreData S f g)
    (htors0 : ∀ x : S.M0, S.r0 x = 0 → ∃ n : ℕ, f ^ n • x = 0)
    (htors1 : ∀ y : S.M1, S.r1 y = 0 → ∃ n : ℕ, g ^ n • y = 0) :
    Module.Finite R S.H0

theorem

finite_H0_of_chartFinite

L758 ↗

TwoChartCech.Sections.finite_H0_of_chartFinite

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H0_of_chartFinite
universe u

Lean source · statement

theorem _root_.TwoChartCech.Sections.finite_H0_of_chartFinite
    {R : Type u} [CommRing R] [IsNoetherianRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
    (S : TwoChartCech.Sections.{u, u, u} 𝒰)
    (f : 𝒰.A0) (g : 𝒰.A1) (hfg : 𝒰.ρ0 f * 𝒰.ρ1 g = 1)
    (hfin0 : Module.Finite (Algebra.adjoin R ({f} : Set 𝒰.A0)) S.M0)
    (hfin1 : Module.Finite (Algebra.adjoin R ({g} : Set 𝒰.A1)) S.M1)
    (hloc0 : ∀ m : S.M01, ∃ n : ℕ, (𝒰.ρ0 f) ^ n • m ∈ LinearMap.range S.r0)
    (hloc1 : ∀ m : S.M01, ∃ n : ℕ, (𝒰.ρ1 g) ^ n • m ∈ LinearMap.range S.r1)
    (htors0 : ∀ x : S.M0, S.r0 x = 0 → ∃ n : ℕ, f ^ n • x = 0)
    (htors1 : ∀ y : S.M1, S.r1 y = 0 → ∃ n : ℕ, g ^ n • y = 0) :
    Module.Finite R S.H0

Module documentation

Declarations