NYLL
Module

TwoChartCech_nonempty_kerBaseChangeTowerEquiv.lean

Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_nonempty_kerBaseChangeTowerEquiv
6 declarations indexed from sourceView source ↗

Module documentation

Equivalences between kernel base changes along a tower of fields.

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 by2

Declarations

theorem

kerBaseChangeHom_bijective_of_flat

L40 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_nonempty_kerBaseChangeTowerEquiv.TwoChartCech.kerBaseChangeHom_bijective_of_flat
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_nonempty_kerBaseChangeTowerEquiv
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

L69 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_nonempty_kerBaseChangeTowerEquiv.TwoChartCech.cancelBaseChange_tmul_baseChange
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_nonempty_kerBaseChangeTowerEquiv
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) [CommRing K] [CommRing 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

L79 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_nonempty_kerBaseChangeTowerEquiv.TwoChartCech.cancelBaseChange_baseChange
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_nonempty_kerBaseChangeTowerEquiv
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) [CommRing K] [CommRing 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

L87 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_nonempty_kerBaseChangeTowerEquiv.TwoChartCech.map_cancelBaseChange_ker
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_nonempty_kerBaseChangeTowerEquiv
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) [CommRing K] [CommRing 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

L106 ↗
AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_nonempty_kerBaseChangeTowerEquiv.TwoChartCech.kerCancelEquiv
Documentation

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

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_nonempty_kerBaseChangeTowerEquiv
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) [CommRing K] [CommRing 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

nonempty_kerBaseChangeTowerEquiv

L115 ↗
TwoChartCech.nonempty_kerBaseChangeTowerEquiv
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_nonempty_kerBaseChangeTowerEquiv
noncomputable section
universe u
open scoped TensorProduct
Lean source · statement
theorem _root_.TwoChartCech.nonempty_kerBaseChangeTowerEquiv
    {R : Type u} [CommRing R] {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1]
      [Module R C1]
    (d : C0 →ₗ[R] C1) (S T : Type u) [CommRing S] [CommRing T] [Algebra R S] [Algebra R T]
      [Algebra S T]
    [IsScalarTower R S T] :
    ∃ e : LinearMap.ker ((d.baseChange S).baseChange T) ≃ₗ[T] LinearMap.ker (d.baseChange T),
      ∀ z, (e z : T ⊗[R] C0) = TensorProduct.AlgebraTensorModule.cancelBaseChange R S T T C0 z

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