NYLL
Module

TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
33 declarations indexed from sourceView source ↗

Module documentation

Construct a two-chart Cech Grothendieck complex over a local ring.

Imports8
  • 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
Imported by3

Declarations

theorem

flat_prod

L45 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.flat_prod
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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

L67 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.flat_ker_of_surjective
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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

L95 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.rank
Documentation

The rank of a chosen finite free module surjecting onto the cokernel of the original differential.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.quot
Documentation

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

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.quot_surjective
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.lift
Documentation

A lift of the chosen cokernel generators to the codomain of the original differential.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.mkQ_comp_lift
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.surjective_coprod
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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

L125 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.K0
Documentation

The kernel of the surjection formed by the original differential and the chosen generator lift.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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

L128 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.dK
Documentation

The projection from the kernel of the combined surjection to its finite free summand.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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

L132 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.iota0
Documentation

The projection from the kernel of the combined surjection to the original source module.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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

L134 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.dK_apply
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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

L135 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.iota0_apply
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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

L137 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.comm
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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

L147 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.h0ToK0
Documentation

Embed the kernel of the original differential into the kernel of the combined surjection with zero finite-free component.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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

L158 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.kerEquiv
Documentation

Identify the kernel of the finite-free projection with the kernel of the original differential.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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

L177 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.finite_K0
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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

L185 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.flat_K0
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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

L189 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.free_K0
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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)
def

model

L195 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.model
Documentation

The finite free two-term complex constructed from the kernel of the combined surjection.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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 model [IsNoetherianRing R] [IsLocalRing R] [Module.Flat R C0] [Module.Flat R C1]
    [Module.Finite R (LinearMap.ker d)] : CoherentBaseChange.TwoTermComplex.{u, u} R
theorem

d_baseChange_comp_iota0_baseChange

L204 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.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.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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

L212 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.subtype_baseChange_injective
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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

L218 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.mem_range_subtype_baseChange
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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

L228 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.prodRight_apply_eq_baseChange
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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

L236 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.prodRight_subtype_baseChange
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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

L248 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.coprod_baseChange_apply
Source context 17 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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

L256 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.kerMap_injective
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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 [IsNoetherianRing R] [IsLocalRing R] [Module.Flat R C0]
    [Module.Finite R (LinearMap.ker d)] :
    Function.Injective (kerMapBaseChange (model d).d d (iota0 d) (-(lift d)) (comm d) A)
theorem

kerMap_surjective

L269 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.kerMap_surjective
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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_surjective [IsNoetherianRing R] [IsLocalRing R] [Module.Flat R C0]
    [Module.Finite R (LinearMap.ker d)] :
    Function.Surjective (kerMapBaseChange (model d).d d (iota0 d) (-(lift d)) (comm d) A)
theorem

cokerMap_surjective

L291 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.cokerMap_surjective
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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 cokerMap_surjective [IsNoetherianRing R] [IsLocalRing R] [Module.Flat R C0]
    [Module.Finite R (LinearMap.ker d)] :
    Function.Surjective (cokerMapBaseChange (model d).d d (iota0 d) (-(lift d)) (comm d) A)
theorem

cokerMap_injective

L309 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.cokerMap_injective
Source context 16 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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 cokerMap_injective [IsNoetherianRing R] [IsLocalRing R] [Module.Flat R C0]
    [Module.Finite R (LinearMap.ker d)] :
    Function.Injective (cokerMapBaseChange (model d).d d (iota0 d) (-(lift d)) (comm d) A)
def

grothendieckComplex

L341 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.Truncation.grothendieckComplex
Documentation

The finite free model whose comparison maps preserve kernel and cokernel under the given flat base changes.

Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
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 · full declaration
def grothendieckComplex [IsNoetherianRing R] [IsLocalRing R] [Module.Flat R C0] [Module.Flat R C1]
    [Module.Finite R (LinearMap.ker d)] : GrothendieckComplex d where
  G := model d
  ι0 := iota0 d
  ι1 := -(lift d)
  comm := comm d
  bijective_kerMap A _ _ := ⟨kerMap_injective d A, kerMap_surjective d A⟩
  bijective_cokerMap A _ _ := ⟨cokerMap_injective d A, cokerMap_surjective d A⟩
theorem

nonempty_of_isLocalRing'

L352 ↗
AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing.TwoChartCech.nonempty_of_isLocalRing'
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
noncomputable section
open scoped TensorProduct
universe u
namespace TwoChartCech
open _root_.TwoChartCech
open _root_.TwoChartCech
Lean source · statement
theorem nonempty_of_isLocalRing' {R : Type u} [CommRing R] [IsNoetherianRing R]
    [IsLocalRing 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)] :
    Nonempty (_root_.TwoChartCech.GrothendieckComplex d)
theorem

nonempty_of_isLocalRing

L361 ↗
TwoChartCech.GrothendieckComplex.nonempty_of_isLocalRing
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace TwoChartCech_GrothendieckComplex_nonempty_of_isLocalRing
noncomputable section
open scoped TensorProduct
universe u
Lean source · statement
theorem _root_.TwoChartCech.GrothendieckComplex.nonempty_of_isLocalRing {R : Type u} [CommRing
    R] [IsNoetherianRing R]
    [IsLocalRing 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)] :
    Nonempty (_root_.TwoChartCech.GrothendieckComplex d)

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