NYLL
Module

Exists_twoAffineOpenCover_fibre_finrank_eq_finrank_cechDiff_baseChange_residueField.lean

Nyll.JacobianVarieties.Picard.Exists_twoAffineOpenCover_fibre_finrank_eq_finrank_cechDiff_baseChange_residueField
9 declarations indexed from sourceView source ↗

Module documentation

Relative Picard varieties and fibre cohomology

Compare the cohomology of a fibre cover with the base change of its chart Čech differential to the residue field.

Imports8
Imported by10

Declarations

def

kerEquivOfConj

L50 ↗
JacobianVarieties.Picard.Proofs.Exists_twoAffineOpenCover_fibre_finrank_eq_finrank_cechDiff_baseChange_residueField.ChiFibre.kerEquivOfConj
Documentation

The kernel equivalence induced by linear conjugacy of the two maps.

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs
namespace Exists_twoAffineOpenCover_fibre_finrank_eq_finrank_cechDiff_baseChange_residueField
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra TensorProduct
open scoped TensorProduct
namespace ChiFibre
section Conj
variable {R : Type*} [CommRing R] {M N M' N' : Type*} [AddCommGroup M] [Module R M]
  [AddCommGroup N] [Module R N]
  [AddCommGroup M'] [Module R M'] [AddCommGroup N'] [Module R N']
Lean source · statement
def kerEquivOfConj (f : M →ₗ[R] N) (f' : M' →ₗ[R] N') (eM : M ≃ₗ[R] M') (eN :
  N ≃ₗ[R] N')
    (h : ∀ x, eN (f x) = f' (eM x)) : LinearMap.ker f ≃ₗ[R] LinearMap.ker f'
def

cokerEquivOfConj

L65 ↗
JacobianVarieties.Picard.Proofs.Exists_twoAffineOpenCover_fibre_finrank_eq_finrank_cechDiff_baseChange_residueField.ChiFibre.cokerEquivOfConj
Documentation

The quotient-of-range equivalence induced by linear conjugacy of the two maps.

Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs
namespace Exists_twoAffineOpenCover_fibre_finrank_eq_finrank_cechDiff_baseChange_residueField
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra TensorProduct
open scoped TensorProduct
namespace ChiFibre
section Conj
variable {R : Type*} [CommRing R] {M N M' N' : Type*} [AddCommGroup M] [Module R M]
  [AddCommGroup N] [Module R N]
  [AddCommGroup M'] [Module R M'] [AddCommGroup N'] [Module R N']
Lean source · statement
def cokerEquivOfConj (f : M →ₗ[R] N) (f' : M' →ₗ[R] N') (eM : M ≃ₗ[R] M') (eN :
  N ≃ₗ[R] N')
    (h : ∀ x, eN (f x) = f' (eM x)) : (N ⧸ LinearMap.range f) ≃ₗ[R] (N' ⧸ LinearMap.range f')
theorem

nonempty_cokerBaseChangeEquiv

L84 ↗
JacobianVarieties.Picard.Proofs.Exists_twoAffineOpenCover_fibre_finrank_eq_finrank_cechDiff_baseChange_residueField.ChiFibre.nonempty_cokerBaseChangeEquiv
Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs
namespace Exists_twoAffineOpenCover_fibre_finrank_eq_finrank_cechDiff_baseChange_residueField
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra TensorProduct
open scoped TensorProduct
namespace ChiFibre
section Coker
variable {R : Type*} [CommRing R] {C0 C1 : Type*} [AddCommGroup C0] [Module R C0]
  [AddCommGroup C1] [Module R C1]
Lean source · statement
theorem nonempty_cokerBaseChangeEquiv (d : C0 →ₗ[R] C1) (A : Type*) [CommRing A] [Algebra R A] :
    Nonempty (((A ⊗[R] C1) ⧸ LinearMap.range (d.baseChange A)) ≃ₗ[A] A ⊗[R]
      (C1 ⧸ LinearMap.range d))
theorem

nonempty_kerBaseChangeEquiv_of_flat

L119 ↗
JacobianVarieties.Picard.Proofs.Exists_twoAffineOpenCover_fibre_finrank_eq_finrank_cechDiff_baseChange_residueField.ChiFibre.nonempty_kerBaseChangeEquiv_of_flat
Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs
namespace Exists_twoAffineOpenCover_fibre_finrank_eq_finrank_cechDiff_baseChange_residueField
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra TensorProduct
open scoped TensorProduct
namespace ChiFibre
section FieldExt
variable {R : Type*} [CommRing R] {C0 C1 : Type*} [AddCommGroup C0] [Module R C0]
  [AddCommGroup C1] [Module R C1]
Lean source · statement
theorem nonempty_kerBaseChangeEquiv_of_flat {K : Type*} [CommRing K] {V0 V1 : Type*}
  [AddCommGroup V0] [Module K V0]
    [AddCommGroup V1] [Module K V1] (δ : V0 →ₗ[K] V1) (K' : Type*) [CommRing K'] [Algebra K K']
      [Module.Flat K K'] :
    Nonempty (LinearMap.ker (δ.baseChange K') ≃ₗ[K'] K' ⊗[K] LinearMap.ker δ)
theorem

baseChange_baseChange_conj

L154 ↗
JacobianVarieties.Picard.Proofs.Exists_twoAffineOpenCover_fibre_finrank_eq_finrank_cechDiff_baseChange_residueField.ChiFibre.baseChange_baseChange_conj
Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs
namespace Exists_twoAffineOpenCover_fibre_finrank_eq_finrank_cechDiff_baseChange_residueField
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra TensorProduct
open scoped TensorProduct
namespace ChiFibre
section FieldExt
variable {R : Type*} [CommRing R] {C0 C1 : Type*} [AddCommGroup C0] [Module R C0]
  [AddCommGroup C1] [Module R C1]
Lean source · statement
theorem baseChange_baseChange_conj (d : C0 →ₗ[R] C1) (K K' : Type*) [CommRing K] [CommRing K']
  [Algebra R K]
    [Algebra R K'] [Algebra K K'] [IsScalarTower R K K'] (x : K' ⊗[K] (K ⊗[R] C0)) :
    TensorProduct.AlgebraTensorModule.cancelBaseChange R K K' K' C1
      ((d.baseChange K).baseChange K' x) =
      d.baseChange K' (TensorProduct.AlgebraTensorModule.cancelBaseChange R K K' K' C0 x)
theorem

finrank_ker_coker_baseChange_field

L163 ↗
JacobianVarieties.Picard.Proofs.Exists_twoAffineOpenCover_fibre_finrank_eq_finrank_cechDiff_baseChange_residueField.ChiFibre.finrank_ker_coker_baseChange_field
Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs
namespace Exists_twoAffineOpenCover_fibre_finrank_eq_finrank_cechDiff_baseChange_residueField
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra TensorProduct
open scoped TensorProduct
namespace ChiFibre
section FieldExt
variable {R : Type*} [CommRing R] {C0 C1 : Type*} [AddCommGroup C0] [Module R C0]
  [AddCommGroup C1] [Module R C1]
Lean source · statement
theorem finrank_ker_coker_baseChange_field {K : Type*} [Field K] {V0 V1 : Type*}
  [AddCommGroup V0] [Module K V0]
    [AddCommGroup V1] [Module K V1] (δ : V0 →ₗ[K] V1) (K' : Type*) [Field K'] [Algebra K K'] :
    Module.finrank K' (LinearMap.ker (δ.baseChange K')) = Module.finrank K (LinearMap.ker δ) ∧
    Module.finrank K' ((K' ⊗[K] V1) ⧸ LinearMap.range (δ.baseChange K')) =
      Module.finrank K (V1 ⧸ LinearMap.range δ)
theorem

finrank_ker_coker_baseChange_eq

L174 ↗
JacobianVarieties.Picard.Proofs.Exists_twoAffineOpenCover_fibre_finrank_eq_finrank_cechDiff_baseChange_residueField.ChiFibre.finrank_ker_coker_baseChange_eq
Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs
namespace Exists_twoAffineOpenCover_fibre_finrank_eq_finrank_cechDiff_baseChange_residueField
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra TensorProduct
open scoped TensorProduct
namespace ChiFibre
section FieldExt
variable {R : Type*} [CommRing R] {C0 C1 : Type*} [AddCommGroup C0] [Module R C0]
  [AddCommGroup C1] [Module R C1]
Lean source · statement
theorem finrank_ker_coker_baseChange_eq (d : C0 →ₗ[R] C1) (K K' : Type*) [Field K] [Field K']
  [Algebra R K]
    [Algebra R K'] [Algebra K K'] [IsScalarTower R K K'] :
    Module.finrank K' (LinearMap.ker (d.baseChange K')) = Module.finrank K (LinearMap.ker
      (d.baseChange K)) ∧
    Module.finrank K' ((K' ⊗[R] C1) ⧸ LinearMap.range (d.baseChange K')) =
      Module.finrank K ((K ⊗[R] C1) ⧸ LinearMap.range (d.baseChange K))
theorem

cover_ext

L194 ↗
JacobianVarieties.Picard.Proofs.Exists_twoAffineOpenCover_fibre_finrank_eq_finrank_cechDiff_baseChange_residueField.ChiFibre.cover_ext
Source context 8 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs
namespace Exists_twoAffineOpenCover_fibre_finrank_eq_finrank_cechDiff_baseChange_residueField
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra TensorProduct
open scoped TensorProduct
namespace ChiFibre
Lean source · statement
theorem cover_ext {X : Scheme.{u}} {𝒱 𝒱' : X.TwoAffineOpenCover}
    (h0 : 𝒱.U0 = 𝒱'.U0) (h1 : 𝒱.U1 = 𝒱'.U1) : 𝒱 = 𝒱'
theorem

exists_twoAffineOpenCover_fibre_finrank_eq_finrank_cechDiff_baseChange_residueField

L203 ↗
AlgebraicGeometry.RelPicard.exists_twoAffineOpenCover_fibre_finrank_eq_finrank_cechDiff_baseChange_residueField
Source context 10 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs
namespace Exists_twoAffineOpenCover_fibre_finrank_eq_finrank_cechDiff_baseChange_residueField
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
  NeronModelInfra TensorProduct
open scoped TensorProduct
open ChiFibre in
open Exists_twoAffineOpenCover_fibre_finrank_eq_finrank_cechDiff_baseChange_residueField in
with_weak_namespace _root_.AlgebraicGeometry.RelPicard
Lean source · statement
theorem exists_twoAffineOpenCover_fibre_finrank_eq_finrank_cechDiff_baseChange_residueField
    {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R))
    {A : Type u} [CommRing A] (j : Spec (CommRingCat.of A) ⟶ T) [IsOpenImmersion j]
    {CA : Scheme.{u}} (πA : CA ⟶ Spec (CommRingCat.of A)) (g' : CA ⟶ pullback c t)
    (hcart : IsPullback g' πA (pullback.snd c t) j)
    (𝒱 : CA.TwoAffineOpenCover) (𝔭 : PrimeSpectrum A)
    {k : Type u} [Field k] (s : Spec (CommRingCat.of k) ⟶ T)
    (hs : s.base (IsLocalRing.closedPoint k) = j.base 𝔭) :
    ∃ 𝒲 : (pullback (pullback.snd c t) s).TwoAffineOpenCover,
      ∀ (M : (pullback c t).Modules), Scheme.Modules.IsInvertible M →
        Module.finrank k (𝒲.sectionsOf (fibreAt c t s) (fibreModule c t s M)).H0 =
          Module.finrank 𝔭.asIdeal.ResidueField
            (LinearMap.ker ((𝒱.sectionsOf πA ((Scheme.Modules.pullback g').obj
              M)).cechDiff.baseChange
              𝔭.asIdeal.ResidueField)) ∧
        Module.finrank k (𝒲.sectionsOf (fibreAt c t s) (fibreModule c t s M)).H1 =
          Module.finrank 𝔭.asIdeal.ResidueField
            ((𝔭.asIdeal.ResidueField ⊗[A] (𝒱.sectionsOf πA
              ((Scheme.Modules.pullback g').obj M)).M01) ⧸
              LinearMap.range ((𝒱.sectionsOf πA ((Scheme.Modules.pullback g').obj
                M)).cechDiff.baseChange
                𝔭.asIdeal.ResidueField))

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