NYLL
Module

TwoChartCech_finrank_ker_baseChange_eq_of_field_extension.lean

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

Module documentation

The dimension of a Cech kernel after base change is unchanged by a field extension.

Imports8
  • Nyll.SchemeTheory.Cohomology.Cech.TwoChartCech
  • Mathlib.LinearAlgebra.Dimension.Finrank
  • Mathlib.LinearAlgebra.Dimension.Free
  • Mathlib.LinearAlgebra.Basis.VectorSpace
  • Mathlib.LinearAlgebra.FreeModule.Finite.Basic
  • Mathlib.RingTheory.Flat.Basic
  • Mathlib.RingTheory.TensorProduct.Free
  • Mathlib.LinearAlgebra.TensorProduct.Tower
Imported by4

Declarations

theorem

kerBaseChangeHom_bijective_of_flat

L41 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_finrank_ker_baseChange_eq_of_field_extension.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 TwoChartCech_finrank_ker_baseChange_eq_of_field_extension
noncomputable section
universe u
open scoped 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

L70 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_finrank_ker_baseChange_eq_of_field_extension.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 TwoChartCech_finrank_ker_baseChange_eq_of_field_extension
noncomputable section
universe u
open scoped 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

L80 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_finrank_ker_baseChange_eq_of_field_extension.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 TwoChartCech_finrank_ker_baseChange_eq_of_field_extension
noncomputable section
universe u
open scoped 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

L88 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_finrank_ker_baseChange_eq_of_field_extension.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 TwoChartCech_finrank_ker_baseChange_eq_of_field_extension
noncomputable section
universe u
open scoped 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

L107 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_finrank_ker_baseChange_eq_of_field_extension.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 TwoChartCech_finrank_ker_baseChange_eq_of_field_extension
noncomputable section
universe u
open scoped 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'

L112 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_finrank_ker_baseChange_eq_of_field_extension.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 TwoChartCech_finrank_ker_baseChange_eq_of_field_extension
noncomputable section
universe u
open scoped 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_baseChange_eq_of_field_extension

L131 ↗
TwoChartCech.finrank_ker_baseChange_eq_of_field_extension
Source context 6 commands

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

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

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