Module

Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.lean

Nyll.AlgebraicCurves.Foundations.HomologicalAlgebra.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex

37 declarations indexed from sourceView source ↗

Module documentation

Module exists two Term Complex ker Map Base Change bijective of flat complex

Imports6

Nyll.SchemeTheory.Cohomology.Cech.TwoChartCech
Mathlib.RingTheory.Flat.Basic
Mathlib.LinearAlgebra.TensorProduct.Prod
Mathlib.RingTheory.Flat.Equalizer
Mathlib.RingTheory.Flat.EquationalCriterion
Mathlib.Algebra.Module.FinitePresentation

Imported by2

theorem

flat_prod

L39 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.flat_prod

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Generalities
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

L63 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.flat_ker_of_surjective

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Generalities
variable {R : Type u} [CommRing R]

Lean source · statement

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

theorem

eq_zero_of_fst_snd_baseChange

L85 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.eq_zero_of_fst_snd_baseChange

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Generalities
variable {R : Type u} [CommRing R]
variable {A : Type u} [CommRing A] [Algebra R A]

Lean source · statement

theorem eq_zero_of_fst_snd_baseChange {M N : Type u} [AddCommGroup M] [Module R M]
    [AddCommGroup N] [Module R N] (z : A ⊗[R] (M × N))
    (h1 : (LinearMap.fst R M N).baseChange A z = 0)
    (h2 : (LinearMap.snd R M N).baseChange A z = 0) : z = 0

theorem

inl_baseChange_injective

L100 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.inl_baseChange_injective

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Generalities
variable {R : Type u} [CommRing R]
variable {A : Type u} [CommRing A] [Algebra R A]

Lean source · statement

theorem inl_baseChange_injective (M N : Type u) [AddCommGroup M] [Module R M]
    [AddCommGroup N] [Module R N] :
    Function.Injective ((LinearMap.inl R M N).baseChange A)

theorem

ker_baseChange_comp_eq

L107 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.ker_baseChange_comp_eq

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Generalities
variable {R : Type u} [CommRing R]
variable {A : Type u} [CommRing A] [Algebra R A]

Lean source · statement

theorem ker_baseChange_comp_eq {M N P : Type u} [AddCommGroup M] [Module R M]
    [AddCommGroup N] [Module R N] [AddCommGroup P] [Module R P]
    (f : M →ₗ[R] N) (g : N →ₗ[R] P) (hg : Function.Injective (g.baseChange A)) :
    LinearMap.ker ((g ∘ₗ f).baseChange A) = LinearMap.ker (f.baseChange A)

theorem

subtype_baseChange_injective

L114 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.subtype_baseChange_injective

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Generalities
variable {R : Type u} [CommRing R]
variable {A : Type u} [CommRing A] [Algebra R A]

Lean source · statement

theorem subtype_baseChange_injective {M K : Type u} [AddCommGroup M] [Module R M]
    [AddCommGroup K] [Module R K] [Module.Flat R K] (σ : M →ₗ[R] K)
    (hσ : Function.Surjective σ) :
    Function.Injective ((LinearMap.ker σ).subtype.baseChange A)

theorem

subtype_baseChange_exact

L122 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.subtype_baseChange_exact

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Generalities
variable {R : Type u} [CommRing R]
variable {A : Type u} [CommRing A] [Algebra R A]

Lean source · statement

theorem subtype_baseChange_exact {M K : Type u} [AddCommGroup M] [Module R M]
    [AddCommGroup K] [Module R K] (σ : M →ₗ[R] K) (hσ : Function.Surjective σ) :
    Function.Exact ((LinearMap.ker σ).subtype.baseChange A) (σ.baseChange A)

theorem

exists_coprod_surjective

L129 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.exists_coprod_surjective

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Generalities
variable {R : Type u} [CommRing R]
variable {A : Type u} [CommRing A] [Algebra R A]
omit [Algebra R A] in

Lean source · statement

theorem exists_coprod_surjective {M K : Type u} [AddCommGroup M] [Module R M]
    [AddCommGroup K] [Module R K] (e : M →ₗ[R] K)
    [Module.Finite R (K ⧸ LinearMap.range e)] :
    ∃ (m : ℕ) (g : (Fin m → R) →ₗ[R] K), Function.Surjective (e.coprod g)

abbrev

Kx

L155 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.Kx

Documentation

The kernel of the sum map from the module and a finite free module.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Ext
variable {R : Type u} [CommRing R]
variable {M K : Type u} [AddCommGroup M] [Module R M] [AddCommGroup K] [Module R K]
variable (e : M →ₗ[R] K) {m : ℕ} (g : (Fin m → R) →ₗ[R] K)

Lean source · statement

abbrev Kx : Submodule R (M × (Fin m → R))

theorem

mem_Kx_iff

L157 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.mem_Kx_iff

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Ext
variable {R : Type u} [CommRing R]
variable {M K : Type u} [AddCommGroup M] [Module R M] [AddCommGroup K] [Module R K]
variable (e : M →ₗ[R] K) {m : ℕ} (g : (Fin m → R) →ₗ[R] K)

Lean source · statement

theorem mem_Kx_iff (x : M × (Fin m → R)) : x ∈ Kx e g ↔ e x.1 + g x.2 = 0

theorem

inl_mem_Kx_iff

L160 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.inl_mem_Kx_iff

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Ext
variable {R : Type u} [CommRing R]
variable {M K : Type u} [AddCommGroup M] [Module R M] [AddCommGroup K] [Module R K]
variable (e : M →ₗ[R] K) {m : ℕ} (g : (Fin m → R) →ₗ[R] K)

Lean source · statement

theorem inl_mem_Kx_iff (c : M) : LinearMap.inl R M (Fin m → R) c ∈ Kx e g ↔ e c = 0

def

φ₀

L164 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.φ₀

Documentation

The projection from the kernel of the sum map to its module coordinate.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Ext
variable {R : Type u} [CommRing R]
variable {M K : Type u} [AddCommGroup M] [Module R M] [AddCommGroup K] [Module R K]
variable (e : M →ₗ[R] K) {m : ℕ} (g : (Fin m → R) →ₗ[R] K)

Lean source · statement

def φ₀ : Kx e g →ₗ[R] M

def

δ

L167 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.δ

Documentation

The projection from the kernel of the sum map to its finite free coordinate.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Ext
variable {R : Type u} [CommRing R]
variable {M K : Type u} [AddCommGroup M] [Module R M] [AddCommGroup K] [Module R K]
variable (e : M →ₗ[R] K) {m : ℕ} (g : (Fin m → R) →ₗ[R] K)

Lean source · statement

def δ : Kx e g →ₗ[R] (Fin m → R)

theorem

φ₀_apply

L169 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.φ₀_apply

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Ext
variable {R : Type u} [CommRing R]
variable {M K : Type u} [AddCommGroup M] [Module R M] [AddCommGroup K] [Module R K]
variable (e : M →ₗ[R] K) {m : ℕ} (g : (Fin m → R) →ₗ[R] K)

Lean source · statement

theorem φ₀_apply (k : Kx e g) : φ₀ e g k = (k : M × (Fin m → R)).1

theorem

δ_apply

L170 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.δ_apply

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Ext
variable {R : Type u} [CommRing R]
variable {M K : Type u} [AddCommGroup M] [Module R M] [AddCommGroup K] [Module R K]
variable (e : M →ₗ[R] K) {m : ℕ} (g : (Fin m → R) →ₗ[R] K)

Lean source · statement

theorem δ_apply (k : Kx e g) : δ e g k = (k : M × (Fin m → R)).2

theorem

e_comp_φ₀

L172 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.e_comp_φ₀

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Ext
variable {R : Type u} [CommRing R]
variable {M K : Type u} [AddCommGroup M] [Module R M] [AddCommGroup K] [Module R K]
variable (e : M →ₗ[R] K) {m : ℕ} (g : (Fin m → R) →ₗ[R] K)

Lean source · statement

theorem e_comp_φ₀ : e ∘ₗ φ₀ e g = (-g) ∘ₗ δ e g

theorem

flat_Kx

L178 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.flat_Kx

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Ext
variable {R : Type u} [CommRing R]
variable {M K : Type u} [AddCommGroup M] [Module R M] [AddCommGroup K] [Module R K]
variable (e : M →ₗ[R] K) {m : ℕ} (g : (Fin m → R) →ₗ[R] K)

Lean source · statement

theorem flat_Kx [Module.Flat R M] [Module.Flat R K] (hσ : Function.Surjective (e.coprod g)) :
    Module.Flat R (Kx e g)

theorem

Kx_inf_ker_snd

L183 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.Kx_inf_ker_snd

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Ext
variable {R : Type u} [CommRing R]
variable {M K : Type u} [AddCommGroup M] [Module R M] [AddCommGroup K] [Module R K]
variable (e : M →ₗ[R] K) {m : ℕ} (g : (Fin m → R) →ₗ[R] K)

Lean source · statement

theorem Kx_inf_ker_snd :
    Kx e g ⊓ LinearMap.ker (LinearMap.snd R M (Fin m → R)) =
      (LinearMap.ker e).map (LinearMap.inl R M (Fin m → R))

theorem

fg_Kx

L199 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.fg_Kx

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Ext
variable {R : Type u} [CommRing R]
variable {M K : Type u} [AddCommGroup M] [Module R M] [AddCommGroup K] [Module R K]
variable (e : M →ₗ[R] K) {m : ℕ} (g : (Fin m → R) →ₗ[R] K)

Lean source · statement

theorem fg_Kx [IsNoetherianRing R] (hfin : Module.Finite R (LinearMap.ker e)) : (Kx e g).FG

theorem

eq_zero_of_δ_φ₀

L207 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.eq_zero_of_δ_φ₀

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Ext
variable {R : Type u} [CommRing R]
variable {M K : Type u} [AddCommGroup M] [Module R M] [AddCommGroup K] [Module R K]
variable (e : M →ₗ[R] K) {m : ℕ} (g : (Fin m → R) →ₗ[R] K)
variable {A : Type u} [CommRing A] [Algebra R A]

Lean source · statement

theorem eq_zero_of_δ_φ₀ [Module.Flat R K] (hσ : Function.Surjective (e.coprod g))
    (x : A ⊗[R] Kx e g) (hδ : (δ e g).baseChange A x = 0) (hφ : (φ₀ e g).baseChange A x = 0) :
    x = 0

theorem

exists_of_baseChange_eq_zero

L218 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.exists_of_baseChange_eq_zero

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Ext
variable {R : Type u} [CommRing R]
variable {M K : Type u} [AddCommGroup M] [Module R M] [AddCommGroup K] [Module R K]
variable (e : M →ₗ[R] K) {m : ℕ} (g : (Fin m → R) →ₗ[R] K)
variable {A : Type u} [CommRing A] [Algebra R A]

Lean source · statement

theorem exists_of_baseChange_eq_zero (hσ : Function.Surjective (e.coprod g))
    (y : A ⊗[R] M) (hy : e.baseChange A y = 0) :
    ∃ x : A ⊗[R] Kx e g, (δ e g).baseChange A x = 0 ∧ (φ₀ e g).baseChange A x = y

def

e'

L237 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.e'

Documentation

Lift the preceding differential into the kernel of the sum map.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Ext
variable {R : Type u} [CommRing R]
variable {M K : Type u} [AddCommGroup M] [Module R M] [AddCommGroup K] [Module R K]
variable (e : M →ₗ[R] K) {m : ℕ} (g : (Fin m → R) →ₗ[R] K)
variable {A : Type u} [CommRing A] [Algebra R A]
variable {M₀ : Type u} [AddCommGroup M₀] [Module R M₀] (d₀ : M₀ →ₗ[R] M) (hed : ∀ x, e (d₀ x) = 0)

Lean source · statement

def e' : M₀ →ₗ[R] Kx e g

theorem

e'_val

L241 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.e'_val

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Ext
variable {R : Type u} [CommRing R]
variable {M K : Type u} [AddCommGroup M] [Module R M] [AddCommGroup K] [Module R K]
variable (e : M →ₗ[R] K) {m : ℕ} (g : (Fin m → R) →ₗ[R] K)
variable {A : Type u} [CommRing A] [Algebra R A]
variable {M₀ : Type u} [AddCommGroup M₀] [Module R M₀] (d₀ : M₀ →ₗ[R] M) (hed : ∀ x, e (d₀ x) = 0)

Lean source · statement

theorem e'_val (x : M₀) : ((e' e g d₀ hed x : Kx e g) : M × (Fin m → R)) = (d₀ x, 0)

theorem

subtype_comp_e'

L243 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.subtype_comp_e'

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Ext
variable {R : Type u} [CommRing R]
variable {M K : Type u} [AddCommGroup M] [Module R M] [AddCommGroup K] [Module R K]
variable (e : M →ₗ[R] K) {m : ℕ} (g : (Fin m → R) →ₗ[R] K)
variable {A : Type u} [CommRing A] [Algebra R A]
variable {M₀ : Type u} [AddCommGroup M₀] [Module R M₀] (d₀ : M₀ →ₗ[R] M) (hed : ∀ x, e (d₀ x) = 0)

Lean source · statement

theorem subtype_comp_e' : (Kx e g).subtype ∘ₗ e' e g d₀ hed = LinearMap.inl R M (Fin m → R) ∘ₗ d₀

theorem

φ₀_comp_e'

L246 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.φ₀_comp_e'

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Ext
variable {R : Type u} [CommRing R]
variable {M K : Type u} [AddCommGroup M] [Module R M] [AddCommGroup K] [Module R K]
variable (e : M →ₗ[R] K) {m : ℕ} (g : (Fin m → R) →ₗ[R] K)
variable {A : Type u} [CommRing A] [Algebra R A]
variable {M₀ : Type u} [AddCommGroup M₀] [Module R M₀] (d₀ : M₀ →ₗ[R] M) (hed : ∀ x, e (d₀ x) = 0)

Lean source · statement

theorem φ₀_comp_e' : φ₀ e g ∘ₗ e' e g d₀ hed = d₀

theorem

ker_e'

L250 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.ker_e'

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Ext
variable {R : Type u} [CommRing R]
variable {M K : Type u} [AddCommGroup M] [Module R M] [AddCommGroup K] [Module R K]
variable (e : M →ₗ[R] K) {m : ℕ} (g : (Fin m → R) →ₗ[R] K)
variable {A : Type u} [CommRing A] [Algebra R A]
variable {M₀ : Type u} [AddCommGroup M₀] [Module R M₀] (d₀ : M₀ →ₗ[R] M) (hed : ∀ x, e (d₀ x) = 0)

Lean source · statement

theorem ker_e' : LinearMap.ker (e' e g d₀ hed) = LinearMap.ker d₀

theorem

ker_baseChange_e'

L262 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.ker_baseChange_e'

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Ext
variable {R : Type u} [CommRing R]
variable {M K : Type u} [AddCommGroup M] [Module R M] [AddCommGroup K] [Module R K]
variable (e : M →ₗ[R] K) {m : ℕ} (g : (Fin m → R) →ₗ[R] K)
variable {A : Type u} [CommRing A] [Algebra R A]
variable {M₀ : Type u} [AddCommGroup M₀] [Module R M₀] (d₀ : M₀ →ₗ[R] M) (hed : ∀ x, e (d₀ x) = 0)

Lean source · statement

theorem ker_baseChange_e' [Module.Flat R K] (hσ : Function.Surjective (e.coprod g)) :
    LinearMap.ker ((e' e g d₀ hed).baseChange A) = LinearMap.ker (d₀.baseChange A)

theorem

finite_coker_e'

L271 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.finite_coker_e'

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Ext
variable {R : Type u} [CommRing R]
variable {M K : Type u} [AddCommGroup M] [Module R M] [AddCommGroup K] [Module R K]
variable (e : M →ₗ[R] K) {m : ℕ} (g : (Fin m → R) →ₗ[R] K)
variable {A : Type u} [CommRing A] [Algebra R A]
variable {M₀ : Type u} [AddCommGroup M₀] [Module R M₀] (d₀ : M₀ →ₗ[R] M) (hed : ∀ x, e (d₀ x) = 0)

Lean source · statement

theorem finite_coker_e' [IsNoetherianRing R] (N : Submodule R M) (hN : LinearMap.ker e = N)
    (hfin : Module.Finite R (N ⧸ (LinearMap.range d₀).comap N.subtype)) :
    Module.Finite R (Kx e g ⧸ LinearMap.range (e' e g d₀ hed))

structure

Trunc

L337 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.Trunc

Documentation

A flat replacement for a complex tail that preserves kernels under algebra base change.

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Truncation
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  [∀ i, Module.Flat R (C i)]
variable (d : ∀ i, C i →ₗ[R] C (i + 1))

Lean source · full declaration

structure Trunc (p : ℕ) : Type (u + 1) where
  /-- The carrier of the replacement module. -/
  K : Type u
  /-- The additive commutative group structure on the replacement module. -/
  [acg : AddCommGroup K]
  /-- The base-ring module structure on the replacement module. -/
  [mod : Module R K]
  /-- The replacement module is flat. -/
  [flat : Module.Flat R K]
  /-- The map from the current complex term to the replacement module. -/
  e : C p →ₗ[R] K
  /-- The map from the replacement module to the next complex term. -/
  ι : K →ₗ[R] C (p + 1)
  /-- The two maps compose to the original differential. -/
  ι_comp : ι ∘ₗ e = d p
  /-- The replacement map has the same kernel as the original differential. -/
  ker_eq : LinearMap.ker e = LinearMap.ker (d p)
  /-- The equality of kernels persists after every algebra base change. -/
  ker_bc : ∀ (A : Type u) [CommRing A] [Algebra R A],
    LinearMap.ker (e.baseChange A) = LinearMap.ker ((d p).baseChange A)
  /-- The cokernel of the replacement map is finitely generated. -/
  fin : Module.Finite R (K ⧸ LinearMap.range e)

def

truncBase

L364 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.truncBase

Documentation

The terminal truncation when the following complex term is subsingleton.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Truncation
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  [∀ i, Module.Flat R (C i)]
variable (d : ∀ i, C i →ₗ[R] C (i + 1))
attribute [scoped instance] Trunc.acg Trunc.mod Trunc.flat
variable {d}

Lean source · full declaration

def truncBase (p : ℕ) [Subsingleton (C (p + 1))] : Trunc d p where
  K := C (p + 1)
  e := d p
  ι := LinearMap.id
  ι_comp := LinearMap.id_comp _
  ker_eq := rfl
  ker_bc _ _ _ := rfl
  fin := inferInstance

theorem

truncStep

L373 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.truncStep

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Truncation
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  [∀ i, Module.Flat R (C i)]
variable (d : ∀ i, C i →ₗ[R] C (i + 1))
attribute [scoped instance] Trunc.acg Trunc.mod Trunc.flat
variable {d}

Lean source · statement

theorem truncStep (p : ℕ) (hdd : d (p + 1) ∘ₗ d p = 0)
    (hfin : Module.Finite R (LinearMap.ker (d (p + 1)) ⧸
      (LinearMap.range (d p)).comap (LinearMap.ker (d (p + 1))).subtype))
    (T : Trunc d (p + 1)) : Nonempty (Trunc d p)

theorem

trunc_all

L394 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.trunc_all

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Truncation
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  [∀ i, Module.Flat R (C i)]
variable (d : ∀ i, C i →ₗ[R] C (i + 1))
attribute [scoped instance] Trunc.acg Trunc.mod Trunc.flat
variable {d}

Lean source · statement

theorem trunc_all (hdd : ∀ i, d (i + 1) ∘ₗ d i = 0) (n : ℕ) (hbdd : ∀ i, n < i → Subsingleton (C i))
    (hfin : ∀ i, Module.Finite R
      (LinearMap.ker (d (i + 1)) ⧸ (LinearMap.range (d i)).comap (LinearMap.ker (d (i +
        1))).subtype)) :
    ∀ j p : ℕ, n ≤ p + j → Nonempty (Trunc d p)

theorem

exists_trunc_zero

L413 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.exists_trunc_zero

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Truncation
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  [∀ i, Module.Flat R (C i)]
variable (d : ∀ i, C i →ₗ[R] C (i + 1))
attribute [scoped instance] Trunc.acg Trunc.mod Trunc.flat
variable {d}

Lean source · statement

theorem exists_trunc_zero (hdd : ∀ i, d (i + 1) ∘ₗ d i = 0) (n : ℕ)
    (hbdd : ∀ i, n < i → Subsingleton (C i))
    (hfin : ∀ i, Module.Finite R
      (LinearMap.ker (d (i + 1)) ⧸ (LinearMap.range (d i)).comap (LinearMap.ker (d (i +
        1))).subtype)) :
    Nonempty (Trunc d 0)

theorem

exists_model

L430 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.exists_model

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel
section Model
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
variable {C : ℕ → Type u} [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)]
  [∀ i, Module.Flat R (C i)]
variable {d : ∀ i, C i →ₗ[R] C (i + 1)}

Lean source · statement

theorem exists_model (T : Trunc d 0) (hfin0 : Module.Finite R (LinearMap.ker (d 0))) :
    ∃ (G : CoherentBaseChange.TwoTermComplex.{u, u} R) (ι0 : G.C0 →ₗ[R] C 0) (ι1 : G.C1 →ₗ[R] C 1)
      (comm : d 0 ∘ₗ ι0 = ι1 ∘ₗ G.d),
      ∀ (A : Type u) [CommRing A] [Algebra R A],
        Function.Bijective (TwoChartCech.kerMapBaseChange G.d (d 0) ι0 ι1 comm A)

theorem

main

L507 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.main

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel

Lean source · statement

theorem main
    (R : Type u) [CommRing R] [IsNoetherianRing R]
    (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)] [∀ i, Module.Flat R (C i)]
    (d : ∀ i, C i →ₗ[R] C (i + 1)) (hdd : ∀ i, d (i + 1) ∘ₗ d i = 0)
    (n : ℕ) (hbdd : ∀ i, n < i → Subsingleton (C i))
    (hfin0 : Module.Finite R (LinearMap.ker (d 0)))
    (hfin : ∀ i, Module.Finite R
      (LinearMap.ker (d (i + 1)) ⧸ (LinearMap.range (d i)).comap (LinearMap.ker (d (i +
        1))).subtype)) :
    ∃ (G : CoherentBaseChange.TwoTermComplex.{u, u} R) (ι0 : G.C0 →ₗ[R] C 0) (ι1 : G.C1 →ₗ[R] C 1)
      (comm : d 0 ∘ₗ ι0 = ι1 ∘ₗ G.d),
      ∀ (A : Type u) [CommRing A] [Algebra R A],
        Function.Bijective (TwoChartCech.kerMapBaseChange G.d (d 0) ι0 ι1 comm A)

theorem

main_trunc

L523 ↗

AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs.Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex.P2mMumfordKerModel.main_trunc

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct
namespace P2mMumfordKerModel

Lean source · statement

theorem main_trunc
    (R : Type u) [CommRing R] [IsNoetherianRing R]
    (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)] [∀ i, Module.Flat R (C i)]
    (d : ∀ i, C i →ₗ[R] C (i + 1)) (hdd : ∀ i, d (i + 1) ∘ₗ d i = 0)
    (n : ℕ) (hbdd : ∀ i, n < i → Subsingleton (C i))
    (hfin : ∀ i, Module.Finite R
      (LinearMap.ker (d (i + 1)) ⧸ (LinearMap.range (d i)).comap (LinearMap.ker (d (i +
        1))).subtype)) :
    ∃ (K : Type u) (_ : AddCommGroup K) (_ : Module R K) (_ : Module.Flat R K)
      (e : C 0 →ₗ[R] K) (ι : K →ₗ[R] C 1),
      ι ∘ₗ e = d 0 ∧ LinearMap.ker e = LinearMap.ker (d 0) ∧
      Module.Finite R (K ⧸ LinearMap.range e) ∧
      ∀ (A : Type u) [CommRing A] [Algebra R A],
        LinearMap.ker (e.baseChange A) = LinearMap.ker ((d 0).baseChange A)

theorem

exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex

L542 ↗

Module.exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.HomologicalAlgebra.Proofs
namespace Module_exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
universe u
open TensorProduct

Lean source · statement

theorem _root_.Module.exists_twoTermComplex_kerMapBaseChange_bijective_of_flat_complex
    (R : Type u) [CommRing R] [IsNoetherianRing R]
    (C : ℕ → Type u) [∀ i, AddCommGroup (C i)] [∀ i, Module R (C i)] [∀ i, Module.Flat R (C i)]
    (d : ∀ i, C i →ₗ[R] C (i + 1)) (hdd : ∀ i, d (i + 1) ∘ₗ d i = 0)
    (n : ℕ) (hbdd : ∀ i, n < i → Subsingleton (C i))
    (hfin0 : Module.Finite R (LinearMap.ker (d 0)))
    (hfin : ∀ i, Module.Finite R
      (LinearMap.ker (d (i + 1)) ⧸ (LinearMap.range (d i)).comap (LinearMap.ker (d (i +
        1))).subtype)) :
    ∃ (G : CoherentBaseChange.TwoTermComplex.{u, u} R) (ι0 : G.C0 →ₗ[R] C 0) (ι1 : G.C1 →ₗ[R] C 1)
      (comm : d 0 ∘ₗ ι0 = ι1 ∘ₗ G.d),
      ∀ (A : Type u) [CommRing A] [Algebra R A],
        Function.Bijective (TwoChartCech.kerMapBaseChange G.d (d 0) ι0 ι1 comm A)

Module documentation

Module exists two Term Complex ker Map Base Change bijective of flat complex

Declarations