NYLL
Module

TwoChartCech_Sections_finite_H1_of_chartFinite.lean

Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_Sections_finite_H1_of_chartFinite
12 declarations indexed from sourceView source ↗

Module documentation

Finiteness of first Cech cohomology from finite sections on a chart. Localization conditions reduce the quotient to finitely many translated generators.

Imports6
Imported by4

Declarations

theorem

vpow_mul_upow

L41 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H1_of_chartFinite.TwoChartCech.ChartFinite.vpow_mul_upow
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H1_of_chartFinite
universe u
open Polynomial
namespace TwoChartCech
open _root_.TwoChartCech
namespace ChartFinite
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
    (S : TwoChartCech.Sections.{u, u, u} 𝒰)
Lean source · full declaration
theorem vpow_mul_upow (f : 𝒰.A0) (g : 𝒰.A1) (hfg : 𝒰.ρ0 f * 𝒰.ρ1 g = 1) (n j : ℕ) :
    𝒰.ρ1 g ^ n * 𝒰.ρ0 f ^ j = if j ≤ n then 𝒰.ρ1 g ^ (n - j) else 𝒰.ρ0 f ^ (j - n) := by
  have hvu : 𝒰.ρ1 g * 𝒰.ρ0 f = 1 := by rw [mul_comm]; exact hfg
  induction n generalizing j with
  | zero => cases j <;> simp
  | succ n ih =>
    cases j with
    | zero => simp
    | succ j =>
      have : 𝒰.ρ1 g ^ (n + 1) * 𝒰.ρ0 f ^ (j + 1) = 𝒰.ρ1 g ^ n * 𝒰.ρ0 f ^ j := by
        rw [pow_succ, pow_succ', mul_assoc, ← mul_assoc (𝒰.ρ1 g) (𝒰.ρ0 f), hvu, one_mul]
      rw [this, ih j]
      simp only [Nat.succ_le_succ_iff, Nat.succ_sub_succ]
def

T

L56 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H1_of_chartFinite.TwoChartCech.ChartFinite.T
Documentation

The finite set of restriction generators multiplied by powers below a fixed bound.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H1_of_chartFinite
universe u
open Polynomial
namespace TwoChartCech
open _root_.TwoChartCech
namespace ChartFinite
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
    (S : TwoChartCech.Sections.{u, u, u} 𝒰)
Lean source · statement
def T (g : 𝒰.A1) (s : Finset S.M0) (N : ℕ) : Finset S.M01
def

W

L60 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H1_of_chartFinite.TwoChartCech.ChartFinite.W
Documentation

The span of the finite translated generators together with Cech boundaries.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H1_of_chartFinite
universe u
open Polynomial
namespace TwoChartCech
open _root_.TwoChartCech
namespace ChartFinite
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
    (S : TwoChartCech.Sections.{u, u, u} 𝒰)
Lean source · statement
def W (g : 𝒰.A1) (s : Finset S.M0) (N : ℕ) : Submodule R S.M01
theorem

range_r0_le

L63 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H1_of_chartFinite.TwoChartCech.ChartFinite.range_r0_le
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H1_of_chartFinite
universe u
open Polynomial
namespace TwoChartCech
open _root_.TwoChartCech
namespace ChartFinite
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
    (S : TwoChartCech.Sections.{u, u, u} 𝒰)
Lean source · statement
theorem range_r0_le (g : 𝒰.A1) (s : Finset S.M0) (N : ℕ) : LinearMap.range S.r0 ≤ W S g s N
theorem

range_r1_le

L69 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H1_of_chartFinite.TwoChartCech.ChartFinite.range_r1_le
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H1_of_chartFinite
universe u
open Polynomial
namespace TwoChartCech
open _root_.TwoChartCech
namespace ChartFinite
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
    (S : TwoChartCech.Sections.{u, u, u} 𝒰)
Lean source · statement
theorem range_r1_le (g : 𝒰.A1) (s : Finset S.M0) (N : ℕ) : LinearMap.range S.r1 ≤ W S g s N
theorem

vpow_smul_mem_range_r1

L75 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H1_of_chartFinite.TwoChartCech.ChartFinite.vpow_smul_mem_range_r1
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H1_of_chartFinite
universe u
open Polynomial
namespace TwoChartCech
open _root_.TwoChartCech
namespace ChartFinite
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
    (S : TwoChartCech.Sections.{u, u, u} 𝒰)
Lean source · statement
theorem vpow_smul_mem_range_r1 (g : 𝒰.A1) {m : S.M01} {n : ℕ} (h : 𝒰.ρ1 g ^ n • m ∈
    LinearMap.range S.r1)
    (k : ℕ) (hk : n ≤ k) : 𝒰.ρ1 g ^ k • m ∈ LinearMap.range S.r1
theorem

upow_smul_r0_mem

L83 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H1_of_chartFinite.TwoChartCech.ChartFinite.upow_smul_r0_mem
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H1_of_chartFinite
universe u
open Polynomial
namespace TwoChartCech
open _root_.TwoChartCech
namespace ChartFinite
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
    (S : TwoChartCech.Sections.{u, u, u} 𝒰)
Lean source · statement
theorem upow_smul_r0_mem (f : 𝒰.A0) (x : S.M0) (i : ℕ) : 𝒰.ρ0 f ^ i • S.r0 x ∈ LinearMap.range
    S.r0
theorem

vpow_smul_r0_mem_W

L89 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H1_of_chartFinite.TwoChartCech.ChartFinite.vpow_smul_r0_mem_W
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H1_of_chartFinite
universe u
open Polynomial
namespace TwoChartCech
open _root_.TwoChartCech
namespace ChartFinite
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
    (S : TwoChartCech.Sections.{u, u, u} 𝒰)
variable {S}
Lean source · statement
theorem vpow_smul_r0_mem_W {g : 𝒰.A1} {s : Finset S.M0} {N : ℕ}
    (hN : ∀ e ∈ s, 𝒰.ρ1 g ^ N • S.r0 e ∈ LinearMap.range S.r1)
    {e : S.M0} (he : e ∈ s) (k : ℕ) : 𝒰.ρ1 g ^ k • S.r0 e ∈ W S g s N
theorem

vpow_smul_smul_mem_W

L100 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H1_of_chartFinite.TwoChartCech.ChartFinite.vpow_smul_smul_mem_W
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H1_of_chartFinite
universe u
open Polynomial
namespace TwoChartCech
open _root_.TwoChartCech
namespace ChartFinite
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
    (S : TwoChartCech.Sections.{u, u, u} 𝒰)
variable {S}
Lean source · statement
theorem vpow_smul_smul_mem_W {f : 𝒰.A0} {g : 𝒰.A1} (hfg : 𝒰.ρ0 f * 𝒰.ρ1 g = 1) {s : Finset S.M0}
    {N : ℕ} {y : S.M01}
    (hv : ∀ i : ℕ, 𝒰.ρ1 g ^ i • y ∈ W S g s N) (hu : ∀ i : ℕ, 𝒰.ρ0 f ^ i • y ∈ W S g s N)
    (p : Algebra.adjoin R ({f} : Set 𝒰.A0)) (n : ℕ) :
    𝒰.ρ1 g ^ n • ((𝒰.ρ0 (p : 𝒰.A0)) • y) ∈ W S g s N
theorem

vpow_smul_r0_mem_W_of_mem_span

L122 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H1_of_chartFinite.TwoChartCech.ChartFinite.vpow_smul_r0_mem_W_of_mem_span
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H1_of_chartFinite
universe u
open Polynomial
namespace TwoChartCech
open _root_.TwoChartCech
namespace ChartFinite
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
    (S : TwoChartCech.Sections.{u, u, u} 𝒰)
variable {S}
Lean source · statement
theorem vpow_smul_r0_mem_W_of_mem_span {f : 𝒰.A0} {g : 𝒰.A1} (hfg : 𝒰.ρ0 f * 𝒰.ρ1 g = 1) {s :
    Finset S.M0} {N : ℕ}
    (hN : ∀ e ∈ s, 𝒰.ρ1 g ^ N • S.r0 e ∈ LinearMap.range S.r1)
    {x : S.M0} (hx : x ∈ Submodule.span (Algebra.adjoin R ({f} : Set 𝒰.A0)) (s : Set S.M0)) (n :
      ℕ) :
    𝒰.ρ1 g ^ n • S.r0 x ∈ W S g s N
theorem

W_eq_top

L138 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H1_of_chartFinite.TwoChartCech.ChartFinite.W_eq_top
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H1_of_chartFinite
universe u
open Polynomial
namespace TwoChartCech
open _root_.TwoChartCech
namespace ChartFinite
open _root_.TwoChartCech
variable {R : Type u} [CommRing R] {𝒰 : TwoChartCech.Cover.{u, u} R}
    (S : TwoChartCech.Sections.{u, u, u} 𝒰)
variable {S}
Lean source · statement
theorem W_eq_top {f : 𝒰.A0} {g : 𝒰.A1} (hfg : 𝒰.ρ0 f * 𝒰.ρ1 g = 1) {s : Finset S.M0}
    (hs : Submodule.span (Algebra.adjoin R ({f} : Set 𝒰.A0)) (s : Set S.M0) = ⊤) {N : ℕ}
    (hN : ∀ e ∈ s, 𝒰.ρ1 g ^ N • S.r0 e ∈ LinearMap.range S.r1)
    (hloc0 : ∀ m : S.M01, ∃ n : ℕ, 𝒰.ρ0 f ^ n • m ∈ LinearMap.range S.r0) :
    W S g s N = ⊤
theorem

finite_H1_of_chartFinite

L155 ↗
TwoChartCech.Sections.finite_H1_of_chartFinite
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_Sections_finite_H1_of_chartFinite
universe u
open Polynomial
open TwoChartCech.ChartFinite in
Lean source · statement
theorem _root_.TwoChartCech.Sections.finite_H1_of_chartFinite
    {R : Type u} [CommRing 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)
    (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) :
    Module.Finite R S.H1

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