NYLL
Module

Scheme_TwoAffineOpenCover_finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite
13 declarations indexed from sourceView source ↗

Module documentation

Cohomology of a finite pushforward on two affine charts

Pushing an invertible module forward along a morphism finite over the field gives finite zeroth cohomology, vanishing first cohomology, and the rank formula for the zeroth group.

Imports8
Imported by2

Declarations

theorem

sections_eq_of_eq_bot

L57 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite.C3Aux.sections_eq_of_eq_bot
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace C3Aux
open TopologicalSpace Opposite
section Sheaf
universe v' u' w x
variable {C : Type u'} [Category.{v'} C] {FC : C → C → Type*} {CC : C → Type w}
variable [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC]
variable [HasLimitsOfSize.{x, x} C] [(forget C).ReflectsIsomorphisms]
variable [PreservesLimitsOfSize.{x, x} (forget C)]
variable {T : TopCat.{x}} (F : TopCat.Sheaf C T)
Lean source · statement
theorem sections_eq_of_eq_bot {W : Opens T} (h : W = ⊥) (s t : ToType (F.1.obj (op W))) :
    s = t
theorem

bijective_pi_restrict

L62 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite.C3Aux.bijective_pi_restrict
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace C3Aux
open TopologicalSpace Opposite
section Sheaf
universe v' u' w x
variable {C : Type u'} [Category.{v'} C] {FC : C → C → Type*} {CC : C → Type w}
variable [∀ X Y, FunLike (FC X Y) (CC X) (CC Y)] [ConcreteCategory C FC]
variable [HasLimitsOfSize.{x, x} C] [(forget C).ReflectsIsomorphisms]
variable [PreservesLimitsOfSize.{x, x} (forget C)]
variable {T : TopCat.{x}} (F : TopCat.Sheaf C T)
Lean source · full declaration
theorem bijective_pi_restrict {ι : Type*} (U : ι → Opens T) (W : Opens T) (hUW : ∀ i, U i ≤ W)
    (hW : W ≤ iSup U) (hdisj : ∀ i j, i ≠ j → U i ⊓ U j = ⊥) :
    Function.Bijective fun (s : ToType (F.1.obj (op W))) (i : ι) =>
      F.1.map (homOfLE (hUW i)).op s := by
  classical
  constructor
  · intro s t hst
    exact F.eq_of_locally_eq' U W (fun i => homOfLE (hUW i)) hW s t (fun i => congrFun hst i)
  · intro sf
    have hc : TopCat.Presheaf.IsCompatible F.1 U sf := by
      intro i j
      by_cases hij : i = j
      · subst hij
        exact congrArg (fun f : U i ⊓ U i ⟶ U i => F.1.map f.op (sf i)) (Subsingleton.elim _ _)
      · exact sections_eq_of_eq_bot F (hdisj i j hij) _ _
    obtain ⟨s, hs, -⟩ := F.existsUnique_gluing' U W (fun i => homOfLE (hUW i)) hW sf hc
    exact ⟨s, funext hs⟩
theorem

restrict_surjective_of_discrete

L82 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite.C3Aux.restrict_surjective_of_discrete
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace C3Aux
open TopologicalSpace Opposite
Lean source · statement
theorem restrict_surjective_of_discrete {Z : Scheme.{u}} [DiscreteTopology Z] (N : Z.Modules)
    {W W' : Z.Opens} (h : W ≤ W') :
    Function.Surjective (N.presheaf.map (homOfLE h).op)
theorem

finite_and_discrete_of_finite

L109 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite.C3Aux.finite_and_discrete_of_finite
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace C3Aux
open TopologicalSpace Opposite
Lean source · statement
theorem finite_and_discrete_of_finite {k : Type u} [Field k] {Z : Scheme.{u}} [IsAffine Z]
    (φ : k →+* Γ(Z, ⊤)) (hφ : φ.Finite) : Finite Z ∧ DiscreteTopology Z
abbrev

modK

L122 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite.C3Aux.modK
Documentation

The scalar action on sections induced by the given ring homomorphism from k.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace C3Aux
open TopologicalSpace Opposite
section PiDecomp
variable {k : Type u} [Field k] {Z : Scheme.{u}}
Lean source · statement
abbrev modK (M : Z.Modules) (W : Z.Opens) (ψ : k →+* Γ(Z, W)) : Module k Γ(M, W)
def

resHom

L126 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite.C3Aux.resHom
Documentation

The base ring homomorphism restricted from global sections to the chosen open.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace C3Aux
open TopologicalSpace Opposite
section PiDecomp
variable {k : Type u} [Field k] {Z : Scheme.{u}}
Lean source · statement
def resHom (ψ₀ : k →+* Γ(Z, ⊤)) (W : Z.Opens) : k →+* Γ(Z, W)
theorem

resHom_apply

L129 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite.C3Aux.resHom_apply
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace C3Aux
open TopologicalSpace Opposite
section PiDecomp
variable {k : Type u} [Field k] {Z : Scheme.{u}}
Lean source · statement
theorem resHom_apply (ψ₀ : k →+* Γ(Z, ⊤)) (W : Z.Opens) (r : k) :
    resHom ψ₀ W r = (Z.presheaf.map (homOfLE (le_top : W ≤ ⊤)).op).hom (ψ₀ r)
def

restrictₖ

L133 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite.C3Aux.restrictₖ
Documentation

Restriction of sections as a k-linear map for the induced scalar structures.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace C3Aux
open TopologicalSpace Opposite
section PiDecomp
variable {k : Type u} [Field k] {Z : Scheme.{u}}
Lean source · full declaration
def restrictₖ (M : Z.Modules) (ψ₀ : k →+* Γ(Z, ⊤)) (W : Z.Opens) :
    letI := modK M ⊤ ψ₀; letI := modK M W (resHom ψ₀ W)
    Γ(M, ⊤) →ₗ[k] Γ(M, W) :=
  letI := modK M ⊤ ψ₀; letI := modK M W (resHom ψ₀ W)
  { toFun := fun s => M.presheaf.map (homOfLE (le_top : W ≤ ⊤)).op s
    map_add' := fun a b => map_add _ a b
    map_smul' := fun r s => by
      change M.presheaf.map (homOfLE (le_top : W ≤ ⊤)).op (ψ₀ r • s)
        = resHom ψ₀ W r • M.presheaf.map (homOfLE (le_top : W ≤ ⊤)).op s
      rw [Scheme.Modules.map_smul]
      rfl }
theorem

restrictₖ_apply

L145 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite.C3Aux.restrictₖ_apply
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace C3Aux
open TopologicalSpace Opposite
section PiDecomp
variable {k : Type u} [Field k] {Z : Scheme.{u}}
Lean source · statement
theorem restrictₖ_apply (M : Z.Modules) (ψ₀ : k →+* Γ(Z, ⊤)) (W : Z.Opens) (s : Γ(M, ⊤)) :
    restrictₖ M ψ₀ W s = M.presheaf.map (homOfLE (le_top : W ≤ ⊤)).op s
def

piEquiv

L149 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite.C3Aux.piEquiv
Documentation

The linear decomposition of global sections over a pairwise disjoint open cover.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace C3Aux
open TopologicalSpace Opposite
section PiDecomp
variable {k : Type u} [Field k] {Z : Scheme.{u}}
Lean source · full declaration
def piEquiv (M : Z.Modules) (ψ₀ : k →+* Γ(Z, ⊤)) {ι : Type u} (U : ι → Z.Opens)
    (hcov : (⊤ : Z.Opens) ≤ iSup U) (hdisj : ∀ a b, a ≠ b → U a ⊓ U b = ⊥) :
    letI := modK M ⊤ ψ₀; letI := fun a => modK M (U a) (resHom ψ₀ (U a))
    Γ(M, ⊤) ≃ₗ[k] (∀ a, Γ(M, U a)) :=
  letI := modK M ⊤ ψ₀; letI := fun a => modK M (U a) (resHom ψ₀ (U a))
  LinearEquiv.ofBijective (LinearMap.pi fun a => restrictₖ M ψ₀ (U a))
    (bijective_pi_restrict (⟨M.presheaf, M.isSheaf⟩ : TopCat.Sheaf Ab Z) U ⊤ (fun _ => le_top)
      hcov hdisj)
instance

nativeUnitSectionsModule

L160 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite.C3Aux.nativeUnitSectionsModule
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace C3Aux
open TopologicalSpace Opposite
Lean source · statement
instance nativeUnitSectionsModule (Z : Scheme.{u}) (O : Z.Opens) :
    Module Γ(Z, O) Γ((SheafOfModules.unit Z.ringCatSheaf : Z.Modules), O)
theorem

exists_addEquiv_of_trivial

L164 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite.C3Aux.exists_addEquiv_of_trivial
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
noncomputable section
namespace C3Aux
open TopologicalSpace Opposite
local instance nativeUnitSectionsModule (Z : Scheme.{u}) (O : Z.Opens) :
    Module Γ(Z, O) Γ((SheafOfModules.unit Z.ringCatSheaf : Z.Modules), O) :=
  ((SheafOfModules.unit Z.ringCatSheaf : Z.Modules).val.obj (Opposite.op O)).isModule
Lean source · statement
theorem exists_addEquiv_of_trivial {Z : Scheme.{u}} (M : Z.Modules) (V : Z.Opens)
    (e : (Scheme.Modules.pullback V.ι).obj M ≅ SheafOfModules.unit V.toScheme.ringCatSheaf)
    (W : V.toScheme.Opens) :
    ∃ τ : Γ(M, V.ι ''ᵁ W) ≃+ Γ((SheafOfModules.unit Z.ringCatSheaf : Z.Modules), V.ι ''ᵁ W),
      ∀ (c : Γ(Z, V.ι ''ᵁ W)) (m : Γ(M, V.ι ''ᵁ W)), τ (c • m) = c • τ m
theorem

finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite

L197 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open C3Aux in
with_weak_namespace _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · statement
theorem finite_H0_and_subsingleton_H1_sectionsOf_pushforward_of_isFinite
    {k : Type u} [Field k] {Z X : Scheme.{u}} (x : X ⟶ Spec (CommRingCat.of k))
    (i : Z ⟶ X) (hZ : IsFinite (i ≫ x))
    (N : Z.Modules) (hN : Scheme.Modules.IsInvertible N) (𝒱 : X.TwoAffineOpenCover) :
    Module.Finite k (𝒱.sectionsOf x ((Scheme.Modules.pushforward i).obj N)).H0 ∧
      Subsingleton (𝒱.sectionsOf x ((Scheme.Modules.pushforward i).obj N)).H1 ∧
      ∀ t : Spec (CommRingCat.of k),
        Module.finrank k (𝒱.sectionsOf x ((Scheme.Modules.pushforward i).obj N)).H0 = (i ≫
            x).finrank t

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