Module

SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle.lean

Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle

19 declarations indexed from sourceView source ↗

Module documentation

Finite cohomology of line bundles on two charts

Localization expresses sections on a basic open using a denominator power. Finite maps on the two affine charts then give finite zeroth and first Cech cohomology for the associated line bundles.

Imports6

Mathlib.Util.WithWeakNamespace
Nyll.AlgebraicCurves.Geometry.Curves.SmoothProperCurveFiniteMapData
Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_Sections_finite_H1_of_chartFinite
Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_Sections_finite_H0_of_chartFinite
Mathlib.RingTheory.Noetherian.Basic
Mathlib.RingTheory.Adjoin.Polynomial.Basic

Imported by3

abbrev

res

L56 ↗

AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle.AlgebraicGeometry.Scheme.TwoAffineOpenCover.ChartFiniteInstances.res

Documentation

Restrict a structure-sheaf section to a smaller open subset.

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace ChartFiniteInstances
variable {X : Scheme.{u}}

Lean source · statement

abbrev res {U W : X.Opens} (h : W ≤ U) : Γ(X, U) → Γ(X, W)

theorem

res_res'

L59 ↗

AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle.AlgebraicGeometry.Scheme.TwoAffineOpenCover.ChartFiniteInstances.res_res'

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace ChartFiniteInstances
variable {X : Scheme.{u}}

Lean source · statement

theorem res_res' {V₁ V₂ V₃ : X.Opens} (h₂₁ : V₂ ≤ V₁) (h₃₂ : V₃ ≤ V₂) (x : Γ(X, V₁)) :
    res h₃₂ (res h₂₁ x) = res (h₃₂.trans h₂₁) x

theorem

res_self

L64 ↗

AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle.AlgebraicGeometry.Scheme.TwoAffineOpenCover.ChartFiniteInstances.res_self

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace ChartFiniteInstances
variable {X : Scheme.{u}}

Lean source · statement

theorem res_self {V : X.Opens} (h : V ≤ V) (x : Γ(X, V)) : res h x = x

theorem

exists_pow_mul_eq_res

L68 ↗

AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle.AlgebraicGeometry.Scheme.TwoAffineOpenCover.ChartFiniteInstances.exists_pow_mul_eq_res

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace ChartFiniteInstances
variable {X : Scheme.{u}}

Lean source · statement

theorem exists_pow_mul_eq_res {U W : X.Opens} (hU : IsAffineOpen U) (f : Γ(X, U)) (hW : W =
    X.basicOpen f)
    (m : Γ(X, W)) :
    ∃ (x : Γ(X, U)) (n : ℕ), res (hW.le.trans (X.basicOpen_le f)) f ^ n * m
      = res (hW.le.trans (X.basicOpen_le f)) x

theorem

exists_pow_mul_eq_zero

L81 ↗

AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle.AlgebraicGeometry.Scheme.TwoAffineOpenCover.ChartFiniteInstances.exists_pow_mul_eq_zero

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace ChartFiniteInstances
variable {X : Scheme.{u}}

Lean source · statement

theorem exists_pow_mul_eq_zero {U W : X.Opens} (hU : IsAffineOpen U) (f : Γ(X, U)) (hW : W =
    X.basicOpen f)
    (x : Γ(X, U)) (hx : res (hW.le.trans (X.basicOpen_le f)) x = 0) :
    ∃ n : ℕ, f ^ n * x = 0

theorem

finite_adjoin_of_aeval_finite

L92 ↗

AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle.AlgebraicGeometry.Scheme.TwoAffineOpenCover.ChartFiniteInstances.finite_adjoin_of_aeval_finite

Source context 20 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace Scheme
open _root_.AlgebraicGeometry.Scheme
namespace TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.AlgebraicGeometry.Scheme
open _root_.AlgebraicGeometry
namespace ChartFiniteInstances
variable {X : Scheme.{u}}

Lean source · statement

theorem finite_adjoin_of_aeval_finite {R : Type u} [CommRing R] {A : Type u} [CommRing A] [Algebra R
    A] (f : A)
    (h : (Polynomial.aeval f : Polynomial R →ₐ[R] A).toRingHom.Finite) :
    Module.Finite (Algebra.adjoin R ({f} : Set A)) A

theorem

VU_le_U

L136 ↗

AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.VU_le_U

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open AlgebraicGeometry.Scheme.TwoAffineOpenCover.ChartFiniteInstances
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (.of R))) c} (𝔉 : FiniteMapData c ε)

Lean source · statement

theorem VU_le_U : 𝔉.V ⊓ 𝔉.U ≤ 𝔉.U

theorem

VU_le_V

L137 ↗

AlgebraicCurves.Geometry.Curves.Proofs.SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.VU_le_V

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open AlgebraicGeometry.Scheme.TwoAffineOpenCover.ChartFiniteInstances
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (.of R))) c} (𝔉 : FiniteMapData c ε)

Lean source · statement

theorem VU_le_V : 𝔉.V ⊓ 𝔉.U ≤ 𝔉.V

theorem

VU_eq_basicOpen_g

L138 ↗

AlgebraicGeometry.SmoothProperCurve.FiniteMapData.VU_eq_basicOpen_g

Source context 21 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open AlgebraicGeometry.Scheme.TwoAffineOpenCover.ChartFiniteInstances
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (.of R))) c} (𝔉 : FiniteMapData c ε)

Lean source · statement

theorem _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.VU_eq_basicOpen_g : 𝔉.V ⊓
    𝔉.U = C.basicOpen 𝔉.g

theorem

VU_eq_basicOpen_f

L141 ↗

AlgebraicGeometry.SmoothProperCurve.FiniteMapData.VU_eq_basicOpen_f

Source context 22 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open AlgebraicGeometry.Scheme.TwoAffineOpenCover.ChartFiniteInstances
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (.of R))) c} (𝔉 : FiniteMapData c ε)
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData

Lean source · statement

theorem _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.VU_eq_basicOpen_f : 𝔉.V ⊓
    𝔉.U = C.basicOpen 𝔉.f

abbrev

gA0

L146 ↗

AlgebraicGeometry.SmoothProperCurve.FiniteMapData.gA0

Source context 24 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open AlgebraicGeometry.Scheme.TwoAffineOpenCover.ChartFiniteInstances
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (.of R))) c} (𝔉 : FiniteMapData c ε)
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
variable (c) in

Lean source · statement

abbrev _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.gA0 :
    (𝔉.twoAffineOpenCover.cover c).A0

abbrev

fA1

L150 ↗

AlgebraicGeometry.SmoothProperCurve.FiniteMapData.fA1

Source context 26 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open AlgebraicGeometry.Scheme.TwoAffineOpenCover.ChartFiniteInstances
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (.of R))) c} (𝔉 : FiniteMapData c ε)
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
variable (c) in
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
variable (c) in

Lean source · statement

abbrev _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.fA1 :
    (𝔉.twoAffineOpenCover.cover c).A1

theorem

ρ0_g_mul_ρ1_f

L155 ↗

AlgebraicGeometry.SmoothProperCurve.FiniteMapData.ρ0_g_mul_ρ1_f

Source context 27 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open AlgebraicGeometry.Scheme.TwoAffineOpenCover.ChartFiniteInstances
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (.of R))) c} (𝔉 : FiniteMapData c ε)
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
variable (c) in
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
variable (c) in
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData

Lean source · statement

theorem _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.ρ0_g_mul_ρ1_f :
    (𝔉.twoAffineOpenCover.cover c).ρ0 (𝔉.gA0 c) * (𝔉.twoAffineOpenCover.cover c).ρ1 (𝔉.fA1 c) = 1

theorem

loc0

L168 ↗

AlgebraicGeometry.SmoothProperCurve.FiniteMapData.loc0

Source context 28 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open AlgebraicGeometry.Scheme.TwoAffineOpenCover.ChartFiniteInstances
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (.of R))) c} (𝔉 : FiniteMapData c ε)
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
variable (c) in
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
variable (c) in
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData

Lean source · statement

theorem _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.loc0 (m :
    (𝔉.twoAffineOpenCover.cover c).A01) :
    ∃ (x : (𝔉.twoAffineOpenCover.cover c).A0) (n : ℕ),
      (𝔉.twoAffineOpenCover.cover c).ρ0 (𝔉.gA0 c) ^ n * m = (𝔉.twoAffineOpenCover.cover c).ρ0 x

theorem

loc1

L177 ↗

AlgebraicGeometry.SmoothProperCurve.FiniteMapData.loc1

Source context 29 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open AlgebraicGeometry.Scheme.TwoAffineOpenCover.ChartFiniteInstances
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (.of R))) c} (𝔉 : FiniteMapData c ε)
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
variable (c) in
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
variable (c) in
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData

Lean source · statement

theorem _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.loc1 (m :
    (𝔉.twoAffineOpenCover.cover c).A01) :
    ∃ (y : (𝔉.twoAffineOpenCover.cover c).A1) (n : ℕ),
      (𝔉.twoAffineOpenCover.cover c).ρ1 (𝔉.fA1 c) ^ n * m = (𝔉.twoAffineOpenCover.cover c).ρ1 y

theorem

tors0

L186 ↗

AlgebraicGeometry.SmoothProperCurve.FiniteMapData.tors0

Source context 30 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open AlgebraicGeometry.Scheme.TwoAffineOpenCover.ChartFiniteInstances
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (.of R))) c} (𝔉 : FiniteMapData c ε)
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
variable (c) in
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
variable (c) in
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData

Lean source · statement

theorem _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.tors0 (x :
    (𝔉.twoAffineOpenCover.cover c).A0) (hx : (𝔉.twoAffineOpenCover.cover c).ρ0 x = 0) :
    ∃ n : ℕ, 𝔉.gA0 c ^ n * x = 0

theorem

tors1

L192 ↗

AlgebraicGeometry.SmoothProperCurve.FiniteMapData.tors1

Source context 31 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open AlgebraicGeometry.Scheme.TwoAffineOpenCover.ChartFiniteInstances
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (.of R))) c} (𝔉 : FiniteMapData c ε)
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
variable (c) in
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
variable (c) in
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData

Lean source · statement

theorem _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.tors1 (y :
    (𝔉.twoAffineOpenCover.cover c).A1) (hy : (𝔉.twoAffineOpenCover.cover c).ρ1 y = 0) :
    ∃ n : ℕ, 𝔉.fA1 c ^ n * y = 0

theorem

chartFinite_lineBundle

L199 ↗

AlgebraicGeometry.SmoothProperCurve.FiniteMapData.chartFinite_lineBundle

Source context 32 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.NeronModelInfra
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace SmoothProperCurve
open _root_.AlgebraicGeometry.SmoothProperCurve
namespace FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open AlgebraicGeometry.Scheme.TwoAffineOpenCover.ChartFiniteInstances
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (.of R))) c} (𝔉 : FiniteMapData c ε)
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
variable (c) in
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
variable (c) in
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData
open _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData

Lean source · full declaration

theorem _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.chartFinite_lineBundle (t :
    (𝔉.twoAffineOpenCover.cover c).A01ˣ) :
    let 𝒰 := 𝔉.twoAffineOpenCover.cover c
    let S := 𝔉.twoAffineOpenCover.lineBundleSections c t
    (𝒰.ρ0 (𝔉.gA0 c) * 𝒰.ρ1 (𝔉.fA1 c) = 1) ∧
    Module.Finite (Algebra.adjoin R ({𝔉.gA0 c} : Set 𝒰.A0)) S.M0 ∧
    Module.Finite (Algebra.adjoin R ({𝔉.fA1 c} : Set 𝒰.A1)) S.M1 ∧
    (∀ m : S.M01, ∃ n : ℕ, (𝒰.ρ0 (𝔉.gA0 c)) ^ n • m ∈ LinearMap.range S.r0) ∧
    (∀ m : S.M01, ∃ n : ℕ, (𝒰.ρ1 (𝔉.fA1 c)) ^ n • m ∈ LinearMap.range S.r1) ∧
    (∀ x : S.M0, S.r0 x = 0 → ∃ n : ℕ, 𝔉.gA0 c ^ n • x = 0) ∧
    (∀ y : S.M1, S.r1 y = 0 → ∃ n : ℕ, 𝔉.fA1 c ^ n • y = 0) := by
  intro 𝒰 S
  refine ⟨𝔉.ρ0_g_mul_ρ1_f, ?_, ?_, ?_, ?_, ?_, ?_⟩
  · exact finite_adjoin_of_aeval_finite (𝔉.gA0 c) 𝔉.finite_g
  · exact finite_adjoin_of_aeval_finite (𝔉.fA1 c) 𝔉.finite_f
  · intro m
    obtain ⟨x, n, h⟩ := 𝔉.loc0 m
    exact ⟨n, x, by rw [TwoChartCech.Cover.lineBundle_r0_apply, smul_eq_mul]; exact h.symm⟩
  · intro m
    obtain ⟨y, n, h⟩ := 𝔉.loc1 ((↑t⁻¹ : 𝒰.A01) * m)
    refine ⟨n, y, ?_⟩
    rw [TwoChartCech.Cover.lineBundle_r1_apply, smul_eq_mul, ← h, mul_left_comm, ← mul_assoc (t :
        𝒰.A01),
      Units.mul_inv, one_mul]
  · intro x hx
    rw [TwoChartCech.Cover.lineBundle_r0_apply] at hx
    obtain ⟨n, hn⟩ := 𝔉.tors0 x hx
    exact ⟨n, by rw [smul_eq_mul]; exact hn⟩
  · intro y hy
    rw [TwoChartCech.Cover.lineBundle_r1_apply] at hy
    obtain ⟨n, hn⟩ := 𝔉.tors1 y ((Units.mul_right_eq_zero t).mp hy)
    exact ⟨n, by rw [smul_eq_mul]; exact hn⟩

theorem

finite_H0_H1_lineBundle

L235 ↗

AlgebraicGeometry.SmoothProperCurve.FiniteMapData.finite_H0_H1_lineBundle

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace SmoothProperCurve_FiniteMapData_finite_H0_H1_lineBundle
noncomputable section
universe u
open _root_.CategoryTheory
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.NeronModelInfra

Lean source · statement

theorem _root_.AlgebraicGeometry.SmoothProperCurve.FiniteMapData.finite_H0_H1_lineBundle
    {R : Type u} [CommRing R] [IsNoetherianRing R] {C : Scheme.{u}} {c : C ⟶ Spec (.of R)}
    {ε : SchemeHomOver (𝟙 (Spec (.of R))) c} (𝔉 : SmoothProperCurve.FiniteMapData c ε)
    (t : (𝔉.twoAffineOpenCover.cover c).A01ˣ) :
    Module.Finite R (𝔉.twoAffineOpenCover.lineBundleSections c t).H0 ∧
      Module.Finite R (𝔉.twoAffineOpenCover.lineBundleSections c t).H1

Module documentation

Finite cohomology of line bundles on two charts

Declarations