NYLL
Module

Scheme_TwoAffineOpenCover_finrank_H0_sectionsOf_baseChange_eq_and_subsingleton_H1_iff.lean

Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_TwoAffineOpenCover_finrank_H0_sectionsOf_baseChange_eq_and_subsingleton_H1_iff
2 declarations indexed from sourceView source ↗

Module documentation

Ranks and vanishing of two-chart cohomology after a field extension

The base-change equivalences of sections on two affine charts and their overlap identify zeroth-cohomology rank and the vanishing of first cohomology across a field extension.

Imports5
Imported by4

Declarations

theorem

main

L40 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.Scheme_TwoAffineOpenCover_finrank_H0_sectionsOf_baseChange_eq_and_subsingleton_H1_iff.CechFieldBCSketch.main
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_finrank_H0_sectionsOf_baseChange_eq_and_subsingleton_H1_iff
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
namespace CechFieldBCSketch
variable {k : Type u} [Field k] {k' : Type u} [Field k'] [Algebra k k']
Lean source · statement
theorem main
    {P0 P1 P01 : Type u} [AddCommGroup P0] [Module k P0] [AddCommGroup P1] [Module k P1]
        [AddCommGroup P01] [Module k P01]
    (r0 : P0 →ₗ[k] P01) (r1 : P1 →ₗ[k] P01)
    {Q0 Q1 Q01 : Type u} [AddCommGroup Q0] [Module k' Q0] [AddCommGroup Q1] [Module k' Q1]
        [AddCommGroup Q01] [Module k' Q01]
    (s0 : Q0 →ₗ[k'] Q01) (s1 : Q1 →ₗ[k'] Q01)
    (e0 : k' ⊗[k] P0 ≃ₗ[k'] Q0) (e1 : k' ⊗[k] P1 ≃ₗ[k'] Q1) (e01 : k' ⊗[k] P01 ≃ₗ[k'] Q01)
    (h0 : ∀ x, e01 ((r0.baseChange k') x) = s0 (e0 x)) (h1 : ∀ x, e01 ((r1.baseChange k') x) =
        s1 (e1 x)) :
    Module.finrank k' (LinearMap.ker ((-s0).coprod s1)) = Module.finrank k (LinearMap.ker
        ((-r0).coprod r1)) ∧
      (Subsingleton (Q01 ⧸ LinearMap.range ((-s0).coprod s1)) ↔ Subsingleton (P01 ⧸
          LinearMap.range ((-r0).coprod r1)))
theorem

finrank_H0_sectionsOf_baseChange_eq_and_subsingleton_H1_iff

L139 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.finrank_H0_sectionsOf_baseChange_eq_and_subsingleton_H1_iff
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace Scheme_TwoAffineOpenCover_finrank_H0_sectionsOf_baseChange_eq_and_subsingleton_H1_iff
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TensorProduct
open CechFieldBCSketch in
with_weak_namespace _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
Lean source · statement
theorem finrank_H0_sectionsOf_baseChange_eq_and_subsingleton_H1_iff
    {k : Type u} [Field k] {X : Scheme.{u}} (x : X ⟶ Spec (CommRingCat.of k)) (𝒱 :
        X.TwoAffineOpenCover)
    (M : X.Modules)
    (hM : ∀ p : X, ∃ U : X.Opens, p ∈ U ∧
      Nonempty ((Scheme.Modules.pullback U.ι).obj M ≅ SheafOfModules.unit U.toScheme.ringCatSheaf))
    (k' : Type u) [Field k'] [Algebra k k'] :
    Module.finrank k'
        ((𝒱.pullback x k').sectionsOf (pullback.snd x (Scheme.TwoAffineOpenCover.specMap k k'))
          ((Scheme.Modules.pullback (pullback.fst x (Scheme.TwoAffineOpenCover.specMap k
              k'))).obj M)).H0 =
      Module.finrank k (𝒱.sectionsOf x M).H0 ∧
    (Subsingleton ((𝒱.pullback x k').sectionsOf (pullback.snd x
        (Scheme.TwoAffineOpenCover.specMap k k'))
          ((Scheme.Modules.pullback (pullback.fst x (Scheme.TwoAffineOpenCover.specMap k
              k'))).obj M)).H1 ↔
      Subsingleton (𝒱.sectionsOf x M).H1)

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