Module

TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.lean

Nyll.AlgebraicCurves.Cohomology.Cech.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective

44 declarations indexed from sourceView source ↗

Module documentation

Finite free two-term models for Cech kernels and their base changes. A lifted presentation of the cokernel yields a model inducing bijections on all kernels.

Imports9

Nyll.SchemeTheory.Cohomology.Cech.TwoChartCech
Mathlib.RingTheory.Flat.Basic
Mathlib.RingTheory.Flat.Equalizer
Mathlib.RingTheory.LocalRing.Module
Mathlib.RingTheory.Noetherian.Basic
Mathlib.LinearAlgebra.TensorProduct.Prod
Mathlib.LinearAlgebra.TensorProduct.RightExactness
Mathlib.Algebra.Module.Projective
Mathlib.Algebra.Module.FinitePresentation

Imported by3

theorem

flat_prod

L47 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.flat_prod

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]

Lean source · statement

theorem flat_prod {M N : Type u} [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
    [Module.Flat R M] [Module.Flat R N] : Module.Flat R (M × N)

theorem

flat_ker_of_surjective

L69 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.flat_ker_of_surjective

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]

Lean source · statement

theorem flat_ker_of_surjective {M N : Type u} [AddCommGroup M] [Module R M]
    [AddCommGroup N] [Module R N] [Module.Flat R M] [Module.Flat R N]
    (f : M →ₗ[R] N) (hf : Function.Surjective f) :
    Module.Flat R (LinearMap.ker f)

def

rank

L96 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.rank

Documentation

The chosen number of free generators of the cokernel of the differential.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]

Lean source · statement

def rank : ℕ

def

quot

L99 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.quot

Documentation

The chosen surjection from a finite free module onto the cokernel.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]

Lean source · statement

def quot : (Fin (rank d) → R) →ₗ[R] (C1 ⧸ LinearMap.range d)

theorem

quot_surjective

L102 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.quot_surjective

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]

Lean source · statement

theorem quot_surjective : Function.Surjective (quot d)

def

lift

L106 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.lift

Documentation

The chosen lift of the cokernel presentation into the target of the differential.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]

Lean source · statement

def lift : (Fin (rank d) → R) →ₗ[R] C1

theorem

mkQ_comp_lift

L110 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.mkQ_comp_lift

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]

Lean source · statement

theorem mkQ_comp_lift : (LinearMap.range d).mkQ ∘ₗ lift d = quot d

theorem

surjective_coprod

L114 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.surjective_coprod

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]

Lean source · statement

theorem surjective_coprod : Function.Surjective (d.coprod (lift d))

abbrev

K0

L124 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.K0

Documentation

The kernel of the differential enlarged by the chosen cokernel lift.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]

Lean source · statement

abbrev K0 : Submodule R (C0 × (Fin (rank d) → R))

def

dK

L127 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.dK

Documentation

Project the enlarged kernel onto its finite free presentation factor.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]

Lean source · statement

def dK : K0 d →ₗ[R] (Fin (rank d) → R)

def

iota0

L131 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.iota0

Documentation

Project the enlarged kernel onto the source of the original differential.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]

Lean source · statement

def iota0 : K0 d →ₗ[R] C0

theorem

dK_apply

L133 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.dK_apply

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]

Lean source · statement

theorem dK_apply (z : K0 d) : dK d z = (z : C0 × (Fin (rank d) → R)).2

theorem

iota0_apply

L134 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.iota0_apply

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]

Lean source · statement

theorem iota0_apply (z : K0 d) : iota0 d z = (z : C0 × (Fin (rank d) → R)).1

theorem

comm

L136 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.comm

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]

Lean source · statement

theorem comm : d ∘ₗ iota0 d = (-(lift d)) ∘ₗ dK d

def

h0ToK0

L145 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.h0ToK0

Documentation

Embed the original kernel into the enlarged kernel with zero presentation coordinate.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]

Lean source · statement

def h0ToK0 : LinearMap.ker d →ₗ[R] K0 d

def

kerEquiv

L155 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.kerEquiv

Documentation

Identify the kernel of the presentation projection with the original kernel.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]

Lean source · statement

def kerEquiv : LinearMap.ker (dK d) ≃ₗ[R] LinearMap.ker d

theorem

finite_K0

L174 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.finite_K0

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]

Lean source · statement

theorem finite_K0 [IsNoetherianRing R] [Module.Finite R (LinearMap.ker d)] : Module.Finite R (K0
    d)

theorem

flat_K0

L182 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.flat_K0

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]

Lean source · statement

theorem flat_K0 [Module.Flat R C0] [Module.Flat R C1] : Module.Flat R (K0 d)

theorem

free_K0

L186 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.free_K0

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]

Lean source · statement

theorem free_K0 [IsNoetherianRing R] [IsLocalRing R] [Module.Flat R C0] [Module.Flat R C1]
    [Module.Finite R (LinearMap.ker d)] : Module.Free R (K0 d)

theorem

d_baseChange_comp_iota0_baseChange

L195 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.d_baseChange_comp_iota0_baseChange

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
section BaseChange
variable (A : Type u) [CommRing A] [Algebra R A]

Lean source · statement

theorem d_baseChange_comp_iota0_baseChange :
    (d.baseChange A) ∘ₗ ((iota0 d).baseChange A)
      = -(((lift d).baseChange A) ∘ₗ ((dK d).baseChange A))

theorem

subtype_baseChange_injective

L203 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.subtype_baseChange_injective

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
section BaseChange
variable (A : Type u) [CommRing A] [Algebra R A]
variable [Module.Flat R C1]

Lean source · statement

theorem subtype_baseChange_injective :
    Function.Injective ((K0 d).subtype.baseChange A)

theorem

mem_range_subtype_baseChange

L209 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.mem_range_subtype_baseChange

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
section BaseChange
variable (A : Type u) [CommRing A] [Algebra R A]
variable [Module.Flat R C1]
omit [Module.Flat R C1] in

Lean source · statement

theorem mem_range_subtype_baseChange (w : A ⊗[R] (C0 × (Fin (rank d) → R))) :
    ((d.coprod (lift d)).baseChange A) w = 0 ↔ ∃ z, ((K0 d).subtype.baseChange A) z = w

theorem

prodRight_apply_eq_baseChange

L219 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.prodRight_apply_eq_baseChange

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
section BaseChange
variable (A : Type u) [CommRing A] [Algebra R A]
variable [Module.Flat R C1]
omit [Module.Flat R C1] in

Lean source · statement

theorem prodRight_apply_eq_baseChange {M N : Type u} [AddCommGroup M] [Module R M]
    [AddCommGroup N] [Module R N] (w : A ⊗[R] (M × N)) :
    (TensorProduct.prodRight R A A M N) w
      = (((LinearMap.fst R M N).baseChange A) w, ((LinearMap.snd R M N).baseChange A) w)

theorem

prodRight_subtype_baseChange

L227 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.prodRight_subtype_baseChange

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
section BaseChange
variable (A : Type u) [CommRing A] [Algebra R A]
variable [Module.Flat R C1]
omit [Module.Flat R C1] in

Lean source · statement

theorem prodRight_subtype_baseChange (z : A ⊗[R] K0 d) :
    (TensorProduct.prodRight R A A C0 (Fin (rank d) → R)) (((K0 d).subtype.baseChange A) z)
      = (((iota0 d).baseChange A) z, ((dK d).baseChange A) z)

theorem

coprod_baseChange_apply

L239 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.coprod_baseChange_apply

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
section BaseChange
variable (A : Type u) [CommRing A] [Algebra R A]
variable [Module.Flat R C1]
omit [Module.Flat R C1] in

Lean source · statement

theorem coprod_baseChange_apply (w : A ⊗[R] (C0 × (Fin (rank d) → R))) :
    ((d.coprod (lift d)).baseChange A) w
      = (d.baseChange A) ((TensorProduct.prodRight R A A C0 (Fin (rank d) → R)) w).1
        + ((lift d).baseChange A) ((TensorProduct.prodRight R A A C0 (Fin (rank d) → R)) w).2

theorem

kerMap_injective'

L247 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.kerMap_injective'

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
section BaseChange
variable (A : Type u) [CommRing A] [Algebra R A]
variable [Module.Flat R C1]

Lean source · statement

theorem kerMap_injective' [Module.Flat R C0] :
    Function.Injective (kerMapBaseChange (dK d) d (iota0 d) (-(lift d)) (comm d) A)

theorem

kerMap_surjective'

L259 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.kerMap_surjective'

Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
section BaseChange
variable (A : Type u) [CommRing A] [Algebra R A]
variable [Module.Flat R C1]
omit [Module.Flat R C1] in

Lean source · statement

theorem kerMap_surjective' [Module.Flat R C0] :
    Function.Surjective (kerMapBaseChange (dK d) d (iota0 d) (-(lift d)) (comm d) A)

theorem

projective_K0

L287 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.projective_K0

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
section Free
variable [IsNoetherianRing R] [Module.Flat R C0] [Module.Flat R C1] [Module.Finite R
  (LinearMap.ker d)]

Lean source · statement

theorem projective_K0 : Module.Projective R (K0 d)

def

n

L293 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.n

Documentation

The chosen number of free generators of the enlarged kernel.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
section Free
variable [IsNoetherianRing R] [Module.Flat R C0] [Module.Flat R C1] [Module.Finite R
  (LinearMap.ker d)]

Lean source · statement

def n : ℕ

def

pi

L296 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.pi

Documentation

The chosen finite free surjection onto the enlarged kernel.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
section Free
variable [IsNoetherianRing R] [Module.Flat R C0] [Module.Flat R C1] [Module.Finite R
  (LinearMap.ker d)]

Lean source · statement

def pi : (Fin (n d) → R) →ₗ[R] K0 d

theorem

pi_surjective

L299 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.pi_surjective

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
section Free
variable [IsNoetherianRing R] [Module.Flat R C0] [Module.Flat R C1] [Module.Finite R
  (LinearMap.ker d)]
omit [Module.Flat R C0] [Module.Flat R C1] in

Lean source · statement

theorem pi_surjective : Function.Surjective (pi d)

def

sec

L303 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.sec

Documentation

The chosen section of the finite free surjection onto the enlarged kernel.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
section Free
variable [IsNoetherianRing R] [Module.Flat R C0] [Module.Flat R C1] [Module.Finite R
  (LinearMap.ker d)]

Lean source · statement

def sec : K0 d →ₗ[R] (Fin (n d) → R)

theorem

pi_comp_sec

L306 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.pi_comp_sec

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
section Free
variable [IsNoetherianRing R] [Module.Flat R C0] [Module.Flat R C1] [Module.Finite R
  (LinearMap.ker d)]

Lean source · statement

theorem pi_comp_sec : pi d ∘ₗ sec d = LinearMap.id

theorem

pi_sec

L309 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.pi_sec

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
section Free
variable [IsNoetherianRing R] [Module.Flat R C0] [Module.Flat R C1] [Module.Finite R
  (LinearMap.ker d)]

Lean source · statement

theorem pi_sec (k : K0 d) : pi d (sec d k) = k

def

dG

L313 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.dG

Documentation

The differential recording the presentation projection and its splitting complement.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
section Free
variable [IsNoetherianRing R] [Module.Flat R C0] [Module.Flat R C1] [Module.Finite R
  (LinearMap.ker d)]

Lean source · statement

def dG : (Fin (n d) → R) →ₗ[R] (Fin (rank d) → R) × (Fin (n d) → R)

theorem

fst_comp_dG

L316 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.fst_comp_dG

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
section Free
variable [IsNoetherianRing R] [Module.Flat R C0] [Module.Flat R C1] [Module.Finite R
  (LinearMap.ker d)]

Lean source · statement

theorem fst_comp_dG : LinearMap.fst R _ _ ∘ₗ dG d = dK d ∘ₗ pi d

theorem

snd_comp_dG

L317 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.snd_comp_dG

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
section Free
variable [IsNoetherianRing R] [Module.Flat R C0] [Module.Flat R C1] [Module.Finite R
  (LinearMap.ker d)]

Lean source · statement

theorem snd_comp_dG : LinearMap.snd R _ _ ∘ₗ dG d = LinearMap.id - sec d ∘ₗ pi d

def

freeModel

L321 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.freeModel

Documentation

The finite free two-term complex constructed from the split presentation.

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
section Free
variable [IsNoetherianRing R] [Module.Flat R C0] [Module.Flat R C1] [Module.Finite R
  (LinearMap.ker d)]

Lean source · statement

def freeModel : CoherentBaseChange.TwoTermComplex.{u, u} R

theorem

comm_free

L324 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.comm_free

Source context 15 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
section Free
variable [IsNoetherianRing R] [Module.Flat R C0] [Module.Flat R C1] [Module.Finite R
  (LinearMap.ker d)]

Lean source · statement

theorem comm_free : d ∘ₗ (iota0 d ∘ₗ pi d) = ((-(lift d)) ∘ₗ LinearMap.fst R _ _) ∘ₗ dG d

theorem

mem_ker_dG_baseChange_iff

L329 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.mem_ker_dG_baseChange_iff

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
section Free
variable [IsNoetherianRing R] [Module.Flat R C0] [Module.Flat R C1] [Module.Finite R
  (LinearMap.ker d)]
variable (A : Type u) [CommRing A] [Algebra R A]

Lean source · statement

theorem mem_ker_dG_baseChange_iff (z : A ⊗[R] (Fin (n d) → R)) :
    (dG d).baseChange A z = 0 ↔
      ((dK d).baseChange A) (((pi d).baseChange A) z) = 0 ∧ z = ((sec d).baseChange A) (((pi
        d).baseChange A) z)

theorem

bijective_kerMap_free_to_K

L356 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.bijective_kerMap_free_to_K

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
section Free
variable [IsNoetherianRing R] [Module.Flat R C0] [Module.Flat R C1] [Module.Finite R
  (LinearMap.ker d)]
variable (A : Type u) [CommRing A] [Algebra R A]

Lean source · statement

theorem bijective_kerMap_free_to_K :
    Function.Bijective (kerMapBaseChange (dG d) (dK d) (pi d) (LinearMap.fst R _ _) (fst_comp_dG
      d).symm A)

theorem

kerMap_free_eq_comp

L382 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.kerMap_free_eq_comp

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
section Free
variable [IsNoetherianRing R] [Module.Flat R C0] [Module.Flat R C1] [Module.Finite R
  (LinearMap.ker d)]
variable (A : Type u) [CommRing A] [Algebra R A]

Lean source · statement

theorem kerMap_free_eq_comp (z : LinearMap.ker ((dG d).baseChange A)) :
    kerMapBaseChange (dG d) d (iota0 d ∘ₗ pi d) ((-(lift d)) ∘ₗ LinearMap.fst R _ _) (comm_free d)
      A z
      = kerMapBaseChange (dK d) d (iota0 d) (-(lift d)) (comm d) A
          (kerMapBaseChange (dG d) (dK d) (pi d) (LinearMap.fst R _ _) (fst_comp_dG d).symm A z)

theorem

bijective_kerMap_free

L392 ↗

AlgebraicCurves.Cohomology.Cech.Proofs.TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective.TwoChartCech.Truncation.bijective_kerMap_free

Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Cohomology.Cech.Proofs
namespace TwoChartCech_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
namespace Truncation
variable {R : Type u} [CommRing R]
variable {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
variable (d : C0 →ₗ[R] C1) [Module.Finite R (C1 ⧸ LinearMap.range d)]
section Free
variable [IsNoetherianRing R] [Module.Flat R C0] [Module.Flat R C1] [Module.Finite R
  (LinearMap.ker d)]
variable (A : Type u) [CommRing A] [Algebra R A]

Lean source · statement

theorem bijective_kerMap_free :
    Function.Bijective
      (kerMapBaseChange (dG d) d (iota0 d ∘ₗ pi d) ((-(lift d)) ∘ₗ LinearMap.fst R _ _) (comm_free
        d) A)

theorem

exists_twoTermComplex_kerMapBaseChange_bijective

L411 ↗

TwoChartCech.exists_twoTermComplex_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_exists_twoTermComplex_kerMapBaseChange_bijective
noncomputable section
open scoped TensorProduct
universe u

Lean source · statement

theorem _root_.TwoChartCech.exists_twoTermComplex_kerMapBaseChange_bijective
    {R : Type u} [CommRing R] [IsNoetherianRing R]
    {C0 C1 : Type u} [AddCommGroup C0] [Module R C0] [AddCommGroup C1] [Module R C1]
    [Module.Flat R C0] [Module.Flat R C1] (d : C0 →ₗ[R] C1)
    [Module.Finite R (LinearMap.ker d)] [Module.Finite R (C1 ⧸ LinearMap.range d)] :
    ∃ (G : CoherentBaseChange.TwoTermComplex.{u, u} R) (ι0 : G.C0 →ₗ[R] C0) (ι1 : G.C1 →ₗ[R] C1)
      (comm : d ∘ₗ ι0 = ι1 ∘ₗ G.d),
      ∀ (A : Type u) [CommRing A] [Algebra R A],
        Function.Bijective (TwoChartCech.kerMapBaseChange G.d d ι0 ι1 comm A)

Module documentation

Declarations