Module

TwoChartCech_projective_ker_of_isReduced_of_kerMapBaseChange_bijective.lean

Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_projective_ker_of_isReduced_of_kerMapBaseChange_bijective

8 declarations indexed from sourceView source ↗

Module documentation

Transfer projective-kernel and base-change conclusions to a Cech kernel. A finite two-term model with bijective kernel comparisons preserves the fibre dimensions.

Imports6

Nyll.SchemeTheory.Cohomology.Cech.TwoChartCech
Nyll.AlgebraicCurves.Cohomology.Cech.CoherentBaseChange_TwoTermComplex_projective_ker_of_isReduced_of_fibreH0_const
Mathlib.LinearAlgebra.Dimension.Finrank
Mathlib.LinearAlgebra.Dimension.Constructions
Mathlib.Algebra.Module.Projective
Mathlib.RingTheory.Nilpotent.Defs

Imported by2

theorem

lid_baseChange

L45 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_projective_ker_of_isReduced_of_kerMapBaseChange_bijective.TwoChartCech.KerModel.lid_baseChange

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_projective_ker_of_isReduced_of_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace KerModel
section Lid
variable {R : Type u} [CommRing R] {M N : Type u} [AddCommGroup M] [Module R M] [AddCommGroup N]
  [Module R N]

Lean source · statement

theorem lid_baseChange (f : M →ₗ[R] N) (x : R ⊗[R] M) :
    TensorProduct.lid R N (f.baseChange R x) = f (TensorProduct.lid R M x)

def

kerLidEquiv

L52 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_projective_ker_of_isReduced_of_kerMapBaseChange_bijective.TwoChartCech.KerModel.kerLidEquiv

Documentation

Identify the kernel after base change along the identity with the original kernel.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_projective_ker_of_isReduced_of_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace KerModel
section Lid
variable {R : Type u} [CommRing R] {M N : Type u} [AddCommGroup M] [Module R M] [AddCommGroup N]
  [Module R N]

Lean source · full declaration

def kerLidEquiv (f : M →ₗ[R] N) : LinearMap.ker (f.baseChange R) ≃ₗ[R] LinearMap.ker f where
  toFun x := ⟨TensorProduct.lid R M x, by
    rw [LinearMap.mem_ker, ← lid_baseChange, LinearMap.mem_ker.mp x.2, map_zero]⟩
  invFun y := ⟨(TensorProduct.lid R M).symm y, by
    rw [LinearMap.mem_ker]
    apply (TensorProduct.lid R N).injective
    rw [lid_baseChange, LinearEquiv.apply_symm_apply, LinearMap.mem_ker.mp y.2, map_zero]⟩
  map_add' x y := Subtype.ext (by simp)
  map_smul' r x := Subtype.ext (by simp)
  left_inv x := Subtype.ext (by simp)
  right_inv y := Subtype.ext (by simp)

theorem

bijective_kerMap_self

L74 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_projective_ker_of_isReduced_of_kerMapBaseChange_bijective.TwoChartCech.KerModel.bijective_kerMap_self

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_projective_ker_of_isReduced_of_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace KerModel
variable {R : Type u} [CommRing R] {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup
  C1]
  [Module R C1] {d : C0 →ₗ[R] C1}
  (G : CoherentBaseChange.TwoTermComplex.{u, u} R) (ι0 : G.C0 →ₗ[R] C0) (ι1 : G.C1 →ₗ[R] C1)
  (comm : d ∘ₗ ι0 = ι1 ∘ₗ G.d)
  (hG : ∀ (A : Type u) [CommRing A] [Algebra R A], Function.Bijective (kerMapBaseChange G.d d ι0
    ι1 comm A))
include hG in

Lean source · statement

theorem bijective_kerMap_self : Function.Bijective (kerMap G.d d ι0 ι1 comm)

def

kerEquiv

L87 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_projective_ker_of_isReduced_of_kerMapBaseChange_bijective.TwoChartCech.KerModel.kerEquiv

Documentation

The kernel equivalence induced by the given model comparison over the base ring.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_projective_ker_of_isReduced_of_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace KerModel
variable {R : Type u} [CommRing R] {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup
  C1]
  [Module R C1] {d : C0 →ₗ[R] C1}
  (G : CoherentBaseChange.TwoTermComplex.{u, u} R) (ι0 : G.C0 →ₗ[R] C0) (ι1 : G.C1 →ₗ[R] C1)
  (comm : d ∘ₗ ι0 = ι1 ∘ₗ G.d)
  (hG : ∀ (A : Type u) [CommRing A] [Algebra R A], Function.Bijective (kerMapBaseChange G.d d ι0
    ι1 comm A))

Lean source · statement

def kerEquiv : LinearMap.ker G.d ≃ₗ[R] LinearMap.ker d

theorem

square

L90 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_projective_ker_of_isReduced_of_kerMapBaseChange_bijective.TwoChartCech.KerModel.square

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_projective_ker_of_isReduced_of_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace KerModel
variable {R : Type u} [CommRing R] {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup
  C1]
  [Module R C1] {d : C0 →ₗ[R] C1}
  (G : CoherentBaseChange.TwoTermComplex.{u, u} R) (ι0 : G.C0 →ₗ[R] C0) (ι1 : G.C1 →ₗ[R] C1)
  (comm : d ∘ₗ ι0 = ι1 ∘ₗ G.d)
  (hG : ∀ (A : Type u) [CommRing A] [Algebra R A], Function.Bijective (kerMapBaseChange G.d d ι0
    ι1 comm A))

Lean source · statement

theorem square (A : Type u) [CommRing A] [Algebra R A] (x : A ⊗[R] LinearMap.ker G.d) :
    kerMapBaseChange G.d d ι0 ι1 comm A (G.kerBaseChangeHom A x)
      = kerBaseChangeHom d A ((kerMap G.d d ι0 ι1 comm).baseChange A x)

theorem

bijective_kerBaseChangeHom_iff

L100 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_projective_ker_of_isReduced_of_kerMapBaseChange_bijective.TwoChartCech.KerModel.bijective_kerBaseChangeHom_iff

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_projective_ker_of_isReduced_of_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace KerModel
variable {R : Type u} [CommRing R] {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup
  C1]
  [Module R C1] {d : C0 →ₗ[R] C1}
  (G : CoherentBaseChange.TwoTermComplex.{u, u} R) (ι0 : G.C0 →ₗ[R] C0) (ι1 : G.C1 →ₗ[R] C1)
  (comm : d ∘ₗ ι0 = ι1 ∘ₗ G.d)
  (hG : ∀ (A : Type u) [CommRing A] [Algebra R A], Function.Bijective (kerMapBaseChange G.d d ι0
    ι1 comm A))
include hG in

Lean source · statement

theorem bijective_kerBaseChangeHom_iff (A : Type u) [CommRing A] [Algebra R A] :
    Function.Bijective (kerBaseChangeHom d A) ↔ Function.Bijective (G.kerBaseChangeHom A)

theorem

fibreH0_eq

L120 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_projective_ker_of_isReduced_of_kerMapBaseChange_bijective.TwoChartCech.KerModel.fibreH0_eq

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_projective_ker_of_isReduced_of_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace KerModel
variable {R : Type u} [CommRing R] {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup
  C1]
  [Module R C1] {d : C0 →ₗ[R] C1}
  (G : CoherentBaseChange.TwoTermComplex.{u, u} R) (ι0 : G.C0 →ₗ[R] C0) (ι1 : G.C1 →ₗ[R] C1)
  (comm : d ∘ₗ ι0 = ι1 ∘ₗ G.d)
  (hG : ∀ (A : Type u) [CommRing A] [Algebra R A], Function.Bijective (kerMapBaseChange G.d d ι0
    ι1 comm A))
include hG in

Lean source · statement

theorem fibreH0_eq (𝔭 : PrimeSpectrum R) :
    G.fibreH0 𝔭 = Module.finrank 𝔭.asIdeal.ResidueField (LinearMap.ker (d.baseChange
      𝔭.asIdeal.ResidueField))

theorem

projective_ker_of_isReduced_of_kerMapBaseChange_bijective

L128 ↗

TwoChartCech.projective_ker_of_isReduced_of_kerMapBaseChange_bijective

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_projective_ker_of_isReduced_of_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u

Lean source · statement

theorem _root_.TwoChartCech.projective_ker_of_isReduced_of_kerMapBaseChange_bijective
    {R : Type u} [CommRing R] [IsReduced R] {C0 C1 : Type u} [AddCommGroup C0] [Module R C0]
    [AddCommGroup C1] [Module R C1] {d : C0 →ₗ[R] C1}
    (G : CoherentBaseChange.TwoTermComplex.{u, u} R) (ι0 : G.C0 →ₗ[R] C0) (ι1 : G.C1 →ₗ[R] C1)
    (comm : d ∘ₗ ι0 = ι1 ∘ₗ G.d)
    (hG : ∀ (A : Type u) [CommRing A] [Algebra R A],
      Function.Bijective (TwoChartCech.kerMapBaseChange G.d d ι0 ι1 comm A))
    {n : ℕ} (hH0 : ∀ 𝔭 : PrimeSpectrum R, Module.finrank 𝔭.asIdeal.ResidueField
      (LinearMap.ker (d.baseChange 𝔭.asIdeal.ResidueField)) = n) :
    Module.Projective R (LinearMap.ker d) ∧
      (∀ (A : Type u) [CommRing A] [Algebra R A], Function.Bijective
        (TwoChartCech.kerBaseChangeHom d A)) ∧
      ∀ 𝔭 : PrimeSpectrum R, Module.finrank 𝔭.asIdeal.ResidueField
          (𝔭.asIdeal.ResidueField ⊗[R] LinearMap.ker d) = n

Module documentation

Declarations