NYLL
Module

TwoChartCech_exists_fibreH0Family.lean

Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_exists_fibreH0Family
7 declarations indexed from sourceView source ↗

Module documentation

Fibre dimension data for a finite two-term kernel after pullback to a scheme over the base ring.

Imports11
Imported by2

Declarations

def

baseChangeTTC

L45 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_fibreH0Family.TwoChartCech.Family.baseChangeTTC
Documentation

The base change of a finite free two term complex to an algebra over the original ring.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_fibreH0Family
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TensorProduct
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Family
Lean source · statement
def baseChangeTTC {R : Type u} [CommRing R] (G : CoherentBaseChange.TwoTermComplex.{u, u} R)
    (S : Type u) [CommRing S] [Algebra R S] : CoherentBaseChange.TwoTermComplex.{u, u} S
def

algebraOfHom'

L54 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_fibreH0Family.TwoChartCech.Family.algebraOfHom'
Documentation

The algebra structure on an open section ring induced by the morphism to the affine base.

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_fibreH0Family
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TensorProduct
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Family
Lean source · statement
def algebraOfHom' {R : Type u} [CommRing R] {T : Scheme.{u}} (f : T ⟶ Spec (.of R))
  (U : T.Opens) :
    Algebra R Γ(T, U)
theorem

specMap_algebraMap_eq

L59 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_fibreH0Family.TwoChartCech.Family.specMap_algebraMap_eq
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_fibreH0Family
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TensorProduct
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Family
Lean source · full declaration
theorem specMap_algebraMap_eq {R : Type u} [CommRing R] {T : Scheme.{u}} (f : T ⟶ Spec (.of R)) (U
    : T.Opens)
    (hU : IsAffineOpen U) :
    letI := algebraOfHom' f U
    Spec.map (CommRingCat.ofHom (algebraMap R Γ(T, U))) = hU.fromSpec ≫ f := by
  let := algebraOfHom' f U
  have halg : (algebraMap R Γ(T, U)) = ((Scheme.ΓSpecIso (.of R)).inv ≫ f.appLE ⊤ U le_top).hom :=
    rfl
  rw [halg, CommRingCat.ofHom_hom, Spec.map_comp, ← Scheme.isoSpec_Spec_inv, ←
    IsAffineOpen.fromSpec_top,
    IsAffineOpen.SpecMap_appLE_fromSpec f (isAffineOpen_top (Spec (.of R))) hU (le_top : U ≤ f ⁻¹ᵁ
      ⊤)]
theorem

base_eq_comap

L72 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_fibreH0Family.TwoChartCech.Family.base_eq_comap
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_fibreH0Family
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TensorProduct
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Family
Lean source · full declaration
theorem base_eq_comap {R : Type u} [CommRing R] {T : Scheme.{u}} (f : T ⟶ Spec (.of R)) (U :
    T.Opens)
    (hU : IsAffineOpen U) (x : U) :
    letI := algebraOfHom' f U
    f.base x.1 = PrimeSpectrum.comap (algebraMap R Γ(T, U)) (hU.primeIdealOf x) := by
  let := algebraOfHom' f U
  have h1 : f.base x.1 = (hU.fromSpec ≫ f).base (hU.primeIdealOf x) := by
    rw [Scheme.Hom.comp_base]
    erw [TopCat.comp_app, hU.fromSpec_primeIdealOf x]
  rw [h1, ← specMap_algebraMap_eq f U hU]
  rfl
theorem

nativeSpecPrime

L88 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_fibreH0Family.TwoChartCech.nativeSpecPrime
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_fibreH0Family
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TensorProduct
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
open Family
Lean source · statement
theorem nativeSpecPrime {R : Type u} [CommRing R] (p : Spec (.of R)) :
    p.asIdeal.IsPrime
theorem

exists_fibreH0Family'

L93 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_fibreH0Family.TwoChartCech.exists_fibreH0Family'
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_fibreH0Family
noncomputable section
universe u
open CategoryTheory AlgebraicGeometry Opposite TensorProduct
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
open Family
attribute [local instance] nativeSpecPrime
Lean source · statement
theorem exists_fibreH0Family'
    {R : Type u} [CommRing R] [IsNoetherianRing R]
    {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
    [Module.Flat R C0] [Module.Flat R C1] (d : C0 →ₗ[R] C1)
    [Module.Finite R (LinearMap.ker d)] [Module.Finite R (C1 ⧸ LinearMap.range d)]
    {T : Scheme.{u}} (f : T ⟶ Spec (.of R)) :
    ∃ F : CoherentBaseChange.FibreH0Family T,
      ∀ x : T, F.h0 x = Module.finrank (f.base x).asIdeal.ResidueField
        (LinearMap.ker (d.baseChange (f.base x).asIdeal.ResidueField))
theorem

exists_fibreH0Family

L135 ↗
TwoChartCech.exists_fibreH0Family
Source context 4 commands

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

section ProofImplementation
universe u
open CategoryTheory AlgebraicGeometry TensorProduct
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs in
Lean source · full declaration
theorem TwoChartCech.exists_fibreH0Family
    {R : Type u} [CommRing R] [IsNoetherianRing R]
    {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
    [Module.Flat R C0] [Module.Flat R C1] (d : C0 →ₗ[R] C1)
    [Module.Finite R (LinearMap.ker d)] [Module.Finite R (C1 ⧸ LinearMap.range d)]
    {T : Scheme.{u}} (f : T ⟶ Spec (.of R)) :
    ∃ F : CoherentBaseChange.FibreH0Family T,
      ∀ x : T, letI := (f.base x).isPrime; F.h0 x =
        Module.finrank (f.base x).asIdeal.ResidueField
          (LinearMap.ker (d.baseChange (f.base x).asIdeal.ResidueField)) := by
  obtain ⟨F, hF⟩ :=
    TwoChartCech_exists_fibreH0Family.TwoChartCech.exists_fibreH0Family'
      (R := R) (C0 := C0) (C1 := C1) (d := d) (T := T) (f := f)
  refine ⟨F, fun x => ?_⟩
  exact hF x

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