NYLL
Module

Scheme_TwoAffineOpenCover_finrank_ker_cechDiff_baseChange_eq_one.lean

Nyll.AlgebraicCurves.Cohomology.Cech.Scheme_TwoAffineOpenCover_finrank_ker_cechDiff_baseChange_eq_one
8 declarations indexed from sourceView source ↗

Module documentation

The base-changed structure-sheaf Cech kernel has dimension one for a smooth proper integral curve.

Imports14
Imported by2

Declarations

theorem

kerBaseChangeHom_bijective_of_flat

L47 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.Scheme_TwoAffineOpenCover_finrank_ker_cechDiff_baseChange_eq_one.TwoChartCech.kerBaseChangeHom_bijective_of_flat
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace Scheme_TwoAffineOpenCover_finrank_ker_cechDiff_baseChange_eq_one
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
Lean source · statement
theorem kerBaseChangeHom_bijective_of_flat {R : Type u} [CommRing R] {C0 C1 : Type u}
    [AddCommGroup C0]
    [Module R C0] [AddCommGroup C1] [Module R C1] (d : C0 →ₗ[R] C1) (A : Type u) [CommRing A]
      [Algebra R A]
    [Module.Flat R A] : Function.Bijective (kerBaseChangeHom d A)
theorem

cancelBaseChange_tmul_baseChange

L76 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.Scheme_TwoAffineOpenCover_finrank_ker_cechDiff_baseChange_eq_one.TwoChartCech.cancelBaseChange_tmul_baseChange
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace Scheme_TwoAffineOpenCover_finrank_ker_cechDiff_baseChange_eq_one
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
section ChangeField
variable {R : Type u} [CommRing R] {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup
  C1]
  [Module R C1] (d : C0 →ₗ[R] C1)
variable (K L : Type u) [Field K] [Field L] [Algebra R K] [Algebra R L] [Algebra K L]
  [IsScalarTower R K L]
Lean source · statement
theorem cancelBaseChange_tmul_baseChange (l : L) (x : K ⊗[R] C0) :
    TensorProduct.AlgebraTensorModule.cancelBaseChange R K L L C1 (l ⊗ₜ[K] (d.baseChange K x))
      = (d.baseChange L) (TensorProduct.AlgebraTensorModule.cancelBaseChange R K L L C0 (l ⊗ₜ[K]
        x))
theorem

cancelBaseChange_baseChange

L86 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.Scheme_TwoAffineOpenCover_finrank_ker_cechDiff_baseChange_eq_one.TwoChartCech.cancelBaseChange_baseChange
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace Scheme_TwoAffineOpenCover_finrank_ker_cechDiff_baseChange_eq_one
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
section ChangeField
variable {R : Type u} [CommRing R] {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup
  C1]
  [Module R C1] (d : C0 →ₗ[R] C1)
variable (K L : Type u) [Field K] [Field L] [Algebra R K] [Algebra R L] [Algebra K L]
  [IsScalarTower R K L]
Lean source · statement
theorem cancelBaseChange_baseChange (z : L ⊗[K] (K ⊗[R] C0)) :
    TensorProduct.AlgebraTensorModule.cancelBaseChange R K L L C1 (((d.baseChange K).baseChange L)
      z)
      = (d.baseChange L) (TensorProduct.AlgebraTensorModule.cancelBaseChange R K L L C0 z)
theorem

map_cancelBaseChange_ker

L94 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.Scheme_TwoAffineOpenCover_finrank_ker_cechDiff_baseChange_eq_one.TwoChartCech.map_cancelBaseChange_ker
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace Scheme_TwoAffineOpenCover_finrank_ker_cechDiff_baseChange_eq_one
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
section ChangeField
variable {R : Type u} [CommRing R] {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup
  C1]
  [Module R C1] (d : C0 →ₗ[R] C1)
variable (K L : Type u) [Field K] [Field L] [Algebra R K] [Algebra R L] [Algebra K L]
  [IsScalarTower R K L]
Lean source · statement
theorem map_cancelBaseChange_ker :
    Submodule.map (TensorProduct.AlgebraTensorModule.cancelBaseChange R K L L C0).toLinearMap
        (LinearMap.ker ((d.baseChange K).baseChange L))
      = LinearMap.ker (d.baseChange L)
def

kerCancelEquiv

L113 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.Scheme_TwoAffineOpenCover_finrank_ker_cechDiff_baseChange_eq_one.TwoChartCech.kerCancelEquiv
Documentation

Identify the kernel after successive field base changes with the kernel after direct base change.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace Scheme_TwoAffineOpenCover_finrank_ker_cechDiff_baseChange_eq_one
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
section ChangeField
variable {R : Type u} [CommRing R] {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup
  C1]
  [Module R C1] (d : C0 →ₗ[R] C1)
variable (K L : Type u) [Field K] [Field L] [Algebra R K] [Algebra R L] [Algebra K L]
  [IsScalarTower R K L]
Lean source · statement
def kerCancelEquiv : LinearMap.ker ((d.baseChange K).baseChange L) ≃ₗ[L] LinearMap.ker
    (d.baseChange L)
theorem

finrank_ker_baseChange_eq

L118 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.Scheme_TwoAffineOpenCover_finrank_ker_cechDiff_baseChange_eq_one.TwoChartCech.finrank_ker_baseChange_eq
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace Scheme_TwoAffineOpenCover_finrank_ker_cechDiff_baseChange_eq_one
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
section ChangeField
variable {R : Type u} [CommRing R] {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup
  C1]
  [Module R C1] (d : C0 →ₗ[R] C1)
variable (K L : Type u) [Field K] [Field L] [Algebra R K] [Algebra R L] [Algebra K L]
  [IsScalarTower R K L]
Lean source · statement
theorem finrank_ker_baseChange_eq :
    Module.finrank K (LinearMap.ker (d.baseChange K)) = Module.finrank L (LinearMap.ker
      (d.baseChange L))
theorem

finrank_ker_eq_one_of_isAlgClosed

L147 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.Scheme_TwoAffineOpenCover_finrank_ker_cechDiff_baseChange_eq_one.AlgebraicGeometry.Scheme.TwoAffineOpenCover.finrank_ker_eq_one_of_isAlgClosed
Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace Scheme_TwoAffineOpenCover_finrank_ker_cechDiff_baseChange_eq_one
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
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
Lean source · statement
theorem finrank_ker_eq_one_of_isAlgClosed
    {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
    (L : Type u) [Field L] [IsAlgClosed L] [Algebra R L]
    [IsIntegral (Limits.pullback c (specMap R L))]
    [Module.Finite L (LinearMap.ker ((𝒱.structureSheafSections c).cechDiff.baseChange L))] :
    Module.finrank L (LinearMap.ker ((𝒱.structureSheafSections c).cechDiff.baseChange L)) = 1
theorem

finrank_ker_cechDiff_baseChange_eq_one

L171 ↗
AlgebraicGeometry.Scheme.TwoAffineOpenCover.finrank_ker_cechDiff_baseChange_eq_one
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace Scheme_TwoAffineOpenCover_finrank_ker_cechDiff_baseChange_eq_one
noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits Opposite TensorProduct
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
open _root_.AlgebraicCurves.Cohomology.Cech.Proofs in
open _root_.AlgebraicGeometry
  Scheme_TwoAffineOpenCover_finrank_ker_cechDiff_baseChange_eq_one.AlgebraicGeometry in
Lean source · statement
theorem _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover.finrank_ker_cechDiff_baseChange_eq_one
    {R : Type u} [CommRing R] {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover) (c : X ⟶ Spec (.of R))
    (hint : ∀ (L : Type u) [Field L] [IsAlgClosed L] [Algebra R L],
      IsIntegral (Limits.pullback c (Scheme.TwoAffineOpenCover.specMap R L)))
    (hfin : ∀ (L : Type u) [Field L] [IsAlgClosed L] [Algebra R L],
      Module.Finite L (LinearMap.ker ((𝒱.structureSheafSections c).cechDiff.baseChange L)))
    (K : Type u) [Field K] [Algebra R K] :
    Module.finrank K (LinearMap.ker ((𝒱.structureSheafSections c).cechDiff.baseChange K)) = 1

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